awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
linarith : -π / 2 < θ.toReal → 2 / 2 = 1
linarith₁ : -π / 2 < θ.toReal → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -π / 2 < θ.toReal → GT.gt (α := ℝ) 2 0
linarith₃ : -π / 2 < θ.toReal → 2 * θ.toReal - -π + (-(1 * π) - 2 * θ.toReal) = 0
⊢ θ.toReal ≤ -π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ.toReal ≤ -π / 2
linarith : 2 * θ.toReal ≤ -3 * π → 2 / 2 = 1
linarith₁ : 2 * θ.toReal ≤ -3 * π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * θ.toReal ≤ -3 * π → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * θ.toReal ≤ -3 * π → 2 * θ.toReal - -3 * π + (0 - π) + 2 * (-π - θ.toReal) = 0
linarith₄ : 2 * θ.toReal ≤ -3 * π → GT.gt (α := ℝ) 2 0
⊢ -3 * π < 2 * θ.toReal

Tactic:
linarith [pi_pos, neg_pi_lt_toReal θ]

Premises used: Real.Angle.neg_pi_lt_toReal, Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2

Tactic:
refine
    ⟨fun h => by linarith, fun h =>
      ⟨by linarith [pi_pos, neg_pi_lt_toReal θ], (le_div_iff₀' (zero_lt_two' ℝ)).1 h⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
rw₂ rw₃ : θ.toReal ≤ -π / 2 ↔ θ.toReal ≤ -π / 2
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_add_two_pi]

Premises used: Real.Angle.two_nsmul_toReal_eq_two_mul_add_two_pi, two_zsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : Real.sin θ.toReal
| θ.sin

Tactic:
rw [← coe_toReal θ, sin_coe]

Premises used: Real.Angle.coe_toReal, Real.Angle.sin_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
conv_rhs : Real.sin θ.toReal = θ.sin
conv_rhs₁ : Real.sin θ.toReal = Real.sin θ.toReal
⊢ Real.sin θ.toReal = θ.sin

Tactic:
conv_rhs => rw [← coe_toReal θ, sin_coe]

Premises used: Real.Angle.coe_toReal, Real.Angle.sin_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : Real.cos θ.toReal
| θ.cos

Tactic:
rw [← coe_toReal θ, cos_coe]

Premises used: Real.Angle.coe_toReal, Real.Angle.cos_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
conv_rhs : Real.cos θ.toReal = θ.cos
conv_rhs₁ : Real.cos θ.toReal = Real.cos θ.toReal
⊢ Real.cos θ.toReal = θ.cos

Tactic:
conv_rhs => rw [← coe_toReal θ, cos_coe]

Premises used: Real.Angle.coe_toReal, Real.Angle.cos_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ 0 < π / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ 0 < π / 2

Tactic:
have : 0 < π / 2 := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
this : 0 < π / 2
⊢ θ.toReal ∈ Set.Ioc (-π) π

Tactic:
have := toReal_mem_Ioc θ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
this_1 : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
rw : 0 ≤ Real.cos |θ.toReal| ↔ |θ.toReal| ≤ π / 2
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
rw [← cos_toReal, ← cos_abs]

Premises used: Real.Angle.cos_toReal, Real.cos_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
this_1 : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ Real.cos |θ.toReal| ↔ |θ.toReal| ≤ π / 2

Tactic:
grind [cos_neg_of_pi_div_two_lt_of_lt, cos_nonneg_of_mem_Icc]

Premises used: Real.cos_neg_of_pi_div_two_lt_of_lt, Real.cos_nonneg_of_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : |θ.toReal| ≤ π / 2 → (|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos)
⊢ 0 < θ.cos ↔ |θ.toReal| < π / 2

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_and_ne, cos_nonneg_iff_abs_toReal_le_pi_div_two, ←
    and_congr_right]

Premises used: lt_iff_le_and_ne, Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two, and_congr_right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
contrapose : |θ.toReal| = π / 2 ↔ 0 = θ.cos
⊢ |θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos

Tactic:
contrapose
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : |θ.toReal| = π / 2 ↔ θ.cos = 0
rw₁ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ.cos = 0
rw₂ rw₃ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ |θ.toReal| = π / 2 ↔ 0 = θ.cos

Tactic:
rw [@eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]

Premises used: Real.Angle.abs_toReal_eq_pi_div_two_iff, Real.Angle.cos_eq_zero_iff, eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
this : θ ≠ ψ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ ↔ θ = ψ

Tactic:
simp [this, two_nsmul_eq_iff]

Premises used: Real.Angle.two_nsmul_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
suffices : θ ≠ ψ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ ↔ θ = ψ

Tactic:
suffices θ ≠ ψ + π by simp [this, two_nsmul_eq_iff]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
hψ : |ψ.toReal| < π / 2
hθ : |(ψ + (↑π : Angle)).toReal| < π / 2
⊢ 0 < -ψ.cos

Tactic:
simp only [← cos_pos_iff_abs_toReal_lt_pi_div_two, cos_add_pi] at hθ hψ

Premises used: Real.Angle.cos_add_pi, Real.Angle.cos_pos_iff_abs_toReal_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
hψ : |ψ.toReal| < π / 2
hθ : |(ψ + (↑π : Angle)).toReal| < π / 2
hθ₁ : 0 < -ψ.cos
⊢ 0 < ψ.cos

Tactic:
simp only [← cos_pos_iff_abs_toReal_lt_pi_div_two, cos_add_pi] at hθ hψ

Premises used: Real.Angle.cos_add_pi, Real.Angle.cos_pos_iff_abs_toReal_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
hθ : 0 < -ψ.cos
hψ : 0 < ψ.cos
⊢ False

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
simp_rw : θ + θ = ψ + ψ ↔ θ = ψ
simp_rw₁ : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ ↔ θ = ψ
⊢ HSMul.hSMul (α := ℤ) 2 θ = HSMul.hSMul (α := ℤ) 2 ψ ↔ θ = ψ

Tactic:
simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two hθ hψ]

Premises used: Real.Angle.two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two, two_zsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
contrapose! : 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
⊢ θ.cos < 0 ↔ π / 2 < |θ.toReal|

Tactic:
contrapose!
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
cos_nonneg_iff_abs_toReal_le_pi_div_two

Premises used: Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
exact cos_nonneg_iff_abs_toReal_le_pi_div_two

Premises used: Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ θ = (↑(π / 2) : Angle) - ψ ∨ θ = (↑(π / 2) : Angle) - ψ + (↑π : Angle)

Tactic:
rw [← eq_sub_iff_add_eq, ← two_nsmul_coe_div_two, ← nsmul_sub, two_nsmul_eq_iff] at h

Premises used: nsmul_sub, eq_sub_iff_add_eq, Real.Angle.two_nsmul_coe_div_two, Real.Angle.two_nsmul_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : θ = (↑(π / 2) : Angle) - ψ ∨ θ = (↑(π / 2) : Angle) - ψ + (↑π : Angle)
inl : |((↑(π / 2) : Angle) - ψ).cos| = |ψ.sin|
inr : |((↑(π / 2) : Angle) - ψ + (↑π : Angle)).cos| = |ψ.sin|
⊢ |θ.cos| = |ψ.sin|

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
⊢ |((↑(π / 2) : Angle) - ψ).cos| = |ψ.sin|

Tactic:
simp [cos_pi_div_two_sub]

Premises used: Real.Angle.cos_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
⊢ |((↑(π / 2) : Angle) - ψ + (↑π : Angle)).cos| = |ψ.sin|

Tactic:
simp [cos_pi_div_two_sub]

Premises used: Real.Angle.cos_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 θ + HSMul.hSMul (α := ℤ) 2 ψ = (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)

Tactic:
simp_rw [two_zsmul, ← two_nsmul] at h

Premises used: two_zsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ |θ.cos| = |ψ.sin|

