split_ifs with h
case h.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 : ℝ
⊢ (if x ∈ Icc b c then 1 x else 0) ≤ Ψ x
case pos
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 : ℝ
h : x ∈ Icc b c
⊢ 1 x ≤ Ψ x

case neg
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 : ℝ
h : x ∉ Icc b c
⊢ 0 ≤ Ψ x