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 α
inst_4 : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f_1 : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
this :
  Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
⊢ 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)
have rw : Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
  ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f_1 : ↥(Lp E 1 μ)
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)
have suffices : Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
  ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
Tactic: suffices setToL1 hT' f = setToL1SCLM α E μ hT f 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f_1 : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
have rw : Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
  ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
Tactic: rw [setToL1_eq_setToL1SCLM]
-- 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 : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
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
-- 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 : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f_1 : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
this :
  Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
⊢ 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)
have rw : Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
  ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f_1 : ↥(Lp E 1 μ)
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)
have suffices : Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
  ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
Tactic: suffices setToL1 hT' f = setToL1SCLM α E μ hT f 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = T' s
f_1 : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
have rw : Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT' : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
  ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
Tactic: rw [setToL1_eq_setToL1SCLM]
-- 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'
f : ↥(Lp E 1 μ)
⊢ (setToL1 ⋯ : (a : ↥(Lp E 1 μ)) → F) f =
    HAdd.hAdd (α := F) (β := 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 μ sorry : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
    ((setToL1 hT + setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
Tactic: apply setToL1_unique (hT.add hT') (A := setToL1 hT + setToL1 hT') _ 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 T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T'' s = T s + T' s
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT'' : (a : ↥(Lp E 1 μ)) → F) f =
    HAdd.hAdd (α := F) (β := 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 + setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
Tactic: apply setToL1_unique hT'' (A := setToL1 hT + setToL1 hT') _ 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
c : ℝ
f : ↥(Lp E 1 μ)
⊢ (setToL1 (T := fun (s : Set α) ↦ c • T s) (C := ‖c‖ * C) ⋯ : (a : ↥(Lp E 1 μ)) → F) f =
    HSMul.hSMul (β := F) c ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
have apply : ∀ (f : ↥(simpleFunc E 1 μ)),
  Eq.{u_3 + 1} (α := F)
    ((setToL1SCLM α E μ (T := fun (s : Set α) ↦ c • T s) (C := ‖c‖ * C) sorry : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
    ((c • setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
Tactic: apply setToL1_unique (hT.smul c) (A := c • setToL1 hT) _ 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T' s = c • T s
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) f = HSMul.hSMul (β := F) c ((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)
    ((c • setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
Tactic: apply setToL1_unique hT' (A := c • setToL1 hT) _ 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 α
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)
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (c • f) = HSMul.hSMul (β := F) c ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)
have rw : (setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) (c • f) =
  HSMul.hSMul (β := F) c ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F) f : F)
Tactic: rw [setToL1_eq_setToL1' hT h_smul, setToL1_eq_setToL1' hT h_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (↑(indicatorConst 1 (s := s) hs ⋯ x) : ↥(Lp E 1 μ)) : F)
    ((T s : (a : E) → F) x : F)
have rw : Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) (indicatorConst 1 (s := s) hs sorry x) : F)
  ((T s : (a : E) → F) x : F)
Tactic: rw [setToL1_eq_setToL1SCLM]
-- 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
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (indicatorConstLp (s := s) 1 hs hμs x) : F)
    ((T s : (a : E) → F) x : F)
have rw : Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (↑(indicatorConst 1 (s := s) hs hμs x) : ↥(Lp E 1 μ)) : F)
  ((T s : (a : E) → F) x : F)
Tactic: rw [← Lp.simpleFunc.coe_indicatorConst hs hμs x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : CompleteSpace G''
inst_7 : 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'')
c : E
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le.{u_8} (α := G'')
    ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (↑(indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (↑(indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
have indicatorConst : LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') c : G'') ((T' s : (a : E) → G'') c : G'')
Tactic: rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : CompleteSpace G''
inst_7 : 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 g : α → E
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
hg_le :
  LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
have add : HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
    ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'') ≤
  HAdd.hAdd (α := G'') (β := G'') ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
Tactic: rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : CompleteSpace G''
inst_7 : 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 : ↥(Lp E 1 μ)
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')
have indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le.{u_8} (α := G'')
    ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (↑(indicatorConst 1 (s := s) hs sorry c) : ↥(Lp E 1 μ)) : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (↑(indicatorConst 1 (s := s) hs sorry c) : ↥(Lp E 1 μ)) : G'')
Tactic: induction f using Lp.induction (hp_ne_top := one_ne_top) with
  | @indicatorConst c s hs hμs =>
    rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
    exact hTT' s hs hμs c
  | @add f g hf hg _ hf_le hg_le =>
    rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
    exact add_le_add hf_le hg_le
  | isClosed => exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : CompleteSpace G''
inst_7 : 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 : ↥(Lp E 1 μ)
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LE.le.{u_8} (α := G'')
      ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
      ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')
have add : ∀ ⦃f g : α → E⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
  Disjoint (Function.support f) (Function.support g) →
    ∀
      (hf_le :
        LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
          ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G''))
      (hg_le :
        LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
          ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')),
      LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
        ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
Tactic: induction f using Lp.induction (hp_ne_top := one_ne_top) with
  | @indicatorConst c s hs hμs =>
    rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
    exact hTT' s hs hμs c
  | @add f g hf hg _ hf_le hg_le =>
    rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
    exact add_le_add hf_le hg_le
  | isClosed => exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
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 : CompleteSpace G''
inst_7 : 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 : ↥(Lp E 1 μ)
indicatorConst :
  ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LE.le.{u_8} (α := G'')
      ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
      ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp E 1 μ)) : G'')
add :
  ∀ ⦃f g : α → E⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      ∀
        (hf_le :
          LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G'')
            ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf) : G''))
        (hg_le :
          LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')
            ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp g hg) : G'')),
        LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
          ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') (MemLp.toLp f hf + MemLp.toLp g hg) : G'')
⊢ LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
    ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')
have isClosed : IsClosed (X := ↥(Lp E 1 μ))
  {f : ↥(Lp E 1 μ) |
    LE.le.{u_8} (α := G'') ((setToL1 hT : (a : ↥(Lp E 1 μ)) → G'') f : G'')
      ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → G'') f : G'')}
Tactic: induction f using Lp.induction (hp_ne_top := one_ne_top) with
  | @indicatorConst c s hs hμs =>
    rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]
    exact hTT' s hs hμs c
  | @add f g hf hg _ hf_le hg_le =>
    rw [(setToL1 hT).map_add, (setToL1 hT').map_add]
    exact add_le_add hf_le hg_le
  | isClosed => exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous
Cleared hypotheses: f
-- 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 : CompleteSpace G''
inst_5 : NormedAddCommGroup G'
inst_6 : PartialOrder G'
inst_7 : NormedSpace ℝ G'
inst_8 : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
⊢ LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') f : G'')
have suffices : ∀ (f : { g : ↥(Lp G' 1 μ) // 0 ≤ g }),
  LE.le.{u_8} (α := G'') (0 : G'') ((setToL1 hT : (a : ↥(Lp G' 1 μ)) → G'') (↑f : ↥(Lp G' 1 μ)) : G'')
Tactic: suffices ∀ f : { g : α →₁[μ] G' // 0 ≤ g }, 0 ≤ setToL1 hT f from
    this (⟨f, hf⟩ : { g : α →₁[μ] G' // 0 ≤ g })