awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)
pos₁ : setToFun μ T hT f₂ + setToFun μ T hT g₂ = setToFun μ' T hT' f₂ + 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₂ + 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]
-- 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₂)
pos₁ : setToFun μ T hT f₂ + setToFun μ T hT g₂ = setToFun μ' T hT' f₂ + setToFun μ' T hT' g₂
pos₂ : setToFun μ' T hT' f₂ + setToFun μ T hT g₂ = setToFun μ' T hT' f₂ + 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₂ + 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]
-- 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 μ'
⊢ IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) | (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (↑(↑f : α →ₘ[μ] E) : α → E)}
have pos : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
  setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: refine isClosed_eq (continuous_setToFun hT) ?_
-- 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 μ'
⊢ Eq (α := (f : ↥(Lp E 1 μ)) → F) (fun (f : ↥(Lp E 1 μ)) ↦ setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E))
    fun (f : ↥(Lp E 1 μ)) ↦ setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : α →ₘ[μ'] E) : α → E)
have h : ∀ (f : ↥(Lp E 1 μ)),
  setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E) =
    setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) sorry) : α →ₘ[μ'] E) : α → E)
Tactic: ext1 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
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E)
have this : Eq (α := (f : ↥(Lp E 1 μ)) → F) (fun (f : ↥(Lp E 1 μ)) ↦ setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E))
  fun (f : ↥(Lp E 1 μ)) ↦ setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) sorry) : α →ₘ[μ'] E) : α → E)
Tactic: have :
      (fun f : α →₁[μ] E => setToFun μ' T hT' f) = fun f : α →₁[μ] E =>
        setToFun μ' T hT' ((h_int f (L1.integrable_coeFn f)).toL1 f) := by
      ext1 f; exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm
-- 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 μ'
this :
  Eq (α := (f : ↥(Lp E 1 μ)) → F) (fun (f : ↥(Lp E 1 μ)) ↦ setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E))
    fun (f : ↥(Lp E 1 μ)) ↦ setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : α →ₘ[μ'] E) : α → E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E)
have pos : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
  setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) sorry) : α →ₘ[μ'] E) : α → E)
Tactic: rw [this]
-- 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 μ'
f₂ g₂ : α → E
hfg : f₂ =ᶠ[ae μ] g₂
h : Integrable f₂ μ
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
have hfg' : f₂ =ᶠ[ae μ'] g₂
Tactic: have hfg' : f₂ =ᵐ[μ'] g₂ := (Measure.absolutelyContinuous_of_le_smul hμ'_le).ae_eq hfg
-- 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
hfg : f₂ =ᶠ[ae μ] g₂
h : Integrable f₂ μ
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
hfg' : f₂ =ᶠ[ae μ'] g₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
have pos : setToFun μ T hT f₂ = setToFun μ' T hT' g₂
Tactic: rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']
-- 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
hfg : f₂ =ᶠ[ae μ] g₂
h : Integrable f₂ μ
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
hfg' : f₂ =ᶠ[ae μ'] g₂
pos : setToFun μ T hT f₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
have pos₁ : setToFun μ' T hT' f₂ = setToFun μ' T hT' g₂
Tactic: rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']
-- 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
hfg : f₂ =ᶠ[ae μ] g₂
h : Integrable f₂ μ
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
hfg' : f₂ =ᶠ[ae μ'] g₂
pos : setToFun μ T hT f₂ = setToFun μ' T hT' g₂
pos₁ : setToFun μ' T hT' f₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
have pos₂ : setToFun μ' T hT' g₂ = setToFun μ' T hT' g₂
Tactic: rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']
-- 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 c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have pos : ∀ (hf : Integrable f μ), setToFun μ T hT f = setToFun μ' T hT' f
Tactic: by_cases hf : Integrable 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 c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
pos : ∀ (hf : Integrable f μ), setToFun μ T hT f = setToFun μ' T hT' f
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT f = setToFun μ' T hT' f
Tactic: by_cases hf : Integrable 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 c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ 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 h_int : ∀ (g : α → E), ¬Integrable g μ → ¬Integrable g μ'
Tactic: have h_int : ∀ g : α → E, ¬Integrable g μ → ¬Integrable g μ' := fun g =>
      mt fun h => h.of_measure_le_smul hc hμ_le
-- 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 c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f μ
h_int : ∀ (g : α → E), ¬Integrable g μ → ¬Integrable g μ'
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have neg : 0 = setToFun μ' T hT' f
Tactic: simp_rw [setToFun_undef _ hf, setToFun_undef _ (h_int f hf)]
-- 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 α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ T hT f
have refine : μ ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')
Tactic: refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf
-- 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 α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')
have rw : μ ≤ μ + μ'
Tactic: rw [one_smul]
-- 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 α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ ≤ μ + μ'
have nth_rw : μ + 0 ≤ μ + μ'
Tactic: nth_rw 1 [← add_zero μ]
-- 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 α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ' T hT f
have refine : μ' ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')
Tactic: refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf
-- 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 α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ' ≤ HSMul.hSMul (α := ℝ≥0∞) 1 (μ + μ')
have rw : μ' ≤ μ + μ'
Tactic: rw [one_smul]
-- 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0)
hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0)
⊢ setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f
have rw : setToFun μ T hTμ f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f
Tactic: rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f (hμ.add_measure hν),
        setToFun_congr_measure_of_add_left hTν_add hTν f (hμ.add_measure hν)]
