α : Type u_1
β : Type ?u.202901
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∀ (x : α), x ∈ s → f x = ↑(ENNReal.toNNReal (f x))

α : Type u_1
β : Type ?u.202901
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∑ a in s, f a ≠ ⊤
α : Type u_1
β : Type ?u.202901
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ENNReal.toNNReal (∑ a in s, f a) = ∑ a in s, ENNReal.toNNReal (f a)
rw [← coe_eq_coe, coe_toNNReal, coe_finset_sum, sum_congr rfl]
α : Type u_1
β : Type ?u.202901
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
x : α
hx : x ∈ s
⊢ f x = ↑(ENNReal.toNNReal (f x))
α : Type u_1
β : Type ?u.202901
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∀ (x : α), x ∈ s → f x = ↑(ENNReal.toNNReal (f x))
intro x hx
no goals
α : Type u_1
β : Type ?u.202901
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
x : α
hx : x ∈ s
⊢ f x = ↑(ENNReal.toNNReal (f x))
exact (coe_toNNReal (hf x hx)).symm
no goals
α : Type u_1
β : Type ?u.202901
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f : α → ℝ≥0∞
hf : ∀ (a : α), a ∈ s → f a ≠ ⊤
⊢ ∑ a in s, f a ≠ ⊤
exact (sum_lt_top hf).ne