awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)
hf : ∀ i ∈ Finset.cons a s ha, f i x ≠ 0
hd : ∀ i ∈ Finset.cons a s ha, DifferentiableAt 𝕜 (f i) x
hf₁ : f a x ≠ 0 ∧ ∀ x_1 ∈ s, f x_1 x ≠ 0
⊢ DifferentiableAt 𝕜 (f a) x ∧ ∀ x_1 ∈ s, DifferentiableAt 𝕜 (f x_1) x

Tactic:
rw [Finset.forall_mem_cons] at hf hd

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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
cons : logDeriv (fun (x : 𝕜) ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ Finset.cons a s ha, f i x) x)
    (∑ i ∈ Finset.cons a s ha, logDeriv (f i) x)

Tactic:
simp_rw [Finset.prod_cons, Finset.sum_cons]

Premises used: Finset.sum_cons, Finset.prod_cons
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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
cons : f a x ≠ 0
cons₁ : Ne.{u_2 + 1} (α := 𝕜') (∏ i ∈ s, f i x) 0
cons₂ : DifferentiableAt 𝕜 (f a) x
cons₃ : DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x
⊢ logDeriv (fun (x : 𝕜) ↦ f a x * ∏ i ∈ s, f i x) x = logDeriv (f a) x + ∑ i ∈ s, logDeriv (f i) x

Tactic:
rw [logDeriv_mul, ih hf.2 hd.2]

Premises used: logDeriv_mul, And.right
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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

Tactic:
exact hf.1

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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
⊢ Ne.{u_2 + 1} (α := 𝕜') (∏ i ∈ s, f i x) 0

Tactic:
simpa [Finset.prod_eq_zero_iff] using hf.2

Premises used: Finset.prod_eq_zero_iff, And.right
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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

Tactic:
hd.1

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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

Tactic:
exact hd.1

Premises used: And.left
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
f : ι → 𝕜 → 𝕜'
x : 𝕜
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (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.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x

Tactic:
.fun_finsetProd hd.2

Premises used: DifferentiableAt.fun_finsetProd, And.right
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜'
x : 𝕜
hf : ∀ i ∈ s, f i x ≠ 0
hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i x ≠ 0)
    (hd : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ ∅, f i x) x) (∑ i ∈ ∅, logDeriv (f i) x)
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      ∀ (hf : ∀ i ∈ s, f i x ≠ 0) (hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x),
        Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x))
    (hf : ∀ i ∈ Finset.cons a s ha, f i x ≠ 0) (hd : ∀ i ∈ Finset.cons a s ha, DifferentiableAt 𝕜 (f i) x),
    Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ Finset.cons a s ha, f i x) x)
      (∑ i ∈ Finset.cons a s ha, logDeriv (f i) x)
