simp [l6]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
⊢ ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
l2 : a < a + ε / 2
l3 : b - ε / 2 < b
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc (a + ε / 2) (b - ε / 2)).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo a b).indicator 1
h5 : Function.support ψ = Ioo a b
l4 : 0 ≤ b - a - ε
l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2)
⊢ (ENNReal.ofReal (b - ε / 2 - (a + ε / 2))).toReal = b - a - ε