awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
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 μ)
⊢ DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
simpleFunc.denseRange one_ne_top

Premises used: Set.Mem, MeasureTheory.Lp.simpleFunc.denseRange, ENNReal.one_ne_top
-- 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)
f : ↥(simpleFunc E 1 μ)
⊢ DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E 𝕜) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
exact simpleFunc.denseRange one_ne_top

Premises used: MeasureTheory.Lp.simpleFunc.denseRange, ENNReal.one_ne_top
-- 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)
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F)
    ((setToL1' 𝕜 hT h_smul : (a : ↥(Lp E 1 μ)) → F)
        ((coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) f : ↥(Lp E 1 μ)) :
      F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
setToL1'_eq_setToL1SCLM 𝕜 hT h_smul f

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
f : ↥(simpleFunc E 1 μ)
⊢ ∀ (c : ℝ) (s : Set α) (x : E), (T s : (a : E) → F) (c • x) = HSMul.hSMul (β := F) c ((T s : (a : E) → F) x : F)

Tactic:
simp
-- 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
f : ↥(simpleFunc E 1 μ)
⊢ Eq.{u_3 + 1} (α := F)
    ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) ((coeToLp α E ℝ : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)) f : ↥(Lp E 1 μ)) :
      F)
    ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)

Tactic:
setToL1_eq_setToL1SCLM hT f

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
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
rw rw₁ : Eq.{u_3 + 1} (α := F) ((A : (a : ↥(Lp E 1 μ)) → F) f : F) ((A : (a : ↥(Lp E 1 μ)) → F) f : F)
⊢ Eq.{u_3 + 1} (α := F) ((setToL1 hT : (a : ↥(Lp E 1 μ)) → F) f : F) ((A : (a : ↥(Lp E 1 μ)) → F) f : 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 : 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 μ)
suffices : 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)

Tactic:
suffices setToL1 hT = A 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 : 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 μ))
H : A ∘SL coeToLp α E ℝ = setToL1SCLM α E μ hT
⊢ setToL1 hT = A

Tactic:
apply ContinuousLinearMap.extend_unique

Premises used: ContinuousLinearMap.extend_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
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 μ)
⊢ DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
(simpleFunc.denseRange one_ne_top)

Premises used: Set.Mem, MeasureTheory.Lp.simpleFunc.denseRange, ENNReal.one_ne_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 α
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 μ)
⊢ DenseRange (X := ↥(Lp E 1 μ)) (α := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
exact (simpleFunc.denseRange one_ne_top)

Premises used: MeasureTheory.Lp.simpleFunc.denseRange, ENNReal.one_ne_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 α
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 μ)
⊢ IsUniformInducing (α := ↥(simpleFunc E 1 μ)) (β := ↥(Lp E 1 μ))
    (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
simpleFunc.isUniformInducing

Premises used: Set.Mem, MeasureTheory.Lp.simpleFunc.isUniformInducing
-- 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
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 μ)
⊢ IsUniformInducing (α := ↥(simpleFunc E 1 μ)) (β := ↥(Lp E 1 μ))
    (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ))

Tactic:
exact simpleFunc.isUniformInducing

Premises used: MeasureTheory.Lp.simpleFunc.isUniformInducing
-- 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
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 :
  ∀ (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)
⊢ A ∘SL coeToLp α E ℝ = setToL1SCLM α E μ hT

Tactic:
ext 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 α
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 μ)
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)
⊢ 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:
rw [hA 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 α
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)
    ((A : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)

Tactic:
rfl
-- 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)
f : ↥(Lp E 1 μ)
⊢ 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
-- 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)
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)
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)}
⊢ 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:
apply Dense.induction (P := fun f : α →₁[μ] E ↦ (setToL1 hT) f = (setToL1' 𝕜 hT h_smul) f) h₁

Premises used: Dense.induction
-- 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)
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 μ)
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)
⊢ 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)

Tactic:
⟨f', hf⟩
-- 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)
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 μ)
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:
simp [← hf]
-- 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)
f : ↥(Lp E 1 μ)
h₁ :
  Dense (X := ↥(Lp E 1 μ))
    (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)))
⊢ 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:
isClosed_eq (setToL1 hT).continuous (setToL1' 𝕜 hT h_smul).continuous

Premises used: ContinuousLinearMap.continuous, isClosed_eq, MeasureTheory.L1.setToL1, MeasureTheory.L1.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)
f : ↥(Lp E 1 μ)
h₁ :
  Dense (X := ↥(Lp E 1 μ))
    (range (ι := ↥(simpleFunc E 1 μ)) (⇑(coeToLp α E ℝ) : (a : ↥(simpleFunc E 1 μ)) → ↥(Lp E 1 μ)))
⊢ 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:
exact isClosed_eq (setToL1 hT).continuous (setToL1' 𝕜 hT h_smul).continuous

Premises used: ContinuousLinearMap.continuous, isClosed_eq, MeasureTheory.L1.setToL1, MeasureTheory.L1.setToL1'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_4 : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive (β := E →L[ℝ] F) μ 0 C
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((0 : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)

Tactic:
simp
-- 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
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(simpleFunc E 1 μ)),
    Eq.{u_3 + 1} (α := F) ((setToL1SCLM α E μ hT : (a : ↥(simpleFunc E 1 μ)) → F) f : F)
      ((0 : (a : ↥(Lp E 1 μ)) → F) (↑f : ↥(Lp E 1 μ)) : F)

Tactic:
simp [setToL1SCLM_zero_left' hT h_zero]

Premises used: MeasureTheory.L1.SimpleFunc.setToL1SCLM_zero_left'
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
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 μ)
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 : 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)
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 : T = T'
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 : T = T'
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 : 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:
setToL1SCLM_congr_left hT' hT h.symm f

Premises used: MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left, Eq.symm