⊢ Eq.{u_2 + 1} (α := 𝕜') (logDeriv (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) x) (∑ i ∈ s, logDeriv (f i) x)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    rw [Finset.forall_mem_cons] at hf hd
    simp_rw [Finset.prod_cons, Finset.sum_cons]
    rw [logDeriv_mul, ih hf.2 hd.2]
    · exact hf.1
    · simpa [Finset.prod_eq_zero_iff] using hf.2
    · exact hd.1
    · exact .fun_finsetProd hd.2

Premises used: logDeriv_mul, Finset.sum_cons, Finset.prod_eq_zero_iff, Finset.forall_mem_cons, Finset.prod_cons
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
inl : logDeriv (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) (f x) 0) x = (↑0 : 𝕜') * logDeriv f x
inr : ∀ (hn : n ≠ 0), logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
⊢ logDeriv (fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) (f x) 0) x = (↑0 : 𝕜') * logDeriv f x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
inr : ∀ (hf : f x = 0), logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
inr₁ : ∀ (hf : f x ≠ 0), logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x

Tactic:
rcases eq_or_ne (f x) 0 with hf | hf

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x = 0
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x

Tactic:
simp [logDeriv_apply, zero_zpow, *]

Premises used: zero_zpow, logDeriv_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
inr : (↑n : 𝕜') * f x ^ (n - 1) * deriv f x / f x ^ n = (↑n : 𝕜') * (deriv f x / f x)
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x

Tactic:
rw [logDeriv_apply, ← comp_def (· ^ n), deriv_comp _ (differentiableAt_zpow.2 <| .inl hf) hdf,
      deriv_zpow, logDeriv_apply]

Premises used: Iff.mpr, differentiableAt_zpow, deriv_comp, logDeriv_apply, Function.comp_def, deriv_zpow, HPow.hPow, Or.inl
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ (↑n : 𝕜') * f x ^ (n - 1) * deriv f x / f x ^ n = (↑n : 𝕜') * (deriv f x / f x)

Tactic:
simp [field, zpow_sub_one₀ hf]

Premises used: zpow_sub_one₀
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℕ
⊢ logDeriv (fun (x : 𝕜) ↦ f x ^ n) x = (↑n : 𝕜') * logDeriv f x

Tactic:
mod_cast logDeriv_fun_zpow hdf n

Premises used: zpow_natCast, logDeriv, Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, Nat.cast, funext, HPow.hPow, logDeriv_fun_zpow, congrFun', Eq, Eq.trans
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
rw : HMul.hMul (α := 𝕜) (↑n : 𝕜) (logDeriv (fun (x : 𝕜) ↦ x) x) = (↑n : 𝕜) / x
rw₁ : (↑n : 𝕜) * (1 / x) = (↑n : 𝕜) / x
rw₂ rw₃ : (↑n : 𝕜) / x = (↑n : 𝕜) / x
⊢ logDeriv (fun (x : 𝕜) ↦ x ^ n) x = (↑n : 𝕜) / x

Tactic:
rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]

Premises used: logDeriv_id', mul_one_div, logDeriv_fun_zpow
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ logDeriv (fun (x : 𝕜) ↦ x ^ n) x = (↑n : 𝕜) / x

Tactic:
mod_cast logDeriv_zpow x n

Premises used: zpow_natCast, logDeriv, Int.cast, Int.cast_natCast, congrArg, cast, HDiv.hDiv, Nat.cast, funext, HPow.hPow, congrFun', Eq, logDeriv_zpow, Eq.trans
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv (fun (x : 𝕜) ↦ x⁻¹) x = -1 / x

Tactic:
simpa using logDeriv_zpow x (-1)

Premises used: OfNat.ofNat, Neg.neg, logDeriv_zpow
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
simp : deriv f (g x) * deriv g x / f (g x) = deriv f (g x) / f (g x) * deriv g x
⊢ logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x

Tactic:
simp only [logDeriv, Pi.div_apply, deriv_comp _ hf hg, comp_apply]

Premises used: logDeriv, deriv_comp, Pi.div_apply, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ deriv f (g x) * deriv g x / f (g x) = deriv f (g x) / f (g x) * deriv g x

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
inl :
  ∀ (hf : DifferentiableOn 𝕜 f ∅) (hg : DifferentiableOn 𝕜 g ∅)
    (hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hsc : IsPreconnected.{u_1} (α := 𝕜) ∅)
    (hgn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → g x ≠ 0)
    (hfn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → f x ≠ 0),
    EqOn (logDeriv f) (logDeriv g) ∅ ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) ∅
inr : ∀ (t : 𝕜) (ht : t ∈ s), EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨t, ht⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
hf : DifferentiableOn 𝕜 f ∅
hg : DifferentiableOn 𝕜 g ∅
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hsc : IsPreconnected.{u_1} (α := 𝕜) ∅
hgn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → g x ≠ 0
hfn : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) ∅ x → f x ≠ 0
⊢ EqOn (logDeriv f) (logDeriv g) ∅ ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) ∅

