Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: case cons
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ logDeriv (f a) x + logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x

pp: case cons.hf
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ f a x ≠ 0

pp: case cons.hg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ ∏ i ∈ s, f i x ≠ 0

pp: case cons.hdf
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (f a) x

pp: case cons.hdg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (fun x ↦ ∏ i ∈ s, f i x) x

Tactic:
ih hf.2 hd.2

Goal state after:
case cons
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x

case cons.hf
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ f a x ≠ 0

case cons.hg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ ∏ i ∈ s, f i x ≠ 0

case cons.hdf
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (f a) x

case cons.hdg
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  (∀ i ∈ s, f i x ≠ 0) →
    (∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) → logDeriv (fun x ↦ ∏ i ∈ s, f i x) x = ∑ i ∈ s, logDeriv (f i) x
hf : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
hd : DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x
⊢ DifferentiableAt 𝕜 (fun x ↦ ∏ i ∈ s, f i x) x