awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f_1 g_1 : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : MeasureTheory.Integrable f μ
hgi : MeasureTheory.Integrable g μ
⊢ MeasureTheory.Integrable (f + g) μ

Tactic:
exact hfi.add hgi

Premises used: MeasureTheory.Integrable.add
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α →ₘ[μ] β
hf : f.Integrable
hg : g.Integrable
⊢ (f - g).Integrable

Tactic:
(sub_eq_add_neg f g).symm ▸ hf.add hg.neg

Premises used: sub_eq_add_neg, Eq.rec, MeasureTheory.AEEqFun.Integrable.neg, Eq.symm, MeasureTheory.AEEqFun.Integrable.add
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_5
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ₘ[μ] β
_f : α → β
hfm : AEStronglyMeasurable _f μ
hfi : (mk _f hfm).Integrable
⊢ MeasureTheory.Integrable (ε := β)
    ((fun (x : β) ↦ c • x) ∘ (↑(Subtype.mk (p := fun (f : α → β) ↦ AEStronglyMeasurable f μ) _f hfm) : α → β)) μ

Tactic:
simpa using ((integrable_mk hfm).1 hfi).smul c

Premises used: MeasureTheory.AEEqFun.integrable_mk, MeasureTheory.Integrable.smul, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
rw : MemLp (↑(↑f : α →ₘ[μ] β) : α → β) 1 μ
⊢ Integrable (↑(↑f : α →ₘ[μ] β) : α → β) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ MemLp (↑(↑f : α →ₘ[μ] β) : α → β) 1 μ

Tactic:
Lp.memLp f

Premises used: MeasureTheory.Lp.memLp
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ MemLp (↑(↑f : α →ₘ[μ] β) : α → β) 1 μ

Tactic:
exact Lp.memLp f

Premises used: MeasureTheory.Lp.memLp
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ HasFiniteIntegral (↑(↑f : α →ₘ[μ] β) : α → β) μ

Tactic:
(integrable_coeFn f).hasFiniteIntegral

Premises used: MeasureTheory.L1.integrable_coeFn, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ StronglyMeasurable (↑(↑f : α →ₘ[μ] β) : α → β)

Tactic:
Lp.stronglyMeasurable f

Premises used: MeasureTheory.Lp.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
f : ↥(Lp β 1 μ)
⊢ Measurable (↑(↑f : α →ₘ[μ] β) : α → β)

Tactic:
(Lp.stronglyMeasurable f).measurable

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] β) : α → β) μ

Tactic:
Lp.aestronglyMeasurable f

Premises used: MeasureTheory.Lp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
f : ↥(Lp β 1 μ)
⊢ AEMeasurable (↑(↑f : α →ₘ[μ] β) : α → β) μ

Tactic:
(Lp.stronglyMeasurable f).measurable.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
simp :
  (if Eq (α := ℝ≥0∞) 1 ∞ then eLpNormEssSup ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) μ
    else ∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ
⊢ edist f g = ∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ

Tactic:
simp only [Lp.edist_def, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm, Pi.sub_apply,
    toReal_one, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]

Premises used: MeasureTheory.Lp.edist_def, ENNReal.toReal_one, ite_false, ENNReal.rpow_one, ne_eq, MeasureTheory.eLpNorm'_eq_lintegral_enorm, one_ne_zero, not_false_eq_true, div_self, Pi.sub_apply, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (if Eq (α := ℝ≥0∞) 1 ∞ then eLpNormEssSup ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) μ
    else ∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ

Tactic:
simp [edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
simp_rw :
  (edist f g).toReal = (∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ).toReal
⊢ dist f g = (∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ).toReal

Tactic:
simp_rw [dist_edist, edist_def]

Premises used: dist_edist, MeasureTheory.L1.edist_def
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ‖f‖ = (∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ).toReal

Tactic:
simp [Lp.norm_def, eLpNorm, eLpNorm'_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm'_eq_lintegral_enorm, MeasureTheory.eLpNorm, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
rw :
  (∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ).toReal =
    (∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ).toReal
⊢ ‖f - g‖ = (∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ).toReal

Tactic:
rw [norm_def]

Premises used: MeasureTheory.L1.norm_def
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
e_a :
  ∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ =
    ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ
⊢ (∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ).toReal =
    (∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ).toReal

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
e_a :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ) fun (a : α) ↦
    ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ
⊢ ∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ =
    ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ

Tactic:
rw [lintegral_congr_ae]

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
h :
  ∀ (a : α) (ha : (↑(↑(f - g) : α →ₘ[μ] β) : α → β) a = ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) a),
    ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ = ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ) fun (a : α) ↦
    ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ

