α : Type u_1
E : Type ?u.26387
F : Type ?u.26390
F' : Type ?u.26393
G : Type ?u.26396
𝕜 : Type ?u.26399
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 α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑(c • μ) s = ⊤
⊢ ↑↑μ s = ⊤
α : Type u_1
E : Type ?u.26387
F : Type ?u.26390
F' : Type ?u.26393
G : Type ?u.26396
𝕜 : Type ?u.26399
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 α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
⊢ FinMeasAdditive μ T
refine' of_eq_top_imp_eq_top (fun s _ hμs => _) hT
α : Type u_1
E : Type ?u.26387
F : Type ?u.26390
F' : Type ?u.26393
G : Type ?u.26396
𝕜 : Type ?u.26399
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 α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : c ≠ 0 ∧ ↑↑μ s = ⊤ ∨ c = ⊤ ∧ ↑↑μ s ≠ 0
⊢ ↑↑μ s = ⊤
α : Type u_1
E : Type ?u.26387
F : Type ?u.26390
F' : Type ?u.26393
G : Type ?u.26396
𝕜 : Type ?u.26399
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 α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : ↑↑(c • μ) s = ⊤
⊢ ↑↑μ s = ⊤
rw [Measure.smul_apply, smul_eq_mul, ENNReal.mul_eq_top] at hμs
α : Type u_1
E : Type ?u.26387
F : Type ?u.26390
F' : Type ?u.26393
G : Type ?u.26396
𝕜 : Type ?u.26399
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 α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : ¬c = 0 ∧ ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤
α : Type u_1
E : Type ?u.26387
F : Type ?u.26390
F' : Type ?u.26393
G : Type ?u.26396
𝕜 : Type ?u.26399
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 α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : c ≠ 0 ∧ ↑↑μ s = ⊤ ∨ c = ⊤ ∧ ↑↑μ s ≠ 0
⊢ ↑↑μ s = ⊤
simp only [hc_ne_top, or_false_iff, Ne.def, false_and_iff] at hμs
no goals
α : Type u_1
E : Type ?u.26387
F : Type ?u.26390
F' : Type ?u.26393
G : Type ?u.26396
𝕜 : Type ?u.26399
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 α
β : Type u_2
inst✝ : AddCommMonoid β
T T' : Set α → β
c : ℝ≥0∞
hc_ne_top : c ≠ ⊤
hT : FinMeasAdditive (c • μ) T
s : Set α
x✝ : MeasurableSet s
hμs : ¬c = 0 ∧ ↑↑μ s = ⊤
⊢ ↑↑μ s = ⊤
exact hμs.2