intro x
case h.right.right.right.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Ψ ≤ (Ioo a d).indicator 1
case h.right.right.right.left
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
⊢ Ψ x ≤ (Ioo a d).indicator 1 x