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
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : IsBoundedSMul 𝕜 E
inst_7 : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
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 : ↥(simpleFunc E 1 μ)
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (c • f)) = SimpleFunc.setToSimpleFunc T (c • toSimpleFunc f)
have refine : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (c • f)) : (a : α) → E) (⇑(c • toSimpleFunc f) : (a : α) → E)
Tactic: refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_
-- 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_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : ↥(simpleFunc E 1 μ)
⊢ ‖setToL1S T f‖ ≤ C * ‖f‖
have rw : ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
  C * ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := E) (⇑(toSimpleFunc f) : (a : α) → E) {x}) * ‖x‖
Tactic: rw [setToL1S, norm_eq_sum_mul 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ setToL1S T (indicatorConst 1 (s := s) hs ⋯ x) = (T s : (a : E) → F) x
have h_empty : T ∅ = 0
Tactic: have h_empty : T ∅ = 0 := h_zero _ MeasurableSet.empty measure_empty
-- 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) = (T s : (a : E) → F) x
have refine : SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs sorry x)) =
  SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))
Tactic: refine Eq.trans ?_ (SimpleFunc.setToSimpleFunc_indicator T h_empty hs x)
-- 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
s : Set α
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_empty : T ∅ = 0
⊢ SimpleFunc.setToSimpleFunc T (toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs ⋯ x)) =
    SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))
have refine : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑(toSimpleFunc (p := 1) (indicatorConst 1 (s := s) hs sorry x)) : (a : α) → E)
  (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0)) : (a : α) → E)
