-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem exists_Lp_half (p : ℝ≥0∞) {δ : ℝ≥0∞} (hδ : δ ≠ 0) :
    ∃ η : ℝ≥0∞,
      0 < η ∧
        ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ →
          eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : LpAddConst p * (η + η) < δ
ηpos : 0 < η
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) ≤ LpAddConst p * (η + η)

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : LpAddConst p * (η + η) < δ
ηpos : 0 < η
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Tactic:
refine ⟨η, ηpos, fun f g hf hg Hf Hg => ?_⟩

Result:
case intro.intro
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : LpAddConst p * (η + η) < δ
ηpos : 0 < η
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ eLpNorm (f + g) p μ < δ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Tactic:
rcases (((tendsto_order.1 this).2 δ hδ.bot_lt).and self_mem_nhdsWithin).exists with ⟨η, hη, ηpos⟩

Result:
case intro.intro
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : LpAddConst p * (η + η) < δ
ηpos : 0 < η
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Tactic:
have :
  Tendsto (fun η : ℝ≥0∞ => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 (LpAddConst p * (0 + 0))) :=
  (ENNReal.Tendsto.const_mul (tendsto_id.add tendsto_id)
        (Or.inr (LpAddConst_lt_top p).ne)).mono_left
    nhdsWithin_le_nhds

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 (LpAddConst p * (0 + 0)))
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : LpAddConst p * (η + η) < δ
ηpos : 0 < η
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ eLpNorm (f + g) p μ < δ

Tactic:
calc
  eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) := eLpNorm_add_le' hf hg p
  _ ≤ LpAddConst p * (η + η) := by gcongr
  _ < δ := hη

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 (LpAddConst p * (0 + 0)))
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Tactic:
simp only [add_zero, mul_zero] at this

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η => LpAddConst p * (η + η)) (𝓝[>] 0) (𝓝 0)
⊢ ∃ η,
    0 < η ∧
      ∀ (f g : α → E),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