case empty
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s → 0 ≤ f x
h : ∀ (x : ι), x ∈ ∅ → 0 ≤ f x
⊢ a ^ ∑ x in ∅, f x = ∏ x in ∅, a ^ f x

case cons
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s✝ : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s✝ → 0 ≤ f x
i : ι
s : Finset ι
hi : ¬i ∈ s
ihs : (∀ (x : ι), x ∈ s → 0 ≤ f x) → a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
h : ∀ (x : ι), x ∈ cons i s hi → 0 ≤ f x
⊢ a ^ ∑ x in cons i s hi, f x = ∏ x in cons i s hi, a ^ f x
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h : ∀ (x : ι), x ∈ s → 0 ≤ f x
⊢ a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
induction' s using Finset.cons_induction with i s hi ihs
no goals
case empty
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s → 0 ≤ f x
h : ∀ (x : ι), x ∈ ∅ → 0 ≤ f x
⊢ a ^ ∑ x in ∅, f x = ∏ x in ∅, a ^ f x
rw [sum_empty, Finset.prod_empty, rpow_zero]
case cons
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s✝ : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s✝ → 0 ≤ f x
i : ι
s : Finset ι
hi : ¬i ∈ s
ihs : (∀ (x : ι), x ∈ s → 0 ≤ f x) → a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
h : 0 ≤ f i ∧ ∀ (x : ι), x ∈ s → 0 ≤ f x
⊢ a ^ ∑ x in cons i s hi, f x = ∏ x in cons i s hi, a ^ f x
case cons
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s✝ : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s✝ → 0 ≤ f x
i : ι
s : Finset ι
hi : ¬i ∈ s
ihs : (∀ (x : ι), x ∈ s → 0 ≤ f x) → a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
h : ∀ (x : ι), x ∈ cons i s hi → 0 ≤ f x
⊢ a ^ ∑ x in cons i s hi, f x = ∏ x in cons i s hi, a ^ f x
rw [forall_mem_cons] at h
no goals
case cons
x y z : ℝ
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s✝ : Finset ι
f : ι → ℝ
h✝ : ∀ (x : ι), x ∈ s✝ → 0 ≤ f x
i : ι
s : Finset ι
hi : ¬i ∈ s
ihs : (∀ (x : ι), x ∈ s → 0 ≤ f x) → a ^ ∑ x in s, f x = ∏ x in s, a ^ f x
h : 0 ≤ f i ∧ ∀ (x : ι), x ∈ s → 0 ≤ f x
⊢ a ^ ∑ x in cons i s hi, f x = ∏ x in cons i s hi, a ^ f x
rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]