θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ tan ψ = (tan θ)⁻¹
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ tan ψ = (tan θ)⁻¹
simp_rw [two_zsmul, ← two_nsmul] at h
no goals
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ tan ψ = (tan θ)⁻¹
exact tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h