Tactic:
filter_upwards [Lp.coeFn_sub f g] with _ ha

Premises used: MeasureTheory.Lp.coeFn_sub
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a : α
ha : (↑(↑(f - g) : α →ₘ[μ] β) : α → β) a = ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) a
⊢ ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ = ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ

Tactic:
simp only [ha, Pi.sub_apply]

Premises used: Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
rw : ∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ ≠ ∞
⊢ ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ

Tactic:
rw [norm_def, ENNReal.ofReal_toReal]

Premises used: MeasureTheory.L1.norm_def, ENNReal.ofReal_toReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ ≠ ∞

Tactic:
ne_of_lt (hasFiniteIntegral_coeFn f)

Premises used: MeasureTheory.L1.hasFiniteIntegral_coeFn, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ ≠ ∞

Tactic:
exact ne_of_lt (hasFiniteIntegral_coeFn f)

Premises used: MeasureTheory.L1.hasFiniteIntegral_coeFn, ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
simp_rw :
  ∫⁻ (x : α), edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) x) 0 ∂μ =
    ∫⁻ (x : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x) 0 ∂μ
⊢ ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ

Tactic:
simp_rw [ofReal_norm_eq_lintegral, ← edist_zero_right]

Premises used: MeasureTheory.L1.ofReal_norm_eq_lintegral, edist_zero_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) a) 0) fun (a : α) ↦
    edist ((↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a) 0
⊢ ∫⁻ (x : α), edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) x) 0 ∂μ =
    ∫⁻ (x : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x) 0 ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
