-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_zero_left (hT : DominatedFinMeasAdditive μ (0 : Set α → E →L[ℝ] F) C)
    (f : α →₁[μ] E) : setToL1 hT f = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
this : setToL1 hT = 0
⊢ 0 f = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
⊢ setToL1 hT = 0

Tactic:
refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT) _ _ _ _ ?_

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
⊢ ContinuousLinearMap.comp 0 (coeToLp α E ℝ) = setToL1SCLM α E μ hT

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
this : setToL1 hT = 0
⊢ (setToL1 hT) f = 0

Tactic:
rw [this]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
this : setToL1 hT = 0
⊢ 0 f = 0

Proof state:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f✝ : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
⊢ (ContinuousLinearMap.comp 0 (coeToLp α E ℝ)) f = (setToL1SCLM α E μ hT) f

Tactic:
rw [setToL1SCLM_zero_left hT f, ContinuousLinearMap.zero_comp, ContinuousLinearMap.zero_apply]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) f = 0

Tactic:
suffices setToL1 hT = 0 by rw [this]; simp

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
⊢ setToL1 hT = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f : ↥(Lp E 1 μ)
⊢ ContinuousLinearMap.comp 0 (coeToLp α E ℝ) = setToL1SCLM α E μ hT

Tactic:
ext1 f

Result:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
C : ℝ
hT : DominatedFinMeasAdditive μ 0 C
f✝ : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
⊢ (ContinuousLinearMap.comp 0 (coeToLp α E ℝ)) f = (setToL1SCLM α E μ hT) f