awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
neg : eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
repeat rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ

Tactic:
eLpNorm'_add_le hf hg hp1_real

Premises used: MeasureTheory.eLpNorm'_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ

Tactic:
exact eLpNorm'_add_le hf hg hp1_real

Premises used: MeasureTheory.eLpNorm'_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
inl : eLpNorm (f + g) 0 μ ≤ LpAddConst 0 * (eLpNorm f 0 μ + eLpNorm g 0 μ)
inr : ∀ (hp : p ≠ 0), eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ eLpNorm (f + g) 0 μ ≤ LpAddConst 0 * (eLpNorm f 0 μ + eLpNorm g 0 μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
inr : ∀ (h'p : p < 1), eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
inr₁ : ∀ (h'p : 1 ≤ p), eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
rcases lt_or_ge p 1 with (h'p | h'p)

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
inr : eLpNorm' (f + g) p.toReal μ ≤ p.LpAddConst * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
simp only [eLpNorm_eq_eLpNorm' hp (h'p.trans ENNReal.one_lt_top).ne]

Premises used: ENNReal.one_lt_top, MeasureTheory.eLpNorm_eq_eLpNorm', LT.lt.trans, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm' (f + g) p.toReal μ ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)

Tactic:
eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _

Premises used: ENNReal.toReal_nonneg, MeasureTheory.eLpNorm'_add_le_of_le_one
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
h : p.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1)
inr : p.toReal ≤ 1
⊢ eLpNorm' (f + g) p.toReal μ ≤ p.LpAddConst * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)

Tactic:
convert! eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _

Premises used: ENNReal.toReal_nonneg, MeasureTheory.eLpNorm'_add_le_of_le_one
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p

Tactic:
have : p ∈ Set.Ioo (0 : ℝ≥0∞) 1 := ⟨hp.bot_lt, h'p⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
this : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
⊢ p.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1)

Tactic:
simp only [LpAddConst, if_pos this]

Premises used: if_pos, ENNReal.LpAddConst
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ p.toReal ≤ 1

Tactic:
simpa using ENNReal.toReal_mono ENNReal.one_ne_top h'p.le

Premises used: LT.lt.le, ENNReal.toReal_mono, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
simpa [LpAddConst_of_one_le h'p] using eLpNorm_add_le hf hg h'p

Premises used: ENNReal.LpAddConst_of_one_le, MeasureTheory.eLpNorm_add_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
⊢ Tendsto (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 (p.LpAddConst * HAdd.hAdd (α := ℝ≥0∞) 0 0))

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
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 (p.LpAddConst * HAdd.hAdd (α := ℝ≥0∞) 0 0))
⊢ Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)

Tactic:
simp only [add_zero, mul_zero] at this

Premises used: MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
rcases :
  ∀ (η : ℝ≥0∞) (hη : p.LpAddConst * (η + η) < δ) (ηpos : 0 < η),
    ∃ (η : ℝ≥0∞),
      0 < η ∧
        ∀ (f g : α → ε),
          AEStronglyMeasurable f μ →
            AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ
⊢ ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        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⟩

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, And.right, self_mem_nhdsWithin, Iff.mp, Ne.bot_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
⊢ ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
refine :
  ∀ (f g : α → ε) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (Hf : eLpNorm f p μ ≤ η)
    (Hg : eLpNorm g p μ ≤ η), eLpNorm (f + g) p μ < δ
⊢ ∃ (η : ℝ≥0∞),
    0 < η ∧
      ∀ (f g : α → ε),
        AEStronglyMeasurable f μ →
          AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < δ

Tactic:
refine ⟨η, ηpos, fun f g hf hg Hf Hg => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
eLpNorm_add_le' hf hg p

Premises used: MeasureTheory.eLpNorm_add_le'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ) ≤ p.LpAddConst * (η + η)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ p.LpAddConst * (η + η) < δ

Tactic:
hη
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (β := ℝ≥0∞) (fun (η : ℝ≥0∞) ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : MeasureTheory.eLpNorm f p μ ≤ η
Hg : MeasureTheory.eLpNorm g p μ ≤ η
eLpNorm : p.LpAddConst * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ) ≤ p.LpAddConst * (η + η)
⊢ MeasureTheory.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η

Premises used: HAdd.hAdd, ENNReal.LpAddConst, MeasureTheory.eLpNorm_add_le', MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ eLpNorm (f - g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
simpa only [sub_eq_add_neg, eLpNorm_neg] using eLpNorm_add_le' hf hg.neg p

Premises used: sub_eq_add_neg, MeasureTheory.AEStronglyMeasurable.neg, MeasureTheory.eLpNorm_neg, MeasureTheory.eLpNorm_add_le'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp : 1 ≤ p
⊢ eLpNorm (f - g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
simpa [LpAddConst_of_one_le hp] using eLpNorm_sub_le' hf hg p

Premises used: ENNReal.LpAddConst_of_one_le, MeasureTheory.eLpNorm_sub_le'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : MemLp f p μ
hg : MemLp g p μ
apply : eLpNorm f p μ + eLpNorm g p μ < ∞
⊢ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ) < ∞