-- 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0)
hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0)
rw : setToFun μ T hTμ f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f
⊢ setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f
have rw₁ : setToFun μ T hTμ f + setToFun ν T' hTν f = setToFun μ T hTμ f + setToFun ν T' hTν f
Tactic: rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f (hμ.add_measure hν),
        setToFun_congr_measure_of_add_left hTν_add hTν f (hμ.add_measure hν)]
-- 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 α
f : α → E
ι : Type u_7
s : Finset ι
hs : s.Nonempty
μ : ι → Measure α
T : ι → Set α → E →L[ℝ] F
C : ι → ℝ
hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
hf : ∀ i ∈ s, Integrable f (μ i)
⊢ setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, setToFun (μ i) (T i) ⋯ f
have singleton : ∀ (i : ι) (hf : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → Integrable f (μ i_1)),
  setToFun (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) sorry f = ∑ i ∈ {i}, setToFun (μ i) (T i) sorry f
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | @cons i s his hs' ih =>
    simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using
      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μ T C hTs)
      (hf i (Finset.mem_cons_self i s))
      (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))
Cleared hypotheses: hs, hf
-- 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 α
f : α → E
ι : Type u_7
s : Finset ι
hs : s.Nonempty
μ : ι → Measure α
T : ι → Set α → E →L[ℝ] F
C : ι → ℝ
hTs : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
hf : ∀ i ∈ s, Integrable f (μ i)
singleton :
  ∀ (i : ι) (hf : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → Integrable f (μ i_1)),
    setToFun (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) ⋯ f = ∑ i ∈ {i}, setToFun (μ i) (T i) ⋯ f
⊢ setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) ⋯ f = ∑ i ∈ s, setToFun (μ i) (T i) ⋯ f
have cons : ∀ (i : ι) (s : Finset ι) (his : i ∉ s) (hs' : s.Nonempty)
  (ih :
    ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
      setToFun (∑ i ∈ s, μ i) (∑ i ∈ s, T i) sorry f = ∑ i ∈ s, setToFun (μ i) (T i) sorry f)
  (hf : ∀ i_1 ∈ Finset.cons i s his, Integrable f (μ i_1)),
  setToFun (∑ i ∈ Finset.cons i s his, μ i) (∑ i ∈ Finset.cons i s his, T i) sorry f =
    ∑ i ∈ Finset.cons i s his, setToFun (μ i) (T i) sorry f
Tactic: induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | @cons i s his hs' ih =>
    simpa [his, ih fun j hj => hf j (Finset.mem_cons_of_mem hj)] using
      setToFun_add_measure (hTs i) (DominatedFinMeasAdditive.finsetSum_measure hs' μ T C hTs)
      (hf i (Finset.mem_cons_self i s))
      (integrable_finsetSum_measure.2 fun j hj => hf j (Finset.mem_cons_of_mem hj))
Cleared hypotheses: hs, hf
-- 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 : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
⊢ setToFun (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T hT f = 0
have refine : ∀ (s : Set α),
  MeasurableSet s →
    ∀ (hμs : LT.lt (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine setToFun_measure_zero' hT fun s _ hμs => ?_
-- 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 : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
s : Set α
h : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hμs₁ : Ne (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [lt_top_iff_ne_top] at hμs
Cleared hypotheses: hμs
-- 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 : ℝ
hT : DominatedFinMeasAdditive (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) T C
f : α → E
s : Set α
h : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hμs₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [true_and, Measure.smul_apply, ENNReal.mul_eq_top,
    top_ne_zero, Ne, not_false_iff, not_or, Classical.not_not, smul_eq_mul] at hμs
Cleared hypotheses: 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' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f
have pos : ∀ (hc0 : c = 0), setToFun μ T hT f = setToFun (c • μ) T hT_smul f
Tactic: by_cases hc0 : c = 0
-- 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' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
pos : ∀ (hc0 : c = 0), setToFun μ T hT f = setToFun (c • μ) T hT_smul f
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f
have neg : ∀ (hc0 : ¬c = 0), setToFun μ T hT f = setToFun (c • μ) T hT_smul f
Tactic: by_cases hc0 : c = 0
-- 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' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f
have hT_smul₁ : @DominatedFinMeasAdditive _ _ _ m 0 T C'
Tactic: simp [hc0] at hT_smul