tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi

English

If 2θ + 2ψ = π, then tan ψ = (tan θ)^{-1}.

Русский

Если 2θ + 2ψ = π, тогда tan ψ = (tan θ)^{-1}.

LaTeX

$$$(2:\mathbb{N})\cdot \theta + (2:\mathbb{N})\cdot \psi = \pi \Rightarrow \tan\psi = (\tan\theta)^{-1}$$$

Lean4

theorem tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi {θ ψ : Angle} (h : (2 : ℕ) • θ + (2 : ℕ) • ψ = π) :
    tan ψ = (tan θ)⁻¹ := by
  induction θ using Real.Angle.induction_on
  induction ψ using Real.Angle.induction_on
  rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h
  rcases h with ⟨k, h⟩
  rw [sub_eq_iff_eq_add, ← mul_inv_cancel_left₀ two_ne_zero π, mul_assoc, ← mul_add, mul_right_inj' (two_ne_zero' ℝ), ←
    eq_sub_iff_add_eq', mul_inv_cancel_left₀ two_ne_zero π, inv_mul_eq_div, mul_comm] at h
  rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]
  exact Real.tan_periodic.int_mul _ _

Похожие утверждения