Theorem: SmoothExistence (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
have := smooth_urysohn_support_Ioo (a := 1 / 2) (b := 1) (c := 3/2) (d := 2) (by linarith)
  (by linarith)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
this :
  ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧
        (Icc 1 (3 / 2)).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo (1 / 2) 2).indicator 1 ∧ Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
this :
  ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧
        (Icc 1 (3 / 2)).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo (1 / 2) 2).indicator 1 ∧ Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
rcases this with ⟨Ψ, hΨContDiff, _, hΨ0, hΨ1, hΨSupport⟩
State after:
case intro.intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x

State before:
case intro.intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
use Ψ, hΨContDiff
State after:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x

State before:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
unfold indicator at hΨ0 hΨ1
State after:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (fun x => if x ∈ Icc 1 (3 / 2) then 1 x else 0) ≤ Ψ
hΨ1 : Ψ ≤ fun x => if x ∈ Ioo (1 / 2) 2 then 1 x else 0
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x

State before:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (fun x => if x ∈ Icc 1 (3 / 2) then 1 x else 0) ≤ Ψ
hΨ1 : Ψ ≤ fun x => if x ∈ Ioo (1 / 2) 2 then 1 x else 0
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
simp only [mem_Icc, Pi.one_apply, Pi.le_def, mem_Ioo] at hΨ0 hΨ1
State after:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x

State before:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
simp only [hΨSupport, subset_def, mem_Ioo, mem_Icc, and_imp]
State after:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ (∀ (x : ℝ), 1 / 2 < x → x < 2 → 1 / 2 ≤ x ∧ x ≤ 2) ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x

State before:
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ (∀ (x : ℝ), 1 / 2 < x → x < 2 → 1 / 2 ≤ x ∧ x ≤ 2) ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
split_ands
State after:
case right.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (x : ℝ), 0 ≤ Ψ x

case right.refine_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (x : ℝ), 1 / 2 < x → x < 2 → 1 / 2 ≤ x ∧ x ≤ 2

case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
h : ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Tactic:
rcases h with ⟨Ψ, hΨ, hΨnonneg, hΨsupp, hΨpos⟩
State after:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1

State before:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Tactic:
let c := (∫ x in Ici 0, Ψ x / x)
State after:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1

State before:
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
Tactic:
use fun y ↦ Ψ y / c
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (ContDiff ℝ ⊤ fun y => Ψ y / c) ∧
    (∀ (x : ℝ), 0 ≤ Ψ x / c) ∧ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (ContDiff ℝ ⊤ fun y => Ψ y / c) ∧
    (∀ (x : ℝ), 0 ≤ Ψ x / c) ∧ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
Tactic:
refine ⟨hΨ.div_const c, fun y ↦ div_nonneg (hΨnonneg y) (le_of_lt hΨpos), ?_, ?_⟩
State after:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2

case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1

State before:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2
Tactic:
rw [Function.support_div, Function.support_const (ne_of_lt hΨpos).symm, inter_univ]
State after:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y) ⊆ Icc (1 / 2) 2

State before:
case h.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y) ⊆ Icc (1 / 2) 2
Tactic:
convert hΨsupp
State after:
no goals

State before:
case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
Tactic:
simp only [div_right_comm _ c _, integral_div c, div_self <| ne_of_gt hΨpos]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ 1 / 2 < 1
Tactic:
linarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ 3 / 2 < 2
Tactic:
linarith
State after:
no goals

State before:
case right.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (x : ℝ), 0 ≤ Ψ x
Tactic:
exact fun x ↦ le_trans (by simp [apply_ite]) (hΨ0 x)
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ 0 ≤ if 1 ≤ x ∧ x ≤ 3 / 2 then 1 else 0
Tactic:
simp [apply_ite]
State after:
no goals

State before:
case right.refine_2.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (x : ℝ), 1 / 2 < x → x < 2 → 1 / 2 ≤ x ∧ x ≤ 2
Tactic:
exact fun y hy hy' ↦ ⟨by linarith, by linarith⟩
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
hy : 1 / 2 < y
hy' : y < 2
⊢ 1 / 2 ≤ y
Tactic:
linarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
hy : 1 / 2 < y
hy' : y < 2
⊢ y ≤ 2
Tactic:
linarith
State after:
no goals

State before:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
Tactic:
rw [integral_pos_iff_support_of_nonneg]
State after:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 < (volume.restrict (Ici 0)) (Function.support fun x => Ψ x / x)

case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 ≤ fun x => Ψ x / x

case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ Integrable (fun x => Ψ x / x) (volume.restrict (Ici 0))

