have := exists_msmooth_zero_iff_one_iff_of_isClosed
  (modelWithCornersSelf ℝ ℝ) (s := Set.Iic a ∪ Set.Ici d) (t := Set.Icc b c)
  (IsClosed.union isClosed_Iic isClosed_Ici)
  (isClosed_Icc)
  (by
    simp_rw [Set.disjoint_union_left, Set.disjoint_iff, Set.subset_def, Set.mem_inter_iff, Set.mem_Iic, Set.mem_Icc,
      Set.mem_empty_iff_false, and_imp, imp_false, not_le, Set.mem_Ici]
    constructor <;> intros <;> linarith)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
this :
  ∃ f,
    Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) f ∧
      range f ⊆ Icc 0 1 ∧ (∀ (x : ℝ), x ∈ Iic a ∪ Ici d ↔ f x = 0) ∧ ∀ (x : ℝ), x ∈ Icc b c ↔ f x = 1
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d