awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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 (HSMul.hSMul (α := 𝕜) 0 f) = HSMul.hSMul.{u_6, u_3, u_3} (α := 𝕜) 0 (setToFun μ T hT f)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
rwa rwa₁ rwa₂ rwa₃ : ¬Integrable f μ
⊢ ¬Integrable (c • f) μ

Tactic:
rwa [integrable_smul_iff hr f]

Premises used: MeasureTheory.integrable_smul_iff
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
⊢ ¬Integrable (c • f) μ

Tactic:
have hf' : ¬Integrable (c • f) μ := by rwa [integrable_smul_iff hr f]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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
neg₂ neg₃ : Eq.{u_3 + 1} (α := F) 0 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
rw [setToFun_undef hT hf, setToFun_undef hT hf', smul_zero]

Premises used: MeasureTheory.setToFun_undef, smul_zero
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
pos : ∀ (hF : CompleteSpace F), setToFun μ T hT f = setToFun μ T hT g
neg : ∀ (hF : ¬CompleteSpace F), setToFun μ T hT f = setToFun μ T hT g
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
by_cases hF : CompleteSpace F

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
simp [setToFun, hF]

Premises used: MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
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
neg : ∀ (hfi : ¬Integrable f μ), setToFun μ T hT f = setToFun μ T hT g
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : Integrable f μ
⊢ Integrable g μ

Tactic:
have hgi : Integrable g μ := hfi.congr h
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
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)
pos₂ 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)
⊢ setToFun μ T hT f = 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]

Premises used: Iff.mpr, MeasureTheory.Integrable.toL1_eq_toL1_iff, MeasureTheory.setToFun_eq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
⊢ ¬Integrable g μ

Tactic:
rw [integrable_congr h] at hfi

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : ¬Integrable g μ
⊢ ¬Integrable g μ

Tactic:
hfi
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : ¬Integrable g μ
⊢ ¬Integrable g μ

Tactic:
exact hfi
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᶠ[ae μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
⊢ ¬Integrable g μ

Tactic:
have hgi : ¬Integrable g μ := by rw [integrable_congr h] at hfi; exact hfi
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
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
neg₁ neg₂ : Eq.{u_3 + 1} (α := F) 0 0
⊢ setToFun μ T hT f = setToFun μ T hT g

Tactic:
rw [setToFun_undef hT hfi, setToFun_undef hT hgi]

Premises used: MeasureTheory.setToFun_undef
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
simp [h, EventuallyEq]

Premises used: Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
have : f =ᵐ[μ] 0 := by simp [h, EventuallyEq]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
this : f =ᶠ[ae μ] 0
rw : setToFun μ T hT 0 = 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := F) 0 0
⊢ setToFun μ T hT f = 0

Tactic:
rw [setToFun_congr_ae hT this, setToFun_zero]

Premises used: MeasureTheory.setToFun_congr_ae, MeasureTheory.setToFun_zero
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ setToFun μ T hT f = 0

Tactic:
setToFun_zero_left' hT fun s hs hμs => hT.eq_zero_of_measure_zero hs (h s hs hμs)

Premises used: MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, MeasureTheory.setToFun_zero_left'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
⊢ setToFun μ T hT (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] E) : α → E) = setToFun μ T hT f

Tactic:
setToFun_congr_ae hT hf.coeFn_toL1

Premises used: MeasureTheory.setToFun_congr_ae, MeasureTheory.Integrable.coeFn_toL1
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
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
rw : setToFun μ T hT (↑(↑(indicatorConstLp (s := s) 1 hs hμs x) : α →ₘ[μ] E) : α → E) = (T s : (a : E) → F) x
⊢ setToFun μ T hT (s.indicator fun (x_1 : α) ↦ x) = (T s : (a : E) → F) x

Tactic:
rw [setToFun_congr_ae hT (@indicatorConstLp_coeFn _ _ _ 1 _ _ _ hs hμs x).symm]

Premises used: MeasureTheory.setToFun_congr_ae, MeasureTheory.indicatorConstLp_coeFn, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
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
rw :
  Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (indicatorConstLp (s := s) 1 hs hμs x) : F)
    ((T s : (a : E) → F) x : F)
⊢ setToFun μ T hT (↑(↑(indicatorConstLp (s := s) 1 hs hμs x) : α →ₘ[μ] E) : α → E) = (T s : (a : E) → F) x

Tactic:
rw [L1.setToFun_eq_setToL1 hT]

Premises used: MeasureTheory.L1.setToFun_eq_setToL1
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
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
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (indicatorConstLp (s := s) 1 hs hμs x) : F)
    ((T s : (a : E) → F) x : F)

Tactic:
L1.setToL1_indicatorConstLp hT hs hμs x

