Theorem: interval_approx_inf (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0 := nhdsWithin_le_nhds <| Iio_mem_nhds (by linarith)
State after:
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
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
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
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
filter_upwards [self_mem_nhdsWithin, l1] with ε (hε : 0 < ε) (hε' : ε < (b - a) / 3)
State after:
case h
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l2 : a < a + ε / 2 := by linarith
State after:
case h
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l3 : b - ε / 2 < b := by linarith
State after:
case h
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
obtain ⟨ψ, h1, h2, h3, h4, h5⟩ := smooth_urysohn_support_Ioo l2 l3
State after:
case h.intro.intro.intro.intro.intro
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h.intro.intro.intro.intro.intro
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
refine ⟨ψ, h1, h2, ?_, ?_, ?_⟩
State after:
case h.intro.intro.intro.intro.intro.refine_1
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
⊢ closure (Function.support ψ) ⊆ Ioi 0

case h.intro.intro.intro.intro.intro.refine_2
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
⊢ ψ ≤ (Ico a b).indicator 1

case h.intro.intro.intro.intro.intro.refine_3
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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
⊢ 0 < (b - a) / 3
Tactic:
linarith
State after:
no goals

State before:
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
⊢ a < a + ε / 2
Tactic:
linarith
State after:
no goals

State before:
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
⊢ b - ε / 2 < b
Tactic:
linarith
State after:
no goals

State before:
case h.intro.intro.intro.intro.intro.refine_1
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
⊢ closure (Function.support ψ) ⊆ Ioi 0
Tactic:
simp [h5, hab.ne, Icc_subset_Ioi_iff hab.le, ha]
State after:
no goals

State before:
case h.intro.intro.intro.intro.intro.refine_2
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
⊢ ψ ≤ (Ico a b).indicator 1
Tactic:
exact h4.trans <| indicator_le_indicator_of_subset Ioo_subset_Ico_self (by simp)
State after:
no goals

State before:
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
⊢ ∀ (a : ℝ), 0 ≤ 1 a
Tactic:
simp
State after:
no goals

State before:
case h.intro.intro.intro.intro.intro.refine_3
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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l4 : 0 ≤ b - a - ε := by linarith
State after:
case h.intro.intro.intro.intro.intro.refine_3
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 - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h.intro.intro.intro.intro.intro.refine_3
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 - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l5 : Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0 := by intro t ht ; simp at ht ⊢ ; linarith
State after:
case h.intro.intro.intro.intro.intro.refine_3
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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h.intro.intro.intro.intro.intro.refine_3
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
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l6 : Icc (a + ε / 2) (b - ε / 2) ∩ Ioi 0 = Icc (a + ε / 2) (b - ε / 2) := inter_eq_left.mpr l5
State after:
case h.intro.intro.intro.intro.intro.refine_3
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)
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h.intro.intro.intro.intro.intro.refine_3
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)
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l7 : ∫ y in Ioi 0, indicator (Icc (a + ε / 2) (b - ε / 2)) 1 y = b - a - ε := by
  simp [l6] ; convert ENNReal.toReal_ofReal l4 using 3 ; ring
State after:
case h.intro.intro.intro.intro.intro.refine_3
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h.intro.intro.intro.intro.intro.refine_3
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l8 : IntegrableOn ψ (Ioi 0) volume := (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn
State after:
case h.intro.intro.intro.intro.intro.refine_3
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h.intro.intro.intro.intro.intro.refine_3
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
rw [← l7]
State after:
case h.intro.intro.intro.intro.intro.refine_3
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y ≤ ∫ (y : ℝ) in Ioi 0, ψ y

State before:
case h.intro.intro.intro.intro.intro.refine_3
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
apply setIntegral_mono ?_ l8 h3
State after:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn ((Icc (a + ε / 2) (b - ε / 2)).indicator 1) (Ioi 0) volume

State before:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn ((Icc (a + ε / 2) (b - ε / 2)).indicator 1) (Ioi 0) volume
Tactic:
rw [IntegrableOn, integrable_indicator_iff measurableSet_Icc]
State after:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) (volume.restrict (Ioi 0))

State before:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) (volume.restrict (Ioi 0))
Tactic:
apply IntegrableOn.mono ?_ subset_rfl Measure.restrict_le_self
State after:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) volume

State before:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ IntegrableOn 1 (Icc (a + ε / 2) (b - ε / 2)) volume
Tactic:
apply integrableOn_const.mpr
State after:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ Real.one = 0 ∨ volume (Icc (a + ε / 2) (b - ε / 2)) < ⊤

State before:
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)
l7 : ∫ (y : ℝ) in Ioi 0, (Icc (a + ε / 2) (b - ε / 2)).indicator 1 y = b - a - ε
l8 : IntegrableOn ψ (Ioi 0) volume
⊢ Real.one = 0 ∨ volume (Icc (a + ε / 2) (b - ε / 2)) < ⊤
Tactic:
simp
State after:
no goals

State before:
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
⊢ 0 ≤ b - a - ε
Tactic:
linarith
State after:
no goals

State before:
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 - ε
⊢ Icc (a + ε / 2) (b - ε / 2) ⊆ Ioi 0
Tactic:
intro t ht
State after:
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 - ε
t : ℝ
ht : t ∈ Icc (a + ε / 2) (b - ε / 2)
⊢ t ∈ Ioi 0

State before:
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 - ε
t : ℝ
ht : t ∈ Icc (a + ε / 2) (b - ε / 2)
⊢ t ∈ Ioi 0
Tactic:
simp at ht ⊢
State after:
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 - ε
t : ℝ
ht : a + ε / 2 ≤ t ∧ t ≤ b - ε / 2
⊢ 0 < t

State before:
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 - ε
t : ℝ
ht : a + ε / 2 ≤ t ∧ t ≤ b - ε / 2
⊢ 0 < t
Tactic:
linarith
State after:
no goals

State before:
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 - ε
Tactic:
simp [l6]
State after:
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 - ε

State before:
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 - ε
Tactic:
convert ENNReal.toReal_ofReal l4 using 3
State after:
case h.e'_2.h.e'_1.h.e'_1
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)
⊢ b - ε / 2 - (a + ε / 2) = b - a - ε

State before:
case h.e'_2.h.e'_1.h.e'_1
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)
⊢ b - ε / 2 - (a + ε / 2) = b - a - ε
Tactic:
ring
State after:
no goals