-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_congr_smul_measure (c : ℝ≥0∞) (hc_ne_top : c ≠ ∞)
    (hT : DominatedFinMeasAdditive μ T C) (hT_smul : DominatedFinMeasAdditive (c • μ) T C')
    (f : α → E) : setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Proof state:
case pos
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
simp [hc0] at hT_smul

Result:
case pos
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul✝ : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : DominatedFinMeasAdditive 0 T C'
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul✝ f

Proof state:
case pos.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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul✝ : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : DominatedFinMeasAdditive 0 T C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0
⊢ c • μ = 0

Tactic:
simp [hc0]

Result:
no goals

Proof state:
case pos
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul✝ : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : DominatedFinMeasAdditive 0 T C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul✝ f

Tactic:
rw [setToFun_zero_left' _ h, setToFun_measure_zero]

Result:
case pos.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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul✝ : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : DominatedFinMeasAdditive 0 T C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0
⊢ c • μ = 0

Proof state:
case neg.refine_2
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ μ = c⁻¹ • c • μ

Tactic:
rw [smul_smul, ENNReal.inv_mul_cancel hc0 hc_ne_top, one_smul]

Result:
no goals

Proof state:
case neg.refine_1
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ c⁻¹ ≠ ⊤

Tactic:
simp [hc0]

Result:
no goals

Proof state:
case pos
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul✝ : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : DominatedFinMeasAdditive 0 T C'
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul✝ f

Tactic:
have h : ∀ s, MeasurableSet s → μ s < ∞ → T s = 0 := fun s hs _ => hT_smul.eq_zero hs

Result:
case pos
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul✝ : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
hT_smul : DominatedFinMeasAdditive 0 T C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul✝ f

Proof state:
case neg
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
refine setToFun_congr_measure c⁻¹ c ?_ hc_ne_top (le_of_eq ?_) le_rfl hT hT_smul f

Result:
case neg.refine_1
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ c⁻¹ ≠ ⊤

case neg.refine_2
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ μ = c⁻¹ • c • μ

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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
by_cases hc0 : c = 0

Result:
case pos
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : c = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

case neg
α : 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
T : Set α → E →L[ℝ] F
C C' : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
hc0 : ¬c = 0
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f