-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem exists_eLpNorm_indicator_le (hp : p ≠ ∞) (c : E) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _ => c) p μ ≤ ε

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Tactic:
have :
  Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
    (𝓝 (0 : ℝ≥0)) := by
  rw [ENNReal.tendsto_coe]
  convert (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
  simp [hp₀''.ne']

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Tactic:
have hε' : 0 < ε := hε.bot_lt

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Proof state:
case h.e'_5.h.e'_3
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ 0 = ‖c‖₊ * 0 ^ (1 / p.toReal)

Tactic:
simp [hp₀''.ne']

Result:
no goals

Proof state:
case inr
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε

Tactic:
obtain ⟨η, hη_pos, hη_le⟩ : ∃ η : ℝ≥0, 0 < η ∧ ‖c‖ₑ * (η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε := by
  have :
    Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
      (𝓝 (0 : ℝ≥0)) := by
    rw [ENNReal.tendsto_coe]
    convert (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
    simp [hp₀''.ne']
  have hε' : 0 < ε := hε.bot_lt
  obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε')
  obtain ⟨η, hη, hηδ⟩ := exists_between hδ
  refine ⟨η, hη, ?_⟩
  simpa only [← ENNReal.coe_rpow_of_nonneg _ hp₀', enorm, ← ENNReal.coe_mul] using hδε' hηδ

Result:
case inr.intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
η : ℝ≥0
hη_pos : 0 < η
hη_le : ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε

Proof state:
case inr.intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
η : ℝ≥0
hη_pos : 0 < η
hη_le : ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε
s : Set α
hs : μ s ≤ ↑η
⊢ eLpNorm (s.indicator fun x => c) p μ ≤ ε

Tactic:
refine (eLpNorm_indicator_const_le _ _).trans (le_trans ?_ hη_le)

Result:
case inr.intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
η : ℝ≥0
hη_pos : 0 < η
hη_le : ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε
s : Set α
hs : μ s ≤ ↑η
⊢ ‖c‖ₑ * μ s ^ (1 / p.toReal) ≤ ‖c‖ₑ * ↑η ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Tactic:
obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε')

Result:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / p.toReal)) ≤ ε
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ Tendsto (fun x => ‖c‖₊ * x ^ (1 / p.toReal)) (𝓝 0) (𝓝 0)

Tactic:
convert (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _

Result:
case h.e'_5.h.e'_3
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ 0 = ‖c‖₊ * 0 ^ (1 / p.toReal)

Proof state:
case inl
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
hp : 0 ≠ ⊤
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) 0 μ ≤ ε

Tactic:
exact ⟨1, zero_lt_one, fun s _ => by simp⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / p.toReal)) ≤ ε
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Tactic:
obtain ⟨η, hη, hηδ⟩ := exists_between hδ

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x => ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / p.toReal)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ∃ η, 0 < η ∧ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Proof state:
case inr
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε

Tactic:
have hp₀' : 0 ≤ 1 / p.toReal := div_nonneg zero_le_one ENNReal.toReal_nonneg

Result:
case inr
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ⊤
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x => c) p μ ≤ ε