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 T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T'' hT'' f = setToFun μ T hT 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 + 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 T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f
have pos : ∀ (hf : Integrable f μ), setToFun μ T'' hT'' 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 T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T'' hT'' f = setToFun μ T hT 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 + 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 T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f
have pos : (L1.setToL1 hT'' : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) =
  HAdd.hAdd (α := F) (β := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
    ((L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: simp_rw [setToFun_eq _ hf, L1.setToL1_add_left' hT hT' hT'' h_add]
-- 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' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f
have neg : 0 = HAdd.hAdd (α := F) 0 0
Tactic: simp_rw [setToFun_undef _ hf, 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
have pos : ∀ (hF : CompleteSpace F), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) sorry f = c • 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) sorry f = c • 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
have pos : ∀ (hf : Integrable f μ), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) sorry f = c • 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) sorry f = c • 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
have pos : (L1.setToL1 (T := fun (s : Set α) ↦ c • T s) (C := ‖c‖ * C) sorry : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) =
  HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left hT c]
-- 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 μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ fun (s : Set α) ↦ c • T s (C := ‖c‖ * C) ⋯ f = c • setToFun μ T hT f
have neg : 0 = HSMul.hSMul (β := F) c 0
Tactic: simp_rw [setToFun_undef _ hf, smul_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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f
have pos : ∀ (hF : CompleteSpace F), setToFun μ T' hT' f = c • 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T' hT' f = c • setToFun μ T hT f
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T' hT' f = c • 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : CompleteSpace F
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f
have pos : ∀ (hf : Integrable f μ), setToFun μ T' hT' f = c • 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T' hT' f = c • setToFun μ T hT f
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ T' hT' f = c • 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f
have pos : (L1.setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) =
  HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left' hT hT' c h_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' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f
have neg : 0 = HSMul.hSMul (β := F) c 0
Tactic: simp_rw [setToFun_undef _ hf, smul_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 : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ setToFun μ T hT 0 = 0
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT 0 = 0
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 : ℝ
hT : DominatedFinMeasAdditive μ T C
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT 0 = 0
⊢ setToFun μ T hT 0 = 0
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT 0 = 0
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 : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ setToFun μ T hT 0 = 0
have pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fun (x : α) ↦ 0) sorry) : F) (0 : F)
Tactic: rw [Pi.zero_def, setToFun_eq hT (integrable_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 : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (fun (x : α) ↦ 0) ⋯) : F) (0 : F)
have pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 0 sorry) : F) (0 : F)
Tactic: simp only [← Pi.zero_def]
-- 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 μ T C
hF : CompleteSpace F
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 0 ⋯) : F) (0 : F)
have pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) 0 : F) (0 : F)
Tactic: rw [Integrable.toL1_zero, map_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 : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) 0 : F) (0 : F)
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 0 ⋯) : F) (0 : F)
have pos₁ : Eq.{u_3 + 1} (α := F) 0 0
Tactic: rw [Integrable.toL1_zero, map_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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
⊢ setToFun μ 0 hT f = 0
have pos : ∀ (hF : CompleteSpace F), setToFun μ 0 hT f = 0
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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
pos : ∀ (hF : CompleteSpace F), setToFun μ 0 hT f = 0
⊢ setToFun μ 0 hT f = 0
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ 0 hT f = 0
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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
⊢ setToFun μ 0 hT f = 0
have pos : ∀ (hf : Integrable f μ), setToFun μ 0 hT f = 0
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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ 0 hT f = 0
⊢ setToFun μ 0 hT f = 0
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ 0 hT f = 0
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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ 0 hT f = 0
have pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (0 : F)
Tactic: rw [setToFun_eq hT 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
⊢ setToFun μ T hT f = 0
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = 0
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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = 0
⊢ setToFun μ T hT f = 0
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = 0
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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
⊢ setToFun μ T hT f = 0
have pos : ∀ (hf : Integrable f μ), setToFun μ T hT f = 0
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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T hT f = 0
⊢ setToFun μ T hT f = 0
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT f = 0
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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T hT f = 0
have pos : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (0 : F)
Tactic: rw [setToFun_eq hT 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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
have pos : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (f + g) sorry) = setToFun μ T hT f + setToFun μ T hT g
Tactic: rw [setToFun_eq hT (hf.add hg), setToFun_eq hT hf, setToFun_eq hT hg, Integrable.toL1_add,
    (L1.setToL1 hT).map_add]
-- 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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
pos : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (f + g) ⋯) = setToFun μ T hT f + setToFun μ T hT g
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g
have pos₁ : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (f + g) sorry) =
  HAdd.hAdd (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) (setToFun μ T hT g)
Tactic: rw [setToFun_eq hT (hf.add hg), setToFun_eq hT hf, setToFun_eq hT hg, Integrable.toL1_add,
    (L1.setToL1 hT).map_add]