Tactic:
simpa using ⟨1, one_ne_zero⟩
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
inr : EqOn (logDeriv f) (logDeriv g) s → ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s
inr₁ : (∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s) → EqOn (logDeriv f) (logDeriv g) s
⊢ EqOn (logDeriv f) (logDeriv g) s ↔ ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
⊢ f t * (g t)⁻¹ ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
inr : ∀ (h : EqOn (logDeriv f) (logDeriv g) s) (y : 𝕜) (hy : y ∈ s), f y = ((f t * (g t)⁻¹) • g) y
⊢ EqOn (logDeriv f) (logDeriv g) s → ∃ (z : 𝕜'), z ≠ 0 ∧ EqOn f (z • g) s

Tactic:
refine fun h ↦ ⟨f t * (g t)⁻¹, by grind, fun y hy ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
z : 𝕜
hz : z ∈ s
rw : deriv f z * g⁻¹ z + f z * deriv g⁻¹ z = (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z
⊢ deriv (f * g⁻¹) z = (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z

Tactic:
rw [deriv_mul (hf.differentiableAt (hs2.mem_nhds hz)) ((hg.differentiableAt
          (hs2.mem_nhds hz)).inv (hgn z hz))]

Premises used: DifferentiableOn.differentiableAt, DifferentiableAt.inv, IsOpen.mem_nhds, deriv_mul
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
z : 𝕜
hz : z ∈ s
⊢ g⁻¹ = (fun (x : 𝕜') ↦ x⁻¹) ∘ g

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
z : 𝕜
hz : z ∈ s
simp :
  deriv f z * (g z)⁻¹ + -(f z * ((HPow.hPow (β := ℕ) (g z) 2)⁻¹ * deriv g z)) =
    deriv f z * (g z)⁻¹ - f z * deriv g z / HPow.hPow (β := ℕ) (g z) 2
⊢ deriv f z * g⁻¹ z + f z * deriv g⁻¹ z = (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z

Tactic:
simp only [Pi.inv_apply, show g⁻¹ = (fun x => x⁻¹) ∘ g by rfl, deriv_inv, neg_mul,
          deriv_comp z (differentiableAt_inv (hgn z hz)) (hg.differentiableAt (hs2.mem_nhds hz)),
          mul_neg, Pi.sub_apply, Pi.mul_apply, comp_apply, Pi.div_apply, Pi.pow_apply]

Premises used: Pi.mul_apply, DifferentiableOn.differentiableAt, deriv_inv, deriv_comp, Pi.div_apply, Pi.pow_apply, IsOpen.mem_nhds, Function.comp_apply, neg_mul, differentiableAt_inv, Pi.inv_apply, mul_neg, Pi.sub_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
z : 𝕜
hz : z ∈ s
⊢ deriv f z * (g z)⁻¹ + -(f z * ((HPow.hPow (β := ℕ) (g z) 2)⁻¹ * deriv g z)) =
    deriv f z * (g z)⁻¹ - f z * deriv g z / HPow.hPow (β := ℕ) (g z) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
⊢ EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) s

Tactic:
have hderiv : s.EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / g ^ 2) := by
        intro z hz
        rw [deriv_mul (hf.differentiableAt (hs2.mem_nhds hz)) ((hg.differentiableAt
          (hs2.mem_nhds hz)).inv (hgn z hz))]
        simp only [Pi.inv_apply, show g⁻¹ = (fun x => x⁻¹) ∘ g by rfl, deriv_inv, neg_mul,
          deriv_comp z (differentiableAt_inv (hgn z hz)) (hg.differentiableAt (hs2.mem_nhds hz)),
          mul_neg, Pi.sub_apply, Pi.mul_apply, comp_apply, Pi.div_apply, Pi.pow_apply]
        ring
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
hderiv : EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) s
z : 𝕜
hz : z ∈ s
simp : deriv f z * (g z)⁻¹ - f z * deriv g z / HPow.hPow (β := ℕ) (g z) 2 = 0
⊢ (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) z = 0 z

Tactic:
simp only [Pi.sub_apply, Pi.mul_apply, Pi.inv_apply, Pi.div_apply, Pi.pow_apply,
          Pi.zero_apply]

Premises used: Pi.mul_apply, Pi.zero_apply, Pi.div_apply, Pi.pow_apply, Pi.inv_apply, Pi.sub_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
hderiv : EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) s
z : 𝕜
hz : z ∈ s
⊢ deriv f z * (g z)⁻¹ - f z * deriv g z / HPow.hPow (β := ℕ) (g z) 2 = 0

Tactic:
grind [logDeriv_apply, Pi.div_apply]

Premises used: logDeriv_apply, Pi.div_apply
-- Module: Mathlib.Analysis.Calculus.LogDeriv
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
hderiv : EqOn (deriv (f * g⁻¹)) (deriv f * g⁻¹ - f * deriv g / HPow.hPow (β := ℕ) g 2) s
⊢ EqOn (deriv (f * g⁻¹)) 0 s

Tactic:
have hfg : EqOn (deriv (f * g⁻¹)) 0 s := hderiv.trans fun z hz ↦ by
        simp only [Pi.sub_apply, Pi.mul_apply, Pi.inv_apply, Pi.div_apply, Pi.pow_apply,
          Pi.zero_apply]
        grind [logDeriv_apply, Pi.div_apply]