Tactic:
abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi h

Premises used: Real.Angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ |θ.cos| = |ψ.sin|

Tactic:
exact abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi h

Premises used: Real.Angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ θ.tan = θ.sin / θ.cos

Tactic:
rfl

Premises used: Real.Angle.tan, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
rw : (↑x : Angle).sin / (↑x : Angle).cos = Real.tan x
rw₁ : Real.sin x / (↑x : Angle).cos = Real.tan x
rw₂ : Real.sin x / Real.cos x = Real.tan x
rw₃ rw₄ : Real.sin x / Real.cos x = Real.sin x / Real.cos x
⊢ (↑x : Angle).tan = Real.tan x

Tactic:
rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]

Premises used: Real.Angle.tan, Real.Angle.sin_coe, Real.Angle.cos_coe, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : (↑0 : Angle).tan = 0
rw₁ : Real.tan 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ tan 0 = 0

Tactic:
rw [← coe_zero, tan_coe, Real.tan_zero]

Premises used: Real.Angle.coe_zero, Real.tan_zero, Real.Angle.tan_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : Real.tan π = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (↑π : Angle).tan = 0

Tactic:
rw [tan_coe, Real.tan_pi]

Premises used: Real.tan_pi, Real.Angle.tan_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), ((↑x : Angle) + (↑π : Angle)).tan = (↑x : Angle).tan
⊢ (θ + (↑π : Angle)).tan = θ.tan

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
h : Real.tan (x + π) = Real.tan x
⊢ ((↑x : Angle) + (↑π : Angle)).tan = (↑x : Angle).tan

Tactic:
rw [← coe_add, tan_coe, tan_coe]

Premises used: Real.Angle.coe_add, Real.Angle.tan_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ Real.tan (x + π) = Real.tan x

Tactic:
Real.tan_periodic _

Premises used: Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ Real.tan (x + π) = Real.tan x

Tactic:
exact Real.tan_periodic _

Premises used: Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (θ + (↑π : Angle)).tan = θ.tan

Tactic:
tan_periodic θ

Premises used: Real.Angle.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (θ - (↑π : Angle)).tan = θ.tan

Tactic:
tan_periodic.sub_eq θ

Premises used: Real.Angle.tan_periodic, Function.Periodic.sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : Real.tan θ.toReal
| θ.tan

Tactic:
rw [← coe_toReal θ, tan_coe]

Premises used: Real.Angle.coe_toReal, Real.Angle.tan_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
conv_rhs : Real.tan θ.toReal = θ.tan
conv_rhs₁ : Real.tan θ.toReal = Real.tan θ.toReal
⊢ Real.tan θ.toReal = θ.tan

Tactic:
conv_rhs => rw [← coe_toReal θ, tan_coe]

Premises used: Real.Angle.coe_toReal, Real.Angle.tan_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + (↑π : Angle)
inl : θ.tan = θ.tan
inr : (ψ + (↑π : Angle)).tan = ψ.tan
⊢ θ.tan = ψ.tan

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ θ.tan = θ.tan

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
⊢ (ψ + (↑π : Angle)).tan = ψ.tan

Tactic:
tan_add_pi _

Premises used: Real.Angle.tan_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
⊢ (ψ + (↑π : Angle)).tan = ψ.tan

Tactic:
exact tan_add_pi _

Premises used: Real.Angle.tan_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
⊢ θ.tan = ψ.tan

Tactic:
tan_eq_of_two_nsmul_eq h

Premises used: Real.Angle.tan_eq_of_two_nsmul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
⊢ θ.tan = ψ.tan

Tactic:
exact tan_eq_of_two_nsmul_eq h

Premises used: Real.Angle.tan_eq_of_two_nsmul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
h₁ :
  ∀ (x : ℝ) (h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)),
    ψ.tan = (↑x : Angle).tan⁻¹