Tactic:
apply ENNReal.mul_lt_top (LpAddConst_lt_top p)

Premises used: ENNReal.LpAddConst_lt_top, ENNReal.mul_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm f p μ + eLpNorm g p μ < ∞

Tactic:
ENNReal.add_lt_top.2 ⟨hf.2, hg.2⟩

Premises used: Iff.mpr, And.right, And.intro, ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm f p μ + eLpNorm g p μ < ∞

Tactic:
exact ENNReal.add_lt_top.2 ⟨hf.2, hg.2⟩

Premises used: Iff.mpr, And.right, And.intro, ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
q : ℝ
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
f : ι → α → ε'
s : Finset ι
hfs : ∀ i ∈ s, AEStronglyMeasurable (f i) μ
hq1 : 1 ≤ q
⊢ eLpNorm'.{u_1, u_4} (ε := ε') (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, eLpNorm' (f i) q μ

Tactic:
Finset.le_sum_of_subadditive_on_pred (fun f : α → ε' => eLpNorm' f q μ)
    (fun f => AEStronglyMeasurable f μ) (eLpNorm'_zero (zero_lt_one.trans_le hq1)).le
    (fun _f _g hf hg => eLpNorm'_add_le hf hg hq1) (fun _f _g hf hg => hf.add hg) _ hfs

Premises used: Finset.le_sum_of_subadditive_on_pred, MeasureTheory.eLpNorm', Eq.le, MeasureTheory.AEStronglyMeasurable.add, MeasureTheory.eLpNorm'_zero, zero_lt_one, LT.lt.trans_le, MeasureTheory.eLpNorm'_add_le, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
f : ι → α → ε'
s : Finset ι
hfs : ∀ i ∈ s, AEStronglyMeasurable (f i) μ
hp1 : 1 ≤ p
⊢ eLpNorm.{u_1, u_4} (ε := ε') (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, eLpNorm (f i) p μ

Tactic:
Finset.le_sum_of_subadditive_on_pred (fun f : α → ε' => eLpNorm f p μ)
    (fun f => AEStronglyMeasurable f μ) eLpNorm_zero.le
    (fun _f _g hf hg => eLpNorm_add_le hf hg hp1)
    (fun _f _g hf hg => hf.add hg) _ hfs

Premises used: Finset.le_sum_of_subadditive_on_pred, MeasureTheory.eLpNorm_zero, Eq.le, MeasureTheory.AEStronglyMeasurable.add, MeasureTheory.eLpNorm_add_le, MeasureTheory.AEStronglyMeasurable, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
inst_2 : ContinuousAdd ε
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f + g) p μ

Tactic:
⟨AEStronglyMeasurable.add hf.1 hg.1, eLpNorm_add_lt_top hf hg⟩

Premises used: MeasureTheory.eLpNorm_add_lt_top, MeasureTheory.AEStronglyMeasurable.add, MeasureTheory.MemLp, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
rw : MemLp (f + -g) p μ
⊢ MemLp (f - g) p μ

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f + -g) p μ

Tactic:
hf.add hg.neg

Premises used: MeasureTheory.MemLp.add, MeasureTheory.MemLp.neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f + -g) p μ

Tactic:
exact hf.add hg.neg

Premises used: MeasureTheory.MemLp.add, MeasureTheory.MemLp.neg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
haveI : ∀ (this : DecidableEq ι), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ

Tactic:
haveI : DecidableEq ι := Classical.decEq _
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
this : DecidableEq ι
revert : ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ

Tactic:
revert hf
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
this : DecidableEq ι
⊢ ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
this : DecidableEq ι
refine_1 :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ),
    MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p μ
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ) →
        ∀ (hf : ∀ i ∈ insert a s, MemLp (f i) p μ),
          MemLp.{u_1, u_4} (ε := ε') (fun (a_3 : α) ↦ ∑ i ∈ insert a s, f i a_3) p μ
⊢ ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
this : DecidableEq ι
⊢ ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) p μ),
    MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s_1 : Finset ι
f : ι → α → ε'
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
refine_2 : MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ insert i s, f i a) p μ

Tactic:
simp only [his, Finset.sum_insert, not_false_iff]

Premises used: Finset.sum_insert, not_false_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s_1 : Finset ι
f : ι → α → ε'
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p μ

Tactic:
(hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Premises used: Finset.mem_insert_self, MeasureTheory.MemLp.add, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s_1 : Finset ι
f : ι → α → ε'
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) p μ), MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p μ

Tactic:
exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Premises used: Finset.mem_insert_self, MeasureTheory.MemLp.add, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddCommMonoid ε'
p : ℝ≥0∞
μ : Measure α
inst_2 : ContinuousAdd ε'
ι : Type u_5
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ MemLp.{u_1, u_4} (ε := ε') (fun (a : α) ↦ ∑ i ∈ s, f i a) p μ

Tactic:
memLp_finsetSum s hf

Premises used: MeasureTheory.memLp_finsetSum