Tactic: refine SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst : NormedAddCommGroup G'
inst_1 : PartialOrder G'
inst_2 : IsOrderedAddMonoid G'
inst_3 : NormedSpace ℝ G'
inst_4 : NormedAddCommGroup G''
inst_5 : PartialOrder G''
inst_6 : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G''), 0 ≤ x → LE.le.{u_8} (α := G') (0 : G') ((T s : (a : G'') → G') x : G')
f : ↥(simpleFunc G'' 1 μ)
hf : 0 ≤ f
⊢ 0 ≤ setToL1S T f
have simp_rw : 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
Tactic: simp_rw [setToL1S]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst : NormedAddCommGroup G'
inst_1 : PartialOrder G'
inst_2 : IsOrderedAddMonoid G'
inst_3 : NormedSpace ℝ G'
inst_4 : NormedAddCommGroup G''
inst_5 : PartialOrder G''
inst_6 : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G''), 0 ≤ x → LE.le.{u_8} (α := G') (0 : G') ((T s : (a : G'') → G') x : G')
f : ↥(simpleFunc G'' 1 μ)
hf : 0 ≤ f
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have obtain : ∀ (f' : SimpleFunc α G'') (hf' : 0 ≤ f')
  (hff' : (↑(↑(↑f : ↥(Lp G'' 1 μ)) : α →ₘ[μ] G'') : α → G'') =ᶠ[ae μ] (⇑f' : (a : α) → G'')),
  0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
Tactic: obtain ⟨f', hf', hff'⟩ := exists_simpleFunc_nonneg_ae_eq hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst : NormedAddCommGroup G'
inst_1 : PartialOrder G'
inst_2 : IsOrderedAddMonoid G'
inst_3 : NormedSpace ℝ G'
inst_4 : NormedAddCommGroup G''
inst_5 : PartialOrder G''
inst_6 : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G''), 0 ≤ x → LE.le.{u_8} (α := G') (0 : G') ((T s : (a : G'') → G') x : G')
f : ↥(simpleFunc G'' 1 μ)
hf : 0 ≤ f
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : (↑(↑(↑f : ↥(Lp G'' 1 μ)) : α →ₘ[μ] G'') : α → G'') =ᶠ[ae μ] (⇑f' : (a : α) → G'')
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have hff'₁ : EventuallyEq.{u_1, u_7} (β := G'') (ae μ) (⇑(toSimpleFunc f) : (a : α) → G'') (⇑f' : (a : α) → G'')
Tactic: replace hff' : simpleFunc.toSimpleFunc f =ᵐ[μ] f' :=
    (Lp.simpleFunc.toSimpleFunc_eq_toFun f).trans hff'
Cleared hypotheses: hff'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst : NormedAddCommGroup G'
inst_1 : PartialOrder G'
inst_2 : IsOrderedAddMonoid G'
inst_3 : NormedSpace ℝ G'
inst_4 : NormedAddCommGroup G''
inst_5 : PartialOrder G''
inst_6 : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G''), 0 ≤ x → LE.le.{u_8} (α := G') (0 : G') ((T s : (a : G'') → G') x : G')
f : ↥(simpleFunc G'' 1 μ)
hf : 0 ≤ f
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : EventuallyEq.{u_1, u_7} (β := G'') (ae μ) (⇑(toSimpleFunc f) : (a : α) → G'') (⇑f' : (a : α) → G'')
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
have rw : 0 ≤ SimpleFunc.setToSimpleFunc T f'
Tactic: rw [SimpleFunc.setToSimpleFunc_congr _ h_zero h_add (SimpleFunc.integrable _) hff']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst : NormedAddCommGroup G'
inst_1 : PartialOrder G'
inst_2 : IsOrderedAddMonoid G'
inst_3 : NormedSpace ℝ G'
inst_4 : NormedAddCommGroup G''
inst_5 : PartialOrder G''
inst_6 : IsOrderedAddMonoid G''
inst_7 : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G''), 0 ≤ x → LE.le.{u_8} (α := G') (0 : G') ((T s : (a : G'') → G') x : G')
f g : ↥(simpleFunc G'' 1 μ)
hfg : f ≤ g
⊢ setToL1S T f ≤ setToL1S T g
have rw : ∀ (hfg : 0 ≤ g - f), 0 ≤ setToL1S T g - setToL1S T f
Tactic: rw [← sub_nonneg] at hfg ⊢
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst : NormedAddCommGroup G'
inst_1 : PartialOrder G'
inst_2 : IsOrderedAddMonoid G'
inst_3 : NormedSpace ℝ G'
inst_4 : NormedAddCommGroup G''
inst_5 : PartialOrder G''
inst_6 : IsOrderedAddMonoid G''
inst_7 : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (x : G''), 0 ≤ x → LE.le.{u_8} (α := G') (0 : G') ((T s : (a : G'') → G') x : G')
f g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T g - setToL1S T f
have rw : 0 ≤ setToL1S T (g - f)
Tactic: rw [← setToL1S_sub h_zero 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : ↥(simpleFunc E 1 μ)
x : Set α
h_1 : MeasurableSet x
h_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ T x = T' x
have rw : T' x = T' x
Tactic: rw [h]
-- 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 α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : IsBoundedSMul 𝕜 E
inst_8 : IsBoundedSMul 𝕜 F
inst_9 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
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)
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
have apply : DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
Tactic: apply ContinuousLinearMap.extend_eq _ _ simpleFunc.isUniformInducing
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
f : ↥(Lp E 1 μ)
this : setToL1 hT = A
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ((A : (a : ↥(Lp E 1 μ)) → F) f : F)
have rw : Eq.{u_3 + 1} (α := F) ((A : (a : ↥(Lp E 1 μ)) → F) f : F) ((A : (a : ↥(Lp E 1 μ)) → F) f : F)
Tactic: rw [this]
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
f : ↥(Lp E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ((A : (a : ↥(Lp E 1 μ)) → F) f : F)
have suffices : setToL1 hT = A
Tactic: suffices setToL1 hT = A by rw [this]
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
f : ↥(Lp E 1 μ)
⊢ setToL1 hT = A
have h_dense : DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
Tactic: apply ContinuousLinearMap.extend_unique
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
f : ↥(Lp E 1 μ)
h_dense :
  DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
⊢ setToL1 hT = A
have h_e : IsUniformInducing (α := ↥(simpleFunc E 1 μ)) (β := ↥(Lp E 1 μ))
  (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
Tactic: apply ContinuousLinearMap.extend_unique
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
f : ↥(Lp E 1 μ)
h_dense :
  DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
h_e :
  IsUniformInducing (α := ↥(simpleFunc E 1 μ)) (β := ↥(Lp E 1 μ))
    (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))
⊢ setToL1 hT = A
have H : A ∘SL coeToLp α E ℝ = setToL1SCLM α E μ hT
Tactic: apply ContinuousLinearMap.extend_unique
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
f : ↥(Lp E 1 μ)
⊢ A ∘SL coeToLp α E ℝ = setToL1SCLM α E μ hT
have H : ∀ (f : ↥(simpleFunc E 1 μ)),
  Eq.{u_3 + 1} (α := F) ((A ∘SL coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
Tactic: ext 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
f_1 : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((A ∘SL coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
have H : Eq.{u_3 + 1} (α := F) ((A ∘SL coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
  ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
Tactic: rw [hA f]
-- 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 α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : IsBoundedSMul 𝕜 E
inst_8 : IsBoundedSMul 𝕜 F
inst_9 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
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)
f : ↥(Lp E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
    ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) f : F)
have h₁ : Dense (X := ↥(Lp E 1 μ)) (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)))
Tactic: have h₁ : Dense (Set.range (coeToLp α E ℝ)) := simpleFunc.denseRange (μ := μ) one_ne_top
-- 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 α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : IsBoundedSMul 𝕜 E
inst_8 : IsBoundedSMul 𝕜 F
inst_9 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
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)
f : ↥(Lp E 1 μ)
h₁ :
  Dense (X := ↥(Lp E 1 μ))
    (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)))
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
    ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) f : F)
have mem : ∀ (x : ↥(Lp E 1 μ)),
  Membership.mem (γ := Set ↥(Lp E 1 μ))
      (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))) x →
    Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) x : F)
      ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) x : F)