⊢ ψ.tan = θ.tan⁻¹

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
x : ℝ
h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
h₁ :
  ∀ (x_1 : ℝ) (h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 (↑x_1 : Angle) = (↑π : Angle)),
    (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
⊢ ψ.tan = (↑x : Angle).tan⁻¹

Tactic:
induction ψ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 (↑x_1 : Angle) = (↑π : Angle)
⊢ ∃ (k : ℤ), 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)

Tactic:
rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h

Premises used: Real.Angle.coe_add, two_mul, Real.Angle.angle_eq_iff_two_pi_dvd_sub, Real.Angle.coe_nsmul, smul_add, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
h : ∃ (k : ℤ), 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)
h₁ : ∀ (k : ℤ) (h : 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)), (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
⊢ (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹

Tactic:
rcases h with ⟨k, h⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
k : ℤ
h : 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)
⊢ x_1 = (↑k : ℝ) * π + π / 2 - x

Tactic:
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

Premises used: eq_sub_iff_add_eq', mul_inv_cancel_left₀, Real, Real.pi, mul_assoc, inv_mul_eq_div, two_ne_zero, two_ne_zero', sub_eq_iff_eq_add, mul_comm, mul_add, mul_right_inj'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
k : ℤ
h : x_1 = (↑k : ℝ) * π + π / 2 - x
h₁ : Real.tan (π / 2 - x + (↑k : ℝ) * π) = Real.tan (π / 2 - x)
⊢ (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹

Tactic:
rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]

Premises used: add_sub_assoc, Real.tan_pi_div_two_sub, add_comm, Real.Angle.tan_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
k : ℤ
h : x_1 = (↑k : ℝ) * π + π / 2 - x
⊢ Real.tan (π / 2 - x + (↑k : ℝ) * π) = Real.tan (π / 2 - x)

Tactic:
Real.tan_periodic.int_mul _ _

Premises used: Function.Periodic.int_mul, Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
k : ℤ
h : x_1 = (↑k : ℝ) * π + π / 2 - x
⊢ Real.tan (π / 2 - x + (↑k : ℝ) * π) = Real.tan (π / 2 - x)

Tactic:
exact Real.tan_periodic.int_mul _ _

Premises used: Function.Periodic.int_mul, Real.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ ψ.tan = θ.tan⁻¹

Tactic:
tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h

Premises used: Real.Angle.tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ ψ.tan = θ.tan⁻¹

Tactic:
exact tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h

Premises used: Real.Angle.tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (sin 0) : SignType) (0 : SignType)
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 0 : SignType) (0 : SignType)
rw₂ rw₃ : Eq (α := SignType) 0 0
⊢ sign 0 = 0

Tactic:
rw [sign, sin_zero, _root_.sign_zero]

Premises used: sign_zero, Real.Angle.sign, Real.Angle.sin_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑π : Angle).sin : SignType) (0 : SignType)
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 0 : SignType) (0 : SignType)
rw₂ rw₃ : Eq (α := SignType) 0 0
⊢ (↑π : Angle).sign = 0

Tactic:
rw [sign, sin_coe_pi, _root_.sign_zero]

Premises used: sign_zero, Real.Angle.sin_coe_pi, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
simp_rw :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ).sin : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
simp_rw₁ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ.sin) : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
⊢ (-θ).sign = -θ.sign

Tactic:
simp_rw [sign, sin_neg, Left.sign_neg]

