awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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' • μ) =
    c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
have rw : c' ^ (1 / 1).toReal * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ =
  c' * eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ
Tactic: rw [eLpNorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 * (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal ≤
    c'.toReal * (ε / 2 / c'.toReal)
have ha : 0 ≤ c'.toReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
have refine : c'.toReal ≠ 0
Tactic: refine mul_div_cancel₀ (ε / 2) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 ≠ 0
have rw : ¬(c' = 0 ∨ c' = ∞)
Tactic: rw [Ne, toReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 < ε
have eLpNorm : (eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal ≤
  (c' * 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ (MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal < ε
have eLpNorm₁ : c'.toReal * (MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ).toReal ≤
  c'.toReal * (ε / 2 / c'.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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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)
⊢ (MeasureTheory.eLpNorm ((↑(↑g : α →ₘ[μ] G) : α → G) - (↑(↑f : α →ₘ[μ] G) : α → G)) 1 μ').toReal < ε
have eLpNorm₂ : c'.toReal * (ε / 2 / c'.toReal) = ε / 2
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 μ
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ' T hT' f
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = setToFun μ' T hT' f
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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
have h_int : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have pos : ∀ (c : E) ⦃s : Set α⦄,
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (s.indicator fun (x : α) ↦ c)
Tactic: apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
pos :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (s.indicator fun (x : α) ↦ c)
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have pos₁ : ∀ ⦃f g : α → E⦄,
  Disjoint (Function.support f) (Function.support g) →
    Integrable f μ →
      Integrable g μ →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f →
          (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g →
            (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (f + g)
Tactic: apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
pos :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (s.indicator fun (x : α) ↦ c)
pos₁ :
  ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f →
            (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g →
              (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (f + g)
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have pos₂ : IsClosed (X := ↥(Lp E 1 μ))
  {f : ↥(Lp E 1 μ) | (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (↑(↑f : α →ₘ[μ] E) : α → E)}
Tactic: apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
pos :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (s.indicator fun (x : α) ↦ c)
pos₁ :
  ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f →
            (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g →
              (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (f + g)
pos₂ :
  IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) | (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (↑(↑f : α →ₘ[μ] E) : α → E)}
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have pos₃ : ∀ ⦃f g : α → E⦄,
  f =ᶠ[ae μ] g →
    Integrable f μ →
      (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g
Tactic: apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : LT.lt (α := ℝ≥0∞) ((c' • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ((hμ'_le s).trans_lt ?_).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((c' • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < ∞
Tactic: rw [Measure.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ setToFun μ T hT (s.indicator fun (x : α) ↦ c) = setToFun μ' T hT' (s.indicator fun (x : α) ↦ c)
have hμ's : Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμ's : μ' s ≠ ∞ := by
      refine ((hμ'_le s).trans_lt ?_).ne
      rw [Measure.smul_apply, smul_eq_mul]
      exact ENNReal.mul_lt_top hc'.lt_top hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ's : Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ setToFun μ T hT (s.indicator fun (x : α) ↦ c) = setToFun μ' T hT' (s.indicator fun (x : α) ↦ c)
have pos : (T s : (a : E) → F) c = setToFun μ' T hT' (s.indicator fun (x : α) ↦ c)
Tactic: rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ's : Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : (T s : (a : E) → F) c = setToFun μ' T hT' (s.indicator fun (x : α) ↦ c)
⊢ setToFun μ T hT (s.indicator fun (x : α) ↦ c) = setToFun μ' T hT' (s.indicator fun (x : α) ↦ c)
have pos₁ : Eq.{u_3 + 1} (α := F) ((T s : (a : E) → F) c : F) ((T s : (a : E) → F) c : F)
Tactic: rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
h : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
have pos : setToFun μ T hT f₂ + setToFun μ T hT g₂ = setToFun μ' T hT' (f₂ + g₂)
Tactic: rw [setToFun_add hT hf₂ hg₂, setToFun_add hT' (h_int f₂ hf₂) (h_int g₂ hg₂), h_eq_f, h_eq_g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
h : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
pos : setToFun μ T hT f₂ + setToFun μ T hT g₂ = setToFun μ' T hT' (f₂ + g₂)
⊢ setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
have pos₁ : setToFun μ T hT f₂ + setToFun μ T hT g₂ = setToFun μ' T hT' f₂ + setToFun μ' T hT' g₂
Tactic: rw [setToFun_add hT hf₂ hg₂, setToFun_add hT' (h_int f₂ hf₂) (h_int g₂ hg₂), h_eq_f, h_eq_g]