case empty
b x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s → f x ≠ 0
hf : ∀ (x : α), x ∈ ∅ → f x ≠ 0
⊢ logb b (∏ i in ∅, f i) = ∑ i in ∅, logb b (f i)

case insert
b x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
hf : ∀ (x : α), x ∈ insert a s → f x ≠ 0
⊢ logb b (∏ i in insert a s, f i) = ∑ i in insert a s, logb b (f i)
b x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ (x : α), x ∈ s → f x ≠ 0
⊢ logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
induction' s using Finset.induction_on with a s ha ih
case insert
b x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
hf : f a ≠ 0 ∧ ∀ (a : α), a ∈ s → f a ≠ 0
⊢ logb b (∏ i in insert a s, f i) = ∑ i in insert a s, logb b (f i)
case insert
b x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
hf : ∀ (x : α), x ∈ insert a s → f x ≠ 0
⊢ logb b (∏ i in insert a s, f i) = ∑ i in insert a s, logb b (f i)
simp only [Finset.mem_insert, forall_eq_or_imp] at hf
no goals
case insert
b x y : ℝ
α : Type u_1
s✝ : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s✝ → f x ≠ 0
a : α
s : Finset α
ha : ¬a ∈ s
ih : (∀ (x : α), x ∈ s → f x ≠ 0) → logb b (∏ i in s, f i) = ∑ i in s, logb b (f i)
hf : f a ≠ 0 ∧ ∀ (a : α), a ∈ s → f a ≠ 0
⊢ logb b (∏ i in insert a s, f i) = ∑ i in insert a s, logb b (f i)
simp [ha, ih hf.2, logb_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]
no goals
case empty
b x y : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf✝ : ∀ (x : α), x ∈ s → f x ≠ 0
hf : ∀ (x : α), x ∈ ∅ → f x ≠ 0
⊢ logb b (∏ i in ∅, f i) = ∑ i in ∅, logb b (f i)
simp