State before:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 < (volume.restrict (Ici 0)) (Function.support fun x => Ψ x / x)
Tactic:
simp only [Function.support_div, measurableSet_Ici, Measure.restrict_apply', hΨSupport, Function.support_id]
State after:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 < volume (Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0)

State before:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 = Ioo (1 / 2) 2
⊢ 0 < volume (Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0)
Tactic:
simp only [this, volume_Ioo, ENNReal.ofReal_pos, sub_pos, gt_iff_lt]
State after:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 = Ioo (1 / 2) 2
⊢ 1 / 2 < 2

State before:
case right.refine_2.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 = Ioo (1 / 2) 2
⊢ 1 / 2 < 2
Tactic:
linarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 = Ioo (1 / 2) 2
Tactic:
ext x
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ x ∈ Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 ↔ x ∈ Ioo (1 / 2) 2

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ x ∈ Ioo (1 / 2) 2 ∩ (Iio 0 ∪ Ioi 0) ∩ Ici 0 ↔ x ∈ Ioo (1 / 2) 2
Tactic:
simp only [mem_inter_iff, mem_Ioo, mem_Ici, mem_Iio, mem_Ioi,
  mem_union, not_lt, and_true, not_le]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x ↔ 1 / 2 < x ∧ x < 2

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x ↔ 1 / 2 < x ∧ x < 2
Tactic:
constructor
State after:
case h.mp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x → 1 / 2 < x ∧ x < 2

case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ 1 / 2 < x ∧ x < 2 → ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x

State before:
case h.mp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x → 1 / 2 < x ∧ x < 2
Tactic:
exact fun h ↦ h.left.left
State after:
no goals

State before:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
⊢ 1 / 2 < x ∧ x < 2 → ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x
Tactic:
intro h
State after:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x

State before:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x
Tactic:
simp only [h, and_self, lt_or_lt_iff_ne, ne_eq, true_and]
State after:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ¬x = 0 ∧ 0 ≤ x

State before:
case h.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
x : ℝ
h : 1 / 2 < x ∧ x < 2
⊢ ¬x = 0 ∧ 0 ≤ x
Tactic:
constructor <;> linarith [h.left]
State after:
no goals

State before:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ 0 ≤ fun x => Ψ x / x
Tactic:
simp_rw [Pi.le_def, Pi.zero_apply]
State after:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (i : ℝ), 0 ≤ Ψ i / i

State before:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ ∀ (i : ℝ), 0 ≤ Ψ i / i
Tactic:
intro y
State after:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
⊢ 0 ≤ Ψ y / y

State before:
case right.refine_2.refine_2.hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
⊢ 0 ≤ Ψ y / y
Tactic:
by_cases h : y ∈ Function.support Ψ
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ Ψ y / y

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ Ψ y / y

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
. apply div_nonneg <| le_trans (by simp [apply_ite]) (hΨ0 y)
  rw [hΨSupport, mem_Ioo] at h; linarith [h.left]
State after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
. simp only [Function.mem_support, ne_eq, not_not] at h; simp [h]
State after:
no goals

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
apply div_nonneg <| le_trans (by simp [apply_ite]) (hΨ0 y)
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ y

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ y
Tactic:
rw [hΨSupport, mem_Ioo] at h
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : 1 / 2 < y ∧ y < 2
⊢ 0 ≤ y

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : 1 / 2 < y ∧ y < 2
⊢ 0 ≤ y
Tactic:
linarith [h.left]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ if 1 ≤ y ∧ y ≤ 3 / 2 then 1 else 0
Tactic:
simp [apply_ite]
State after:
no goals

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∉ Function.support Ψ
⊢ 0 ≤ Ψ y / y
Tactic:
simp only [Function.mem_support, ne_eq, not_not] at h
State after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : Ψ y = 0
⊢ 0 ≤ Ψ y / y

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : Ψ y = 0
⊢ 0 ≤ Ψ y / y
Tactic:
simp [h]
State after:
no goals

State before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ Integrable (fun x => Ψ x / x) (volume.restrict (Ici 0))
Tactic:
have : (fun x ↦ Ψ x / x).support ⊆ Icc (1 / 2) 2 := by
  rw [Function.support_div, hΨSupport]
  apply subset_trans (by apply inter_subset_left) Ioo_subset_Icc_self
State after:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ Integrable (fun x => Ψ x / x) (volume.restrict (Ici 0))

State before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ Integrable (fun x => Ψ x / x) (volume.restrict (Ici 0))
Tactic:
apply (integrableOn_iff_integrable_of_support_subset this).mp
State after:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ IntegrableOn (fun x => Ψ x / x) (Icc (1 / 2) 2) (volume.restrict (Ici 0))

State before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ IntegrableOn (fun x => Ψ x / x) (Icc (1 / 2) 2) (volume.restrict (Ici 0))
Tactic:
apply ContinuousOn.integrableOn_compact isCompact_Icc
State after:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ContinuousOn (fun x => Ψ x / x) (Icc (1 / 2) 2)

State before:
case right.refine_2.refine_2.hfi
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ContinuousOn (fun x => Ψ x / x) (Icc (1 / 2) 2)
Tactic:
apply hΨContDiff.continuous.continuousOn.div continuousOn_id ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ x ∈ Icc (1 / 2) 2, id x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ x ∈ Icc (1 / 2) 2, id x ≠ 0
Tactic:
simp only [mem_Icc, ne_eq, and_imp, id_eq]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 1 / 2 ≤ x → x ≤ 2 → ¬x = 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 1 / 2 ≤ x → x ≤ 2 → ¬x = 0
Tactic:
intros
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
x✝ : ℝ
a✝¹ : 1 / 2 ≤ x✝
a✝ : x✝ ≤ 2
⊢ ¬x✝ = 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
this : (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
x✝ : ℝ
a✝¹ : 1 / 2 ≤ x✝
a✝ : x✝ ≤ 2
⊢ ¬x✝ = 0
Tactic:
linarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Function.support fun x => Ψ x / x) ⊆ Icc (1 / 2) 2
Tactic:
rw [Function.support_div, hΨSupport]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Ioo (1 / 2) 2 ∩ Function.support fun x => x) ⊆ Icc (1 / 2) 2

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Ioo (1 / 2) 2 ∩ Function.support fun x => x) ⊆ Icc (1 / 2) 2
Tactic:
apply subset_trans (by apply inter_subset_left) Ioo_subset_Icc_self
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
⊢ (Ioo (1 / 2) 2 ∩ Function.support fun x => x) ⊆ Ioo (1 / 2) 2
Tactic:
apply inter_subset_left
State after:
no goals