x✝ y x : ℂ
hx : cos x ≠ 0
this : cos x ^ 2 ≠ 0
⊢ (1 + tan x ^ 2)⁻¹ = cos x ^ 2
x✝ y x : ℂ
hx : cos x ≠ 0
⊢ (1 + tan x ^ 2)⁻¹ = cos x ^ 2
have : cos x ^ 2 ≠ 0 := pow_ne_zero 2 hx
x✝ y x : ℂ
hx : cos x ≠ 0
this : cos x ^ 2 ≠ 0
⊢ (1 + sin x ^ 2 / cos x ^ 2)⁻¹ = cos x ^ 2
x✝ y x : ℂ
hx : cos x ≠ 0
this : cos x ^ 2 ≠ 0
⊢ (1 + tan x ^ 2)⁻¹ = cos x ^ 2
rw [tan_eq_sin_div_cos, div_pow]
no goals
x✝ y x : ℂ
hx : cos x ≠ 0
this : cos x ^ 2 ≠ 0
⊢ (1 + sin x ^ 2 / cos x ^ 2)⁻¹ = cos x ^ 2
field_simp [this]