case h.e'_7
x : ℂ
h : cos x ≠ 0
⊢ ↑1 / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (↑1 / cos x ^ 2) x
convert (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1
case h.e'_7
x : ℂ
h : ¬cos x = 0
⊢ (sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
case h.e'_7
x : ℂ
h : cos x ≠ 0
⊢ ↑1 / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
rw_mod_cast [← sin_sq_add_cos_sq x]
no goals
case h.e'_7
x : ℂ
h : ¬cos x = 0
⊢ (sin x ^ 2 + cos x ^ 2) / cos x ^ 2 = (cos x * cos x - sin x * -sin x) / cos x ^ 2
ring