Premises used: Real.Angle.sin_neg, Real.Angle.sign, Left.sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : (SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin = -θ.sign
rw₁ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
rw₂ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ.sin) : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
rw₃ rw₄ :
  Eq (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
⊢ (θ + (↑π : Angle)).sign = -θ.sign

Tactic:
rw [sign, sign, sin_add_pi, Left.sign_neg]

Premises used: Real.Angle.sin_add_pi, Real.Angle.sign, Left.sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (θ + (↑π : Angle)).sign = -θ.sign

Tactic:
sign_antiperiodic θ

Premises used: Real.Angle.sign_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : (θ + (↑π : Angle)).sign = -θ.sign
rw₁ rw₂ : -θ.sign = -θ.sign
⊢ ((↑π : Angle) + θ).sign = -θ.sign

Tactic:
rw [add_comm, sign_add_pi]

Premises used: add_comm, Real.Angle.sign_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (θ - (↑π : Angle)).sign = -θ.sign

Tactic:
sign_antiperiodic.sub_eq θ

Premises used: Function.Antiperiodic.sub_eq, Real.Angle.sign_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ ((↑π : Angle) - θ).sign = θ.sign

Tactic:
simp [sign_antiperiodic.sub_eq']

Premises used: Function.Antiperiodic.sub_eq', Real.Angle.sign_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType) (0 : SignType) ↔ θ = 0 ∨ θ = (↑π : Angle)
rw₁ : θ.sin = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
rw₂ rw₃ : θ = 0 ∨ θ = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ.sign = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
rw [sign, _root_.sign_eq_zero_iff, sin_eq_zero_iff]

Premises used: Real.Angle.sin_eq_zero_iff, Real.Angle.sign, sign_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.sign ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
rw₁ rw₂ : θ.sign ≠ 0 ↔ ¬θ.sign = 0
⊢ θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)

Tactic:
rw [← not_or, ← sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, not_or
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.toReal < 0 ↔ Real.sin θ.toReal < 0
⊢ θ.toReal < 0 ↔ θ.sign = -1

Tactic:
rw [sign, ← sin_toReal, sign_eq_neg_one_iff]

Premises used: Real.Angle.sign, Real.Angle.sin_toReal, sign_eq_neg_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Tactic:
grind [sin_nonneg_of_nonneg_of_le_pi, sin_neg_of_neg_of_neg_pi_lt, toReal_mem_Ioc]

Premises used: Real.Angle.toReal_mem_Ioc, Real.sin_nonneg_of_nonneg_of_le_pi, Real.sin_neg_of_neg_of_neg_pi_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
simp : 0 ≤ θ.toReal ↔ 0 ≤ Real.sin θ.toReal
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign

Tactic:
simp only [sign, ← sin_toReal, sign_nonneg_iff]

Premises used: sign_nonneg_iff, Real.Angle.sign, Real.Angle.sin_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ 0 ≤ θ.toReal ↔ 0 ≤ Real.sin θ.toReal

Tactic:
grind [sin_nonneg_of_nonneg_of_le_pi, sin_neg_of_neg_of_neg_pi_lt, toReal_mem_Ioc]

Premises used: Real.Angle.toReal_mem_Ioc, Real.sin_nonneg_of_nonneg_of_le_pi, Real.sin_neg_of_neg_of_neg_pi_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
inl : ∀ (ht : θ.toReal < 0), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
inr : ∀ (ht : θ.toReal = 0), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
inr₁ : ∀ (ht : 0 < θ.toReal), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign

Tactic:
rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)

Premises used: OfNat.ofNat, Real.Angle.toReal, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
ht : θ.toReal < 0
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign

Tactic:
simp [ht, toReal_neg_iff_sign_neg.1 ht]

Premises used: Real.Angle.toReal_neg_iff_sign_neg, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
ht : θ.toReal = 0
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign

Tactic:
simp [sign, ht, ← sin_toReal]

Premises used: Real.Angle.sign, Real.Angle.sin_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
ht : 0 < θ.toReal
inr :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
    ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
inr₁ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (Real.sin θ.toReal) : SignType)
inr₂ : Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin θ.toReal) : SignType)
inr₃ inr₄ : Eq (α := SignType) 1 1
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign

Tactic:
rw [sign, ← sin_toReal, sign_pos ht,
      sign_pos
        (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]

Premises used: Iff.mpr, Real.Angle.toReal_eq_pi_iff, sign_pos, Iff.not, Real.sin_pos_of_pos_of_lt_pi, LE.le.lt_of_ne, Real.Angle.sign, Real.Angle.toReal_le_pi, Real.Angle.sin_toReal