awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
⊢ eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'

Tactic:
have :
    eLpNorm (⇑(Integrable.toL1 g (h_int g)) - ⇑(Integrable.toL1 f (h_int f))) 1 μ' =
      eLpNorm (⇑g - ⇑f) 1 μ' :=
    eLpNorm_congr_ae ((Integrable.coeFn_toL1 _).sub (Integrable.coeFn_toL1 _))
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal < ε
⊢ (eLpNorm
        ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
          (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
        1 μ').toReal <
    ε

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
rw : eLpNorm (↑(↑(g - f) : α →ₘ[μ] G) : α → G) 1 μ ≠ ∞
⊢ eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞

Tactic:
rw [← eLpNorm_congr_ae (Lp.coeFn_sub _ _)]

Premises used: MeasureTheory.Lp.coeFn_sub, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
⊢ eLpNorm (↑(↑(g - f) : α →ₘ[μ] G) : α → G) 1 μ ≠ ∞

Tactic:
Lp.eLpNorm_ne_top _

Premises used: MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
⊢ eLpNorm (↑(↑(g - f) : α →ₘ[μ] G) : α → G) 1 μ ≠ ∞

Tactic:
exact Lp.eLpNorm_ne_top _

Premises used: MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
⊢ eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞

Tactic:
have h_eLpNorm_ne_top : eLpNorm (⇑g - ⇑f) 1 μ ≠ ∞ := by
    rw [← eLpNorm_congr_ae (Lp.coeFn_sub _ _)]; exact Lp.eLpNorm_ne_top _
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal ≤
    (c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal

Tactic:
toReal_mono (ENNReal.mul_ne_top hc' h_eLpNorm_ne_top) ?_

Premises used: ENNReal.mul_ne_top, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
refine :
  eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ' ≤
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
⊢ (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal ≤
    (c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal

Tactic:
refine toReal_mono (ENNReal.mul_ne_top hc' h_eLpNorm_ne_top) ?_

Premises used: ENNReal.mul_ne_top, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ' ≤
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ

Tactic:
(eLpNorm_mono_measure (⇑g - ⇑f) hμ'_le).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.AEEqFun.cast, HSub.hSub, MeasureTheory.eLpNorm_mono_measure, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
refine :
  eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 (c' • μ) =
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
⊢ eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ' ≤
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ

Tactic:
refine (eLpNorm_mono_measure (⇑g - ⇑f) hμ'_le).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.AEEqFun.cast, HSub.hSub, MeasureTheory.eLpNorm_mono_measure, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
rw :
  c' ^ (1 / 1).toReal * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ =
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
⊢ eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 (c' • μ) =
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ

Tactic:
rw [eLpNorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]

Premises used: smul_eq_mul, MeasureTheory.eLpNorm_smul_measure_of_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ c' ^ (1 / 1).toReal * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ =
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ (c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal =
    c'.toReal * (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal

Tactic:
toReal_mul

Premises used: ENNReal.toReal_mul
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
ha : 0 ≤ c'.toReal
⊢ c'.toReal * (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal ≤
    c'.toReal * (ε / 2 / c'.toReal)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ c'.toReal * (ε / 2 / c'.toReal) = ε / 2

Tactic:
mul_div_cancel₀ (ε / 2) ?_

Premises used: HDiv.hDiv, mul_div_cancel₀, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
refine : c'.toReal ≠ 0
⊢ c'.toReal * (ε / 2 / c'.toReal) = ε / 2

Tactic:
refine mul_div_cancel₀ (ε / 2) ?_

Premises used: HDiv.hDiv, mul_div_cancel₀, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
rw : ¬(c' = 0 ∨ c' = ∞)
⊢ c'.toReal ≠ 0

Tactic:
rw [Ne, toReal_eq_zero_iff]

Premises used: Ne, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ ¬(c' = 0 ∨ c' = ∞)

Tactic:
simp [hc', hc'0]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
⊢ ε / 2 < ε

Tactic:
half_lt_self hε_pos

Premises used: half_lt_self
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑(↑f' : α →ₘ[μ] G) : α → G) μ' := ⋯
this :
  MeasureTheory.eLpNorm
      ((↑(↑(Integrable.toL1 (↑(↑g : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G) -
        (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ'] G) : α → G))
      1 μ' =
    MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ'
h_eLpNorm_ne_top : MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ ≠ ∞
eLpNorm :
  (MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal ≤
    (c' * MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal
eLpNorm₁ :
  c'.toReal * (MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal ≤
    c'.toReal * (ε / 2 / c'.toReal)
eLpNorm₂ : c'.toReal * (ε / 2 / c'.toReal) = ε / 2
⊢ (MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal < ε

Tactic:
calc
    (eLpNorm (⇑g - ⇑f) 1 μ').toReal ≤ (c' * eLpNorm (⇑g - ⇑f) 1 μ).toReal := by
      refine toReal_mono (ENNReal.mul_ne_top hc' h_eLpNorm_ne_top) ?_
      refine (eLpNorm_mono_measure (⇑g - ⇑f) hμ'_le).trans_eq ?_
      rw [eLpNorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
      simp
    _ = c'.toReal * (eLpNorm (⇑g - ⇑f) 1 μ).toReal := toReal_mul
    _ ≤ c'.toReal * (ε / 2 / c'.toReal) := by gcongr
    _ = ε / 2 := by
      refine mul_div_cancel₀ (ε / 2) ?_; rw [Ne, toReal_eq_zero_iff]; simp [hc', hc'0]
    _ < ε := half_lt_self hε_pos

Premises used: half_lt_self, HMul.hMul, MeasureTheory.AEEqFun.cast, HSub.hSub, HDiv.hDiv, ENNReal.toReal, ENNReal.toReal_mul, OfNat.ofNat, Subtype.val, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ' T hT' f
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = setToFun μ' T hT' f
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
simp [setToFun, hF]

Premises used: MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
⊢ ∀ (g : α → E), Integrable g μ → Integrable g μ'

Tactic:
have h_int : ∀ g : α → E, Integrable g μ → Integrable g μ' := fun g hg =>
    Integrable.of_measure_le_smul hc' hμ'_le hg