Premises used: MeasureTheory.L1.setToL1_indicatorConstLp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
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
⊢ Eq.{u_3 + 1} (α := F) ((L1.setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (indicatorConstLp (s := s) 1 hs hμs x) : F)
    ((T s : (a : E) → F) x : F)

Tactic:
exact L1.setToL1_indicatorConstLp hT hs hμs x

Premises used: MeasureTheory.L1.setToL1_indicatorConstLp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
inst_5 : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
⊢ Eq (α := α → E) (fun (x_1 : α) ↦ x) (indicator univ fun (x_1 : α) ↦ x)

Tactic:
have : (fun _ : α => x) = Set.indicator univ fun _ => x := (indicator_univ _).symm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
inst_5 : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : Eq (α := α → E) (fun (x_1 : α) ↦ x) (indicator univ fun (x_1 : α) ↦ x)
rw : setToFun μ T hT (indicator univ fun (x_1 : α) ↦ x) = (T univ : (a : E) → F) x
⊢ (setToFun μ T hT fun (x_1 : α) ↦ x) = (T univ : (a : E) → F) x

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
inst_5 : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : Eq (α := α → E) (fun (x_1 : α) ↦ x) (indicator univ fun (x_1 : α) ↦ x)
⊢ setToFun μ T hT (indicator univ fun (x_1 : α) ↦ x) = (T univ : (a : E) → F) x

Tactic:
setToFun_indicator_const hT MeasurableSet.univ (measure_ne_top _ _) x

Premises used: MeasureTheory.measure_ne_top, MeasureTheory.setToFun_indicator_const, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
inst_5 : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : Eq (α := α → E) (fun (x_1 : α) ↦ x) (indicator univ fun (x_1 : α) ↦ x)
⊢ setToFun μ T hT (indicator univ fun (x_1 : α) ↦ x) = (T univ : (a : E) → F) x

Tactic:
exact setToFun_indicator_const hT MeasurableSet.univ (measure_ne_top _ _) x

Premises used: MeasureTheory.measure_ne_top, MeasureTheory.setToFun_indicator_const, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ

Tactic:
have h'f : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
⊢ (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)

Tactic:
have A : f =ᵐ[μ] g := h'f.coeFn_toLp.symm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
rw :
  Eq.{u_3 + 1} (α := F) ((L1.SimpleFunc.setToL1SCLM α E μ hT : (a : ↥(Lp.simpleFunc E 1 μ)) → F) g : F)
    (∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)
⊢ setToFun μ T hT (⇑f : (a : α) → E) = ∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x

Tactic:
rw [setToFun_congr_ae hT A, L1.setToFun_eq_setToL1 hT, L1.setToL1_eq_setToL1SCLM]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.L1.setToFun_eq_setToL1, MeasureTheory.setToFun_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
apply : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)
⊢ Eq.{u_3 + 1} (α := F) ((L1.SimpleFunc.setToL1SCLM α E μ hT : (a : ↥(Lp.simpleFunc E 1 μ)) → F) g : F)
    (∑ x ∈ f.range, (T (preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F) x : F)

Tactic:
apply (SimpleFunc.setToSimpleFunc_congr T (fun s ↦ hT.eq_zero_of_measure_zero) hT.1 hf _).symm

Premises used: MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, And.left, MeasureTheory.SimpleFunc.setToSimpleFunc_congr, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst_4 : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
f : SimpleFunc α E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
h'f : MemLp.{u_1, u_2} (ε := E) (⇑f : (a : α) → E) 1 μ
g : ↥(Lp.simpleFunc E 1 μ) := f.toLp h'f
A : (⇑f : (a : α) → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
grw : (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)
grw₁ grw₂ : (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(↑g : ↥(Lp E 1 μ)) : α →ₘ[μ] E) : α → E)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑(Lp.simpleFunc.toSimpleFunc g) : (a : α) → E)

Tactic:
grw [A, Lp.simpleFunc.toSimpleFunc_eq_toFun]

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
inst_6 : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E), LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : α → E
pos : ∀ (hG'' : CompleteSpace G''), setToFun μ T hT f ≤ setToFun μ T' hT' f
neg : ∀ (hG'' : ¬CompleteSpace G''), setToFun μ T hT f ≤ setToFun μ T' hT' f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

Tactic:
by_cases hG'' : CompleteSpace G''

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
inst_6 : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E), LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : α → E
hG'' : ¬CompleteSpace G''
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

Tactic:
simp [setToFun, hG'']

Premises used: MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst_2 : NormedAddCommGroup G''
inst_3 : PartialOrder G''
inst_4 : IsOrderedAddMonoid G''
inst_5 : NormedSpace ℝ G''
inst_6 : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : E), LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') x : G'') ((T' s : (a : E) → G'') x : G'')
f : α → E
hG'' : CompleteSpace G''
pos : ∀ (hf : Integrable f μ), setToFun μ T hT f ≤ setToFun μ T' hT' f
neg : ∀ (hf : ¬Integrable f μ), setToFun μ T hT f ≤ setToFun μ T' hT' f
⊢ setToFun μ T hT f ≤ setToFun μ T' hT' f

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable