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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
rw : setToFun μ T hT (f + -g) = setToFun μ T hT f - setToFun μ T hT g
rw₁ : setToFun μ T hT (f + -g) = setToFun μ T hT f + -setToFun μ T hT g
rw₂ : 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 - setToFun μ T hT g
have rw₃ : setToFun μ T hT f + -setToFun μ T hT g = setToFun μ T hT f + -setToFun μ T hT g
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, setToFun_add hT hf hg.neg, setToFun_neg hT g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos : ∀ (hF : CompleteSpace F), setToFun μ T hT (c • 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
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT (c • f) = c • setToFun μ T hT f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT (c • 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
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos : ∀ (hf : Integrable f μ), setToFun μ T hT (c • 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
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
pos : ∀ (hf : Integrable f μ), setToFun μ T hT (c • f) = c • setToFun μ T hT f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT (c • 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
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos : setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
      L1.setToL1_smul hT h_smul c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos :
  setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos₁ : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (c • f) sorry) =
  HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
      L1.setToL1_smul hT h_smul c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos :
  setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
pos₁ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (c • f) ⋯) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos₂ : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (c • Integrable.toL1 f hf) =
  HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
      L1.setToL1_smul hT h_smul c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
pos :
  setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
pos₁ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 (c • f) ⋯) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
pos₂ :
  (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (c • Integrable.toL1 f hf) =
    HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos₃ : HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F) =
  HSMul.hSMul (β := F) c ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hf) : F)
Tactic: rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
      L1.setToL1_smul hT h_smul c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos : ∀ (hr : c = 0), setToFun μ T hT (c • f) = c • setToFun μ T hT f
Tactic: by_cases hr : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
pos : ∀ (hr : c = 0), setToFun μ T hT (c • f) = c • setToFun μ T hT f
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have neg : ∀ (hr : ¬c = 0), setToFun μ T hT (c • f) = c • setToFun μ T hT f
Tactic: by_cases hr : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
hr : c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have pos : setToFun μ T hT (HSMul.hSMul (α := 𝕜) 0 f) = HSMul.hSMul.{u_6, u_3, u_3} (α := 𝕜) 0 (setToFun μ T hT f)
Tactic: rw [hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
hr : ¬c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have hf' : ¬Integrable (c • f) μ
Tactic: have hf' : ¬Integrable (c • f) μ := by rwa [integrable_smul_iff hr f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
hr : ¬c = 0
hf' : ¬Integrable (c • f) μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have neg : setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c 0
Tactic: rw [setToFun_undef hT hf, setToFun_undef hT 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
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
hr : ¬c = 0
hf' : ¬Integrable (c • f) μ
neg : setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have neg₁ : 0 = HSMul.hSMul (β := F) c 0
Tactic: rw [setToFun_undef hT hf, setToFun_undef hT 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
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : NormedDivisionRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : NormSMulClass 𝕜 E
inst_7 : Module 𝕜 F
inst_8 : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
hr : ¬c = 0
hf' : ¬Integrable (c • f) μ
neg : setToFun μ T hT (c • f) = HSMul.hSMul (β := F) c 0
neg₁ : 0 = HSMul.hSMul (β := F) c 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
have neg₂ : Eq.{u_3 + 1} (α := F) 0 0
Tactic: rw [setToFun_undef hT hf, setToFun_undef hT 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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
⊢ setToFun μ T hT f = setToFun μ T hT g
have pos : ∀ (hF : CompleteSpace F), 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
h : f =ᶠ[ae μ] g
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ T hT g
⊢ setToFun μ T hT f = setToFun μ T hT g
have neg : ∀ (hF : ¬CompleteSpace F), 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
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T hT g
have pos : ∀ (hfi : Integrable f μ), setToFun μ T hT f = setToFun μ T hT g
Tactic: by_cases hfi : 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 g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
pos : ∀ (hfi : Integrable f μ), setToFun μ T hT f = setToFun μ T hT g
⊢ setToFun μ T hT f = setToFun μ T hT g
have neg : ∀ (hfi : ¬Integrable f μ), setToFun μ T hT f = setToFun μ T hT g
Tactic: by_cases hfi : 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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T hT g
have hgi : Integrable g μ
Tactic: have hgi : Integrable g μ := hfi.congr 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 : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : Integrable f μ
hgi : Integrable g μ
⊢ setToFun μ T hT f = setToFun μ T hT g
have pos : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hfi) = setToFun μ T hT g
Tactic: rw [setToFun_eq hT hfi, setToFun_eq hT hgi, (Integrable.toL1_eq_toL1_iff f g hfi hgi).2 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 : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : Integrable f μ
hgi : Integrable g μ
pos : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hfi) = setToFun μ T hT g
⊢ setToFun μ T hT f = setToFun μ T hT g
have pos₁ : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hfi) : F)
  ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 g hgi) : F)
Tactic: rw [setToFun_eq hT hfi, setToFun_eq hT hgi, (Integrable.toL1_eq_toL1_iff f g hfi hgi).2 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 : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : Integrable f μ
hgi : Integrable g μ
pos : (L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hfi) = setToFun μ T hT g
pos₁ :
  Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 f hfi) : F)
    ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 g hgi) : F)
⊢ setToFun μ T hT f = setToFun μ T hT g
have pos₂ : Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 g hgi) : F)
  ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (Integrable.toL1 g hgi) : F)
Tactic: rw [setToFun_eq hT hfi, setToFun_eq hT hgi, (Integrable.toL1_eq_toL1_iff f g hfi hgi).2 h]
-- 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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T hT g
have hgi : ¬Integrable g μ
Tactic: have hgi : ¬Integrable g μ := by rw [integrable_congr h] at hfi; exact hfi
-- 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
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
hgi : ¬Integrable g μ
⊢ setToFun μ T hT f = setToFun μ T hT g
have neg : 0 = setToFun μ T hT g
Tactic: rw [setToFun_undef hT hfi, setToFun_undef hT hgi]
-- 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
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
hgi : ¬Integrable g μ
neg : 0 = setToFun μ T hT g
⊢ setToFun μ T hT f = setToFun μ T hT g
have neg₁ : Eq.{u_3 + 1} (α := F) 0 0
Tactic: rw [setToFun_undef hT hfi, setToFun_undef hT hgi]
-- 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
⊢ setToFun μ T hT f = 0
have this : f =ᶠ[ae μ] 0
Tactic: have : f =ᵐ[μ] 0 := by simp [h, EventuallyEq]
-- 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 : μ = 0
this : f =ᶠ[ae μ] 0
⊢ setToFun μ T hT f = 0
have rw : setToFun μ T hT 0 = 0
Tactic: rw [setToFun_congr_ae hT this, setToFun_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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
this : f =ᶠ[ae μ] 0
rw : setToFun μ T hT 0 = 0
⊢ setToFun μ T hT f = 0
have rw₁ : Eq.{u_3 + 1} (α := F) 0 0
Tactic: rw [setToFun_congr_ae hT this, setToFun_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 : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ setToFun μ T hT (s.indicator fun (x_1 : α) ↦ x) = (T s : (a : E) → F) x
have rw : setToFun μ T hT (↑(↑(indicatorConstLp (s := s) 1 hs hμs x) : α →ₘ[μ] E) : α → E) = (T s : (a : E) → F) x
Tactic: rw [setToFun_congr_ae hT (@indicatorConstLp_coeFn _ _ _ 1 _ _ _ hs hμs x).symm]