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 α
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)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
exact setToL1SCLM_congr_left hT' hT h.symm f

Premises used: MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left, 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 α
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 μ)
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)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ((setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) f : F)

Tactic:
apply setToL1_unique hT (A := setToL1 hT') _ f

Premises used: MeasureTheory.L1.setToL1_unique
-- 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 α
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)
rw 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)
⊢ 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:
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 α
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 μ)
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)
⊢ 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:
suffices setToL1 hT' f = setToL1SCLM α E μ hT f by 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 α
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 μ)
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)
⊢ 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:
rw [setToL1_eq_setToL1SCLM]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM
-- 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 α
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)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
(setToL1SCLM_congr_left' hT hT' h f).symm

Premises used: MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left', 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 α
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)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
exact (setToL1SCLM_congr_left' hT hT' h f).symm

Premises used: MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left', 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 α
inst_4 : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : ↥(Lp E 1 μ)
apply :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ ⋯ : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((setToL1 hT + setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
⊢ (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)

Tactic:
apply setToL1_unique (hT.add hT') (A := setToL1 hT + setToL1 hT') _ f

Premises used: MeasureTheory.L1.setToL1_unique, MeasureTheory.DominatedFinMeasAdditive.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 α
inst_4 : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ ⋯ : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((setToL1 hT + setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)

Tactic:
simp [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left hT hT']

Premises used: MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left, MeasureTheory.L1.setToL1_eq_setToL1SCLM
-- 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 α
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 μ)
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)
⊢ (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)

Tactic:
apply setToL1_unique hT'' (A := setToL1 hT + setToL1 hT') _ f

Premises used: MeasureTheory.L1.setToL1_unique
-- 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 α
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 μ)
⊢ ∀ (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:
simp [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left' hT hT' hT'' h_add]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : ↥(Lp E 1 μ)
apply :
  ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F)
      ((setToL1SCLM α E μ (T := fun (s : Set α) ↦ c • T s) (C := ‖c‖ * C) ⋯ : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((c • setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)
⊢ (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)

Tactic:
apply setToL1_unique (hT.smul c) (A := c • setToL1 hT) _ f

Premises used: MeasureTheory.DominatedFinMeasAdditive.smul, MeasureTheory.L1.setToL1_unique
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F)
      ((setToL1SCLM α E μ (T := fun (s : Set α) ↦ c • T s) (C := ‖c‖ * C) ⋯ : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((c • setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)

Tactic:
simp [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left c hT]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_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 α
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 μ)
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)
⊢ (setToL1 hT' : (a : ↥(Lp E 1 μ)) → F) f = HSMul.hSMul (β := F) c ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)

Tactic:
apply setToL1_unique hT' (A := c • setToL1 hT) _ f

Premises used: MeasureTheory.L1.setToL1_unique
-- 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 α
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 μ)
⊢ ∀ (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:
simp [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left' c hT hT' h_smul]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left'
-- 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 α
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 μ)
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)
⊢ (setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (c • f) = HSMul.hSMul (β := F) c ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F)

Tactic:
rw [setToL1_eq_setToL1' hT h_smul, setToL1_eq_setToL1' hT h_smul]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1'
-- 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 α
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 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:
map_smul _ _ _

Premises used: map_smul
-- 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 α
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 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:
exact map_smul _ _ _

Premises used: map_smul
-- 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 α
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
rw :
  Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) (indicatorConst 1 (s := s) hs ⋯ x) : F)
    ((T s : (a : E) → F) x : F)
⊢ 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)

Tactic:
rw [setToL1_eq_setToL1SCLM]

Premises used: MeasureTheory.L1.setToL1_eq_setToL1SCLM
-- 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 α
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) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) (indicatorConst 1 (s := s) hs ⋯ x) : F)
    ((T s : (a : E) → F) x : F)

Tactic:
setToL1S_indicatorConst (fun s => hT.eq_zero_of_measure_zero) hT.1 hs hμs x

Premises used: Multiset.sum, Multiset.foldr, MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst, MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, And.left, MeasureTheory.L1.SimpleFunc.setToL1S, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum
-- 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 α
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) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) (indicatorConst 1 (s := s) hs ⋯ x) : F)
    ((T s : (a : E) → F) x : F)

Tactic:
exact setToL1S_indicatorConst (fun s => hT.eq_zero_of_measure_zero) hT.1 hs hμs x

Premises used: MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst, MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zero, And.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 α
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
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)
⊢ 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)

Tactic:
rw [← Lp.simpleFunc.coe_indicatorConst hs hμs x]

Premises used: MeasureTheory.Lp.simpleFunc.coe_indicatorConst
-- 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 α
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) (↑(indicatorConst 1 (s := s) hs hμs x) : ↥(Lp E 1 μ)) : F)
    ((T s : (a : E) → F) x : F)

Tactic:
setToL1_simpleFunc_indicatorConst hT hs hμs.lt_top x

Premises used: Ne.lt_top, MeasureTheory.L1.setToL1_simpleFunc_indicatorConst
-- 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 α
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) (↑(indicatorConst 1 (s := s) hs hμs x) : ↥(Lp E 1 μ)) : F)
    ((T s : (a : E) → F) x : F)

Tactic:
exact setToL1_simpleFunc_indicatorConst hT hs hμs.lt_top x

Premises used: Ne.lt_top, MeasureTheory.L1.setToL1_simpleFunc_indicatorConst
-- 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 α
inst_4 : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst_5 : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) (indicatorConstLp (s := univ) 1 ⋯ ⋯ x) : F)
    ((T univ : (a : E) → F) x : F)

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

Premises used: MeasureTheory.L1.setToL1_indicatorConstLp, MeasureTheory.measure_ne_top, MeasurableSet.univ
-- 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 : 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∞)
indicatorConst : LE.le.{u_8} (α := G'') ((T s : (a : E) → G'') c : G'') ((T' s : (a : E) → G'') c : G'')
⊢ 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'')

Tactic:
rw [setToL1_simpleFunc_indicatorConst hT hs hμs, setToL1_simpleFunc_indicatorConst hT' hs hμs]

Premises used: MeasureTheory.L1.setToL1_simpleFunc_indicatorConst
-- 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 : 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'') ((T s : (a : E) → G'') c : G'') ((T' s : (a : E) → G'') c : G'')

Tactic:
hTT' s hs hμs c