h :
  ∀ (a : α) (ha : (↑(↑(f - g) : α →ₘ[μ] β) : α → β) a = ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) a),
    edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) a) 0 =
      edist ((↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) a) 0) fun (a : α) ↦
    edist ((↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a) 0

Tactic:
filter_upwards [Lp.coeFn_sub f g] with _ ha

Premises used: MeasureTheory.Lp.coeFn_sub
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a : α
ha : (↑(↑(f - g) : α →ₘ[μ] β) : α → β) a = ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) a
⊢ edist ((↑(↑(f - g) : α →ₘ[μ] β) : α → β) a) 0 =
    edist ((↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a) 0

Tactic:
simp only [ha, Pi.sub_apply]

Premises used: Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
hf : Integrable (↑(↑f : α →ₘ[μ] β) : α → β) μ
⊢ toL1 (↑(↑f : α →ₘ[μ] β) : α → β) hf = f

Tactic:
simp [Integrable.toL1]

Premises used: MeasureTheory.Integrable.toL1
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ (↑(↑(toL1 f hf) : α →ₘ[μ] β) : α → β) =ᶠ[ae μ] f

Tactic:
AEEqFun.coeFn_mk _ _

Premises used: MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
h : Integrable.{u_2, u_1} (ε := β) 0 μ
⊢ toL1 0 h = 0

Tactic:
rfl

Premises used: Set.Mem, MeasureTheory.MemLp.toLp, MeasureTheory.Integrable.toL1, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ (↑(toL1 f hf) : α →ₘ[μ] β) = AEEqFun.mk f ⋯

Tactic:
rfl

Premises used: rfl, MeasureTheory.AEEqFun.mk
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ toL1 f hf = toL1 g hg ↔ f =ᶠ[ae μ] g

Tactic:
MemLp.toLp_eq_toLp_iff _ _

Premises used: MeasureTheory.MemLp.toLp_eq_toLp_iff, MeasureTheory.Integrable.toL1
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ toL1 (f + g) ⋯ = toL1 f hf + toL1 g hg

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.comp₂, MeasureTheory.MemLp.toLp, MeasureTheory.Integrable.toL1, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ toL1 (-f) ⋯ = -toL1 f hf

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.MemLp.toLp, MeasureTheory.Integrable.toL1, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ toL1 (f - g) ⋯ = toL1 f hf - toL1 g hg

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.comp₂, MeasureTheory.MemLp.toLp, MeasureTheory.Integrable.toL1, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal

Tactic:
simp [toL1, Lp.norm_toLp, eLpNorm, eLpNorm'_eq_lintegral_enorm]

Premises used: MeasureTheory.Lp.norm_toLp, MeasureTheory.eLpNorm'_eq_lintegral_enorm, MeasureTheory.Integrable.toL1, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
simp : eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ
⊢ ‖toL1 f hf‖ₑ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp only [Lp.enorm_def, toL1_eq_mk, eLpNorm_aeeqFun]

Premises used: MeasureTheory.Integrable.toL1_eq_mk, MeasureTheory.Lp.enorm_def, MeasureTheory.eLpNorm_aeeqFun
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp [eLpNorm, eLpNorm']

Premises used: MeasureTheory.eLpNorm', MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
rw : (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
rw₁ rw₂ : (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
rw [norm_toL1, lintegral_norm_eq_lintegral_edist]

Premises used: MeasureTheory.Integrable.norm_toL1, MeasureTheory.lintegral_norm_eq_lintegral_edist
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
simp_rw : (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ).toReal

Tactic:
simp_rw [norm_toL1, edist_zero_right]

Premises used: MeasureTheory.Integrable.norm_toL1, edist_zero_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
simp :
  (if Eq (α := ℝ≥0∞) 1 ∞ then eLpNormEssSup (f - g) μ else ∫⁻ (a : α), ‖f a - g a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist (f a) (g a) ∂μ
⊢ edist (toL1 f hf) (toL1 g hg) = ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
simp only [toL1, Lp.edist_toLp_toLp, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm,
    Pi.sub_apply, toReal_one, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]

Premises used: ENNReal.toReal_one, ite_false, MeasureTheory.Lp.edist_toLp_toLp, ENNReal.rpow_one, ne_eq, MeasureTheory.eLpNorm'_eq_lintegral_enorm, MeasureTheory.Integrable.toL1, one_ne_zero, not_false_eq_true, div_self, Pi.sub_apply, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ (if Eq (α := ℝ≥0∞) 1 ∞ then eLpNormEssSup (f - g) μ else ∫⁻ (a : α), ‖f a - g a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
simp [edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
simp : eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ
⊢ edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
simp only [edist_zero_right, Lp.enorm_def, toL1_eq_mk, eLpNorm_aeeqFun]

Premises used: MeasureTheory.Integrable.toL1_eq_mk, edist_zero_right, MeasureTheory.Lp.enorm_def, MeasureTheory.eLpNorm_aeeqFun
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
apply eLpNorm_one_eq_lintegral_enorm

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_5
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
hf : Integrable f μ
k : 𝕜
⊢ toL1 (fun (a : α) ↦ k • f a) ⋯ = k • toL1 f hf

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.MemLp.toLp, MeasureTheory.Integrable.toL1, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_5
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
hf : Integrable f μ
k : 𝕜
⊢ toL1 (k • f) ⋯ = k • toL1 f hf

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.MemLp.toLp, MeasureTheory.Integrable.toL1, rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
simp only [edist_zero_right]

Premises used: edist_zero_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
simp only [ofReal_norm, edist_zero_right]

Premises used: edist_zero_right, ofReal_norm
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
rw : ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ

Tactic:
rw [← lintegral_add_left' (hf.edist hh)]

Premises used: MeasureTheory.lintegral_add_left', MeasureTheory.AEStronglyMeasurable.edist
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ

Tactic:
lintegral_mono fun a => ?_

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
refine : ∀ (a : α), edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ

Tactic:
refine lintegral_mono fun a => ?_

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
a : α
⊢ edist (f a) (g a) ≤ edist (f a) (h a) + edist (g a) (h a)

Tactic:
apply edist_triangle_right

Premises used: edist_triangle_right
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
⊢ ∫⁻ (x : α), enorm.{u_6} (E := ε'') 0 ∂μ = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
Goal:
α : Type u_1
ε' : Type u_5
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε'
inst_1 : TopologicalSpace ε''
inst_2 : ESeminormedAddMonoid ε''
f : α → ε''
hf : AEStronglyMeasurable f μ
g : α → ε'
⊢ ∫⁻ (a : α), ‖f a‖ₑ + ‖g a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖g a‖ₑ ∂μ

Tactic:
lintegral_add_left' hf.enorm _

Premises used: MeasureTheory.lintegral_add_left', MeasureTheory.AEStronglyMeasurable.enorm