α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1671137
G : Type ?u.1671140
𝕜 : Type ?u.1671143
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑(⊤ • μ) s < ⊤
⊢ ↑↑(⊤ • μ) s = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1671137
G : Type ?u.1671140
𝕜 : Type ?u.1671143
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
⊢ setToFun (⊤ • μ) T hT f = 0
refine' setToFun_measure_zero' hT fun s _ hμs => _
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1671137
G : Type ?u.1671140
𝕜 : Type ?u.1671143
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑(⊤ • μ) s ≠ ⊤
⊢ ↑↑(⊤ • μ) s = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1671137
G : Type ?u.1671140
𝕜 : Type ?u.1671143
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑(⊤ • μ) s < ⊤
⊢ ↑↑(⊤ • μ) s = 0
rw [lt_top_iff_ne_top] at hμs
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1671137
G : Type ?u.1671140
𝕜 : Type ?u.1671143
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ¬↑↑μ s = ⊤ ∧ ↑↑μ s = 0
⊢ ↑↑(⊤ • μ) s = 0
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1671137
G : Type ?u.1671140
𝕜 : Type ?u.1671143
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑(⊤ • μ) s ≠ ⊤
⊢ ↑↑(⊤ • μ) s = 0
simp only [true_and_iff, Measure.smul_apply, ENNReal.mul_eq_top, eq_self_iff_true,
  top_ne_zero, Ne.def, not_false_iff, not_or, Classical.not_not, smul_eq_mul] at hμs
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1671137
G : Type ?u.1671140
𝕜 : Type ?u.1671143
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ¬↑↑μ s = ⊤ ∧ ↑↑μ s = 0
⊢ ↑↑(⊤ • μ) s = 0
simp only [hμs.right, Measure.smul_apply, MulZeroClass.mul_zero, smul_eq_mul]