x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = ↑1 / cos x ^ 2
x : ℝ
h : cos x = 0
⊢ deriv tan x = ↑1 / cos x ^ 2
have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
no goals
x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = ↑1 / cos x ^ 2
simp [deriv_zero_of_not_differentiableAt this, h, sq]