awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
pos :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (s.indicator fun (x : α) ↦ c)
pos₁ :
  ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f →
            (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g →
              (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (f + g)
pos₂ :
  IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) | (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (↑(↑f : α →ₘ[μ] E) : α → E)}
pos₃ :
  ∀ ⦃f g : α → E⦄,
    f =ᶠ[ae μ] g →
      Integrable f μ →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f →
          (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)

Premises used: Eq, MeasureTheory.Integrable.induction, 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
((hμ'_le s).trans_lt ?_).ne

Premises used: LE.le.trans_lt, LT.lt.ne
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : LT.lt (α := ℝ≥0∞) ((c' • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine ((hμ'_le s).trans_lt ?_).ne

Premises used: LE.le.trans_lt, LT.lt.ne
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((c' • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.smul_apply, smul_eq_mul]

Premises used: MeasureTheory.Measure.smul_apply, smul_eq_mul
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < ∞

Tactic:
ENNReal.mul_lt_top hc'.lt_top hμs

Premises used: ENNReal.mul_lt_top, Ne.lt_top
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.mul_lt_top hc'.lt_top hμs

Premises used: ENNReal.mul_lt_top, Ne.lt_top
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hμ's : μ' s ≠ ∞ := by
      refine ((hμ'_le s).trans_lt ?_).ne
      rw [Measure.smul_apply, smul_eq_mul]
      exact ENNReal.mul_lt_top hc'.lt_top hμs
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ's : Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : (T s : (a : E) → F) c = setToFun μ' T hT' (s.indicator fun (x : α) ↦ c)
pos₁ pos₂ : Eq.{u_3 + 1} (α := F) ((T s : (a : E) → F) c : F) ((T s : (a : E) → F) c : F)
⊢ setToFun μ T hT (s.indicator fun (x : α) ↦ c) = setToFun μ' T hT' (s.indicator fun (x : α) ↦ c)

Tactic:
rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's]

Premises used: MeasureTheory.setToFun_indicator_const, LT.lt.ne
-- 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 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
pos :
  Disjoint (Function.support f₂) (Function.support g₂) →
    Integrable f₂ μ →
      Integrable g₂ μ →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f₂ →
          (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g₂ →
            (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (f₂ + g₂)
⊢ Disjoint (Function.support f₂) (Function.support g₂) →
    Integrable f₂ μ →
      Integrable g₂ μ →
        (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f₂ →
          (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g₂ →
            (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (f₂ + g₂)

Tactic:
_
-- 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 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₂
pos₃ 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₂)

Tactic:
rw [setToFun_add hT hf₂ hg₂, setToFun_add hT' (h_int f₂ hf₂) (h_int g₂ hg₂), h_eq_f, h_eq_g]

Premises used: MeasureTheory.setToFun_add
-- 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 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)}

Tactic:
isClosed_eq (continuous_setToFun hT) ?_

Premises used: MeasureTheory.continuous_setToFun, setOf, isClosed_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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
pos :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ IsClosed (X := ↥(Lp E 1 μ))
    {f : ↥(Lp E 1 μ) | (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) (↑(↑f : α →ₘ[μ] E) : α → E)}

Tactic:
refine isClosed_eq (continuous_setToFun hT) ?_

Premises used: MeasureTheory.continuous_setToFun, isClosed_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 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 μ'
h :
  ∀ (f : ↥(Lp E 1 μ)),
    setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E) =
      setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : α →ₘ[μ'] E) : α → E)
⊢ 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)

Tactic:
ext1 f
-- 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f_1 : α → E
hfμ : Integrable f_1 μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f : ↥(Lp E 1 μ)
⊢ setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E) =
    setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : α →ₘ[μ'] E) : α → E)

Tactic:
setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm

Premises used: MeasureTheory.setToFun_congr_ae, MeasureTheory.Integrable.coeFn_toL1, 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f_1 : α → E
hfμ : Integrable f_1 μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f : ↥(Lp E 1 μ)
⊢ setToFun μ' T hT' (↑(↑f : α →ₘ[μ] E) : α → E) =
    setToFun μ' T hT' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : α →ₘ[μ'] E) : α → E)

Tactic:
exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm

Premises used: MeasureTheory.setToFun_congr_ae, MeasureTheory.Integrable.coeFn_toL1, 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 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)

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
-- 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 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)
pos :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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)

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 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' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : α →ₘ[μ'] E) : α → E)

Tactic:
(continuous_setToFun hT').comp (continuous_L1_toL1 c' hc' hμ'_le)

Premises used: MeasureTheory.continuous_setToFun, Continuous.comp, dite, MeasureTheory.setToFun, MeasureTheory.continuous_L1_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 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' (↑(↑(Integrable.toL1 (↑(↑f : α →ₘ[μ] E) : α → E) ⋯) : α →ₘ[μ'] E) : α → E)

Tactic:
exact (continuous_setToFun hT').comp (continuous_L1_toL1 c' hc' hμ'_le)

Premises used: MeasureTheory.continuous_setToFun, Continuous.comp, MeasureTheory.continuous_L1_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 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₂
pos :
  Integrable f₂ μ →
    (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f₂ →
      (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g₂
⊢ Integrable f₂ μ →
    (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) f₂ →
      (fun (f : α → E) ↦ setToFun μ T hT f = setToFun μ' T hT' f) g₂

Tactic:
_
-- 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 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₂
⊢ f₂ =ᶠ[ae μ'] g₂

Tactic:
have hfg' : f₂ =ᵐ[μ'] g₂ := (Measure.absolutelyContinuous_of_le_smul hμ'_le).ae_eq hfg
-- 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 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₂
pos₂ pos₃ : setToFun μ' T hT' g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂

Tactic:
rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']

Premises used: 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 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
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
-- 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 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

Tactic:
setToFun_congr_measure_of_integrable c' hc' hμ'_le hT hT' f hf

Premises used: MeasureTheory.setToFun_congr_measure_of_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 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

Tactic:
exact setToFun_congr_measure_of_integrable c' hc' hμ'_le hT hT' f hf

Premises used: MeasureTheory.setToFun_congr_measure_of_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 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 μ
⊢ ∀ (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