Tactic: apply Dense.induction (P := fun f : α →₁[μ] E ↦ (setToL1 hT) f = (setToL1' 𝕜 hT h_smul) f) h₁
-- 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 α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : IsBoundedSMul 𝕜 E
inst_8 : IsBoundedSMul 𝕜 F
inst_9 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
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)
f : ↥(Lp E 1 μ)
h₁ :
  Dense (X := ↥(Lp E 1 μ))
    (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)))
mem :
  ∀ (x : ↥(Lp E 1 μ)),
    Membership.mem (γ := Set ↥(Lp E 1 μ))
        (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))) x →
      Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) x : F)
        ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) x : F)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
    ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) f : F)
have isClosed : IsClosed (X := ↥(Lp E 1 μ))
  {x : ↥(Lp E 1 μ) |
    Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) x : F)
      ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) x : F)}
Tactic: apply Dense.induction (P := fun f : α →₁[μ] E ↦ (setToL1 hT) f = (setToL1' 𝕜 hT h_smul) f) h₁
-- 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 α
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
inst_7 : IsBoundedSMul 𝕜 E
inst_8 : IsBoundedSMul 𝕜 F
inst_9 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
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)
f_1 : ↥(Lp E 1 μ)
h₁ :
  Dense (X := ↥(Lp E 1 μ))
    (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)))
f : ↥(Lp E 1 μ)
⊢ Membership.mem (γ := Set ↥(Lp E 1 μ))
      (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))) f →
    Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
      ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) f : F)
have mem : ∀ (f' : ↥(simpleFunc E 1 μ)) (hf : (coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) f' = f),
  Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
    ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) f : F)
Tactic: ⟨f', hf⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : ↥(Lp E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) f : F)
have apply : ∀ (f : ↥(simpleFunc E 1 μ)),
  Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
Tactic: apply setToL1_unique hT (A := setToL1 hT') _ f