-- Mathlib/FieldTheory/Differential/Basic.lean
lemma logDeriv_multisetProd {ι : Type*} (s : Multiset ι) {f : ι → R} (h : ∀ x ∈ s, f x ≠ 0) :
    logDeriv (s.map f).prod = (s.map fun x ↦ logDeriv (f x)).sum

Proof state:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (f a✝ * (Multiset.map f s✝).prod) = logDeriv (f a✝) + logDeriv (Multiset.map f s✝).prod

Tactic:
apply logDeriv_mul

Result:
case cons.ha
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ f a✝ ≠ 0

case cons.hb
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ (Multiset.map f s✝).prod ≠ 0

Proof state:
case cons.ha
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ f a✝ ≠ 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ ∀ x ∈ s✝, f x ≠ 0

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (Multiset.map f (a✝ ::ₘ s✝)).prod = (Multiset.map (fun x => logDeriv (f x)) (a✝ ::ₘ s✝)).sum

Tactic:
simp only [Function.comp_apply, Multiset.map_cons, Multiset.sum_cons, Multiset.prod_cons]

Result:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (f a✝ * (Multiset.map f s✝).prod) = logDeriv (f a✝) + (Multiset.map (fun x => logDeriv (f x)) s✝).sum

Proof state:
case cons.hb
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ (Multiset.map f s✝).prod ≠ 0

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (f a✝ * (Multiset.map f s✝).prod) = logDeriv (f a✝) + (Multiset.map (fun x => logDeriv (f x)) s✝).sum

Tactic:
rw [← h₂]

Result:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (f a✝ * (Multiset.map f s✝).prod) = logDeriv (f a✝) + logDeriv (Multiset.map f s✝).prod

case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ ∀ x ∈ s✝, f x ≠ 0

Proof state:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝¹ : ι
s✝ : Multiset ι
a✝ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝¹ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (Multiset.map f (a✝¹ ::ₘ s✝)).prod = (Multiset.map (fun x => logDeriv (f x)) (a✝¹ ::ₘ s✝)).sum

Tactic:
rename_i h₂

Result:
case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝ : ι
s✝ : Multiset ι
h₂ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (Multiset.map f (a✝ ::ₘ s✝)).prod = (Multiset.map (fun x => logDeriv (f x)) (a✝ ::ₘ s✝)).sum

Proof state:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Multiset ι
f : ι → R
h : ∀ x ∈ s, f x ≠ 0
⊢ logDeriv (Multiset.map f s).prod = (Multiset.map (fun x => logDeriv (f x)) s).sum

Tactic:
induction s using Multiset.induction_on

Result:
case empty
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
h : ∀ x ∈ 0, f x ≠ 0
⊢ logDeriv (Multiset.map f 0).prod = (Multiset.map (fun x => logDeriv (f x)) 0).sum

case cons
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
a✝¹ : ι
s✝ : Multiset ι
a✝ : (∀ x ∈ s✝, f x ≠ 0) → logDeriv (Multiset.map f s✝).prod = (Multiset.map (fun x => logDeriv (f x)) s✝).sum
h : ∀ x ∈ a✝¹ ::ₘ s✝, f x ≠ 0
⊢ logDeriv (Multiset.map f (a✝¹ ::ₘ s✝)).prod = (Multiset.map (fun x => logDeriv (f x)) (a✝¹ ::ₘ s✝)).sum

Proof state:
case empty
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
h : ∀ x ∈ 0, f x ≠ 0
⊢ logDeriv (Multiset.map f 0).prod = (Multiset.map (fun x => logDeriv (f x)) 0).sum

Tactic:
simp

Result:
no goals