Theorem: DifferentiableAt.deriv_eq_deriv_pow_div_pow (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
Tactic:
have h1 : g z ≠ 0 := λ h => fz_nonzero (by simp [Eventually.self_of_nhds hg, h, n_pos.ne.symm])
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
Tactic:
have h2 : n * (g z) ^ (n - 1) ≠ 0 := by simp [pow_ne_zero, h1, n_pos.ne.symm]
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
Tactic:
rw [(EventuallyEq.deriv hg).self_of_nhds, deriv_pow'' _ g_diff, eq_div_iff h2]
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z * (↑n * g z ^ (n - 1)) = ↑n * g z ^ (n - 1) * deriv g z

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z * (↑n * g z ^ (n - 1)) = ↑n * g z ^ (n - 1) * deriv g z
Tactic:
ring
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h : g z = 0
⊢ f z = 0
Tactic:
simp [Eventually.self_of_nhds hg, h, n_pos.ne.symm]
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
⊢ ↑n * g z ^ (n - 1) ≠ 0
Tactic:
simp [pow_ne_zero, h1, n_pos.ne.symm]
State after:
no goals