awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
nth_rw : θ.sin = sin 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ.sin = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
nth_rw 1 [← sin_zero]

Premises used: Real.Angle.sin_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ = 0 ∨ θ + 0 = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
rw [sin_eq_iff_eq_or_add_eq_pi]

Premises used: Real.Angle.sin_eq_iff_eq_or_add_eq_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ θ = 0 ∨ θ + 0 = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.sin ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
rw₁ rw₂ : θ.sin ≠ 0 ↔ ¬θ.sin = 0
⊢ θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)

Tactic:
rw [← not_or, ← sin_eq_zero_iff]

Premises used: Real.Angle.sin_eq_zero_iff, not_or
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), (-(↑x : Angle)).sin = -(↑x : Angle).sin
⊢ (-θ).sin = -θ.sin

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

Tactic:
Real.sin_neg _

Premises used: Quotient.liftOn', Real.sin_neg, Function.Periodic.lift, Real.Angle.sin, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ (-(↑x : Angle)).sin = -(↑x : Angle).sin

Tactic:
exact Real.sin_neg _

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

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

Tactic:
Real.sin_antiperiodic _

Premises used: Quotient.liftOn', Real.sin_antiperiodic, Function.Periodic.lift, Real.Angle.sin, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) + (↑π : Angle)).sin = -(↑x : Angle).sin

Tactic:
exact Real.sin_antiperiodic _

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

Tactic:
sin_antiperiodic θ

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

Tactic:
sin_antiperiodic.sub_eq θ

Premises used: Function.Antiperiodic.sub_eq, Real.Angle.sin_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : (↑0 : Angle).cos = 1
rw₁ : Real.cos 0 = 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ cos 0 = 1

Tactic:
rw [← coe_zero, cos_coe, Real.cos_zero]

Premises used: Real.Angle.cos_coe, Real.Angle.coe_zero, Real.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : Real.cos π = -1
rw₁ rw₂ : Eq (α := ℝ) (-1) (-1)
⊢ (↑π : Angle).cos = -1

Tactic:
rw [cos_coe, Real.cos_pi]

Premises used: Real.Angle.cos_coe, Real.cos_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), (-(↑x : Angle)).cos = (↑x : Angle).cos
⊢ (-θ).cos = θ.cos

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

Tactic:
Real.cos_neg _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.cos_neg, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ (-(↑x : Angle)).cos = (↑x : Angle).cos

Tactic:
exact Real.cos_neg _

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

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

Tactic:
Real.cos_antiperiodic _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.cos_antiperiodic, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) + (↑π : Angle)).cos = -(↑x : Angle).cos

Tactic:
exact Real.cos_antiperiodic _

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

Tactic:
cos_antiperiodic θ

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

Tactic:
cos_antiperiodic.sub_eq θ

Premises used: Function.Antiperiodic.sub_eq, Real.Angle.cos_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.cos = Real.cos (π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : θ.cos = (↑(π / 2) : Angle).cos ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₂ : θ = (↑(π / 2) : Angle) ∨ θ = -(↑(π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₃ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-(π / 2)) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₄ rw₅ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ θ.cos = 0 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)

Tactic:
rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]

Premises used: neg_div, Real.cos_pi_div_two, Real.Angle.cos_coe, Real.Angle.cos_eq_iff_eq_or_eq_neg, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ₁ θ₂ : Angle
h : ∀ (x : ℝ), ((↑x : Angle) + θ₂).sin = (↑x : Angle).sin * θ₂.cos + (↑x : Angle).cos * θ₂.sin
⊢ (θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin

Tactic:
induction θ₁ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ₂ : Angle
x : ℝ
h :
  ∀ (x_1 : ℝ),
    ((↑x : Angle) + (↑x_1 : Angle)).sin = (↑x : Angle).sin * (↑x_1 : Angle).cos + (↑x : Angle).cos * (↑x_1 : Angle).sin
⊢ ((↑x : Angle) + θ₂).sin = (↑x : Angle).sin * θ₂.cos + (↑x : Angle).cos * θ₂.sin

Tactic:
induction θ₂ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
⊢ ((↑x : Angle) + (↑x_1 : Angle)).sin = (↑x : Angle).sin * (↑x_1 : Angle).cos + (↑x : Angle).cos * (↑x_1 : Angle).sin

Tactic:
Real.sin_add _ _

Premises used: Quotient.liftOn', Real.cos, Real.sin_add, Function.Periodic.lift, Real.Angle.sin, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
⊢ ((↑x : Angle) + (↑x_1 : Angle)).sin = (↑x : Angle).sin * (↑x_1 : Angle).cos + (↑x : Angle).cos * (↑x_1 : Angle).sin

Tactic:
exact Real.sin_add _ _

Premises used: Real.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ₁ θ₂ : Angle
h : ∀ (x : ℝ), (θ₁ + (↑x : Angle)).cos = θ₁.cos * (↑x : Angle).cos - θ₁.sin * (↑x : Angle).sin
⊢ (θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin

Tactic:
induction θ₂ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ₁ : Angle
x : ℝ
h :
  ∀ (x_1 : ℝ),
    ((↑x_1 : Angle) + (↑x : Angle)).cos = (↑x_1 : Angle).cos * (↑x : Angle).cos - (↑x_1 : Angle).sin * (↑x : Angle).sin
⊢ (θ₁ + (↑x : Angle)).cos = θ₁.cos * (↑x : Angle).cos - θ₁.sin * (↑x : Angle).sin

Tactic:
induction θ₁ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
⊢ ((↑x_1 : Angle) + (↑x : Angle)).cos = (↑x_1 : Angle).cos * (↑x : Angle).cos - (↑x_1 : Angle).sin * (↑x : Angle).sin

Tactic:
Real.cos_add _ _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.cos_add, Real.Angle.sin, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
⊢ ((↑x_1 : Angle) + (↑x : Angle)).cos = (↑x_1 : Angle).cos * (↑x : Angle).cos - (↑x_1 : Angle).sin * (↑x : Angle).sin

Tactic:
exact Real.cos_add _ _

Premises used: Real.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 θ).sin = HSMul.hSMul (α := ℕ) 2 (θ.sin * θ.cos)

Tactic:
simp [two_nsmul, two_mul, sin_add, mul_comm]

Premises used: two_mul, Real.Angle.sin_add, mul_comm, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), HPow.hPow (β := ℕ) (↑x : Angle).cos 2 + HPow.hPow (β := ℕ) (↑x : Angle).sin 2 = 1
⊢ HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2 = 1

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (↑x : Angle).cos 2 + HPow.hPow (β := ℕ) (↑x : Angle).sin 2 = 1

Tactic:
Real.cos_sq_add_sin_sq _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.cos_sq_add_sin_sq, Real.Angle.sin, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (↑x : Angle).cos 2 + HPow.hPow (β := ℕ) (↑x : Angle).sin 2 = 1

Tactic:
exact Real.cos_sq_add_sin_sq _

Premises used: Real.cos_sq_add_sin_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), ((↑x : Angle) + (↑(π / 2) : Angle)).sin = (↑x : Angle).cos
⊢ (θ + (↑(π / 2) : Angle)).sin = θ.cos

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

Tactic:
Real.sin_add_pi_div_two _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.sin_add_pi_div_two, Real.Angle.sin, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) + (↑(π / 2) : Angle)).sin = (↑x : Angle).cos

Tactic:
exact Real.sin_add_pi_div_two _

Premises used: Real.sin_add_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), ((↑x : Angle) - (↑(π / 2) : Angle)).sin = -(↑x : Angle).cos
⊢ (θ - (↑(π / 2) : Angle)).sin = -θ.cos

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) - (↑(π / 2) : Angle)).sin = -(↑x : Angle).cos

Tactic:
Real.sin_sub_pi_div_two _

Premises used: Quotient.liftOn', Real.cos, Real.sin_sub_pi_div_two, Function.Periodic.lift, Real.Angle.sin, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) - (↑(π / 2) : Angle)).sin = -(↑x : Angle).cos

Tactic:
exact Real.sin_sub_pi_div_two _

Premises used: Real.sin_sub_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), ((↑(π / 2) : Angle) - (↑x : Angle)).sin = (↑x : Angle).cos
⊢ ((↑(π / 2) : Angle) - θ).sin = θ.cos

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑(π / 2) : Angle) - (↑x : Angle)).sin = (↑x : Angle).cos

Tactic:
Real.sin_pi_div_two_sub _

Premises used: Quotient.liftOn', Real.cos, Real.sin_pi_div_two_sub, Function.Periodic.lift, Real.Angle.sin, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑(π / 2) : Angle) - (↑x : Angle)).sin = (↑x : Angle).cos

Tactic:
exact Real.sin_pi_div_two_sub _

Premises used: Real.sin_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), ((↑x : Angle) + (↑(π / 2) : Angle)).cos = -(↑x : Angle).sin
⊢ (θ + (↑(π / 2) : Angle)).cos = -θ.sin

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

Tactic:
Real.cos_add_pi_div_two _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.cos_add_pi_div_two, Real.Angle.sin, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) + (↑(π / 2) : Angle)).cos = -(↑x : Angle).sin

Tactic:
exact Real.cos_add_pi_div_two _

Premises used: Real.cos_add_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), ((↑x : Angle) - (↑(π / 2) : Angle)).cos = (↑x : Angle).sin
⊢ (θ - (↑(π / 2) : Angle)).cos = θ.sin

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) - (↑(π / 2) : Angle)).cos = (↑x : Angle).sin

Tactic:
Real.cos_sub_pi_div_two _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.Angle.sin, Real.cos_sub_pi_div_two, Real.sin, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑x : Angle) - (↑(π / 2) : Angle)).cos = (↑x : Angle).sin

Tactic:
exact Real.cos_sub_pi_div_two _

Premises used: Real.cos_sub_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), ((↑(π / 2) : Angle) - (↑x : Angle)).cos = (↑x : Angle).sin
⊢ ((↑(π / 2) : Angle) - θ).cos = θ.sin

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑(π / 2) : Angle) - (↑x : Angle)).cos = (↑x : Angle).sin

Tactic:
Real.cos_pi_div_two_sub _

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, Real.Angle.sin, Real.sin, Real.cos_pi_div_two_sub, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ ((↑(π / 2) : Angle) - (↑x : Angle)).cos = (↑x : Angle).sin

Tactic:
exact Real.cos_pi_div_two_sub _

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

Tactic:
rw [two_nsmul_eq_iff] at h

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

Tactic:
rcases h with (rfl | rfl)

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

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
inr : |(-ψ.sin)| = |ψ.sin|
inr₁ inr₂ : |ψ.sin| = |ψ.sin|
⊢ |(ψ + (↑π : Angle)).sin| = |ψ.sin|

Tactic:
rw [sin_add_pi, abs_neg]

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

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 ψ
⊢ |θ.sin| = |ψ.sin|

Tactic:
abs_sin_eq_of_two_nsmul_eq h

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

Tactic:
exact abs_sin_eq_of_two_nsmul_eq h

Premises used: Real.Angle.abs_sin_eq_of_two_nsmul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + (↑π : Angle)
inl : |θ.cos| = |θ.cos|
inr : |(ψ + (↑π : Angle)).cos| = |ψ.cos|
⊢ |θ.cos| = |ψ.cos|

Tactic:
rcases h with (rfl | rfl)

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

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
inr : |(-ψ.cos)| = |ψ.cos|
inr₁ inr₂ : |ψ.cos| = |ψ.cos|
⊢ |(ψ + (↑π : Angle)).cos| = |ψ.cos|

Tactic:
rw [cos_add_pi, abs_neg]

Premises used: abs_neg, Real.Angle.cos_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
⊢ |θ.cos| = |ψ.cos|

Tactic:
abs_cos_eq_of_two_nsmul_eq h

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

Tactic:
exact abs_cos_eq_of_two_nsmul_eq h

Premises used: Real.Angle.abs_cos_eq_of_two_nsmul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
rw : ∃ (k : ℤ), toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)
⊢ (↑(toIcoMod two_pi_pos ψ θ) : Angle) = (↑θ : Angle)

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub]

Premises used: Real.Angle.angle_eq_iff_two_pi_dvd_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
⊢ ∃ (k : ℤ), toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)

Tactic:
⟨-toIcoDiv two_pi_pos ψ θ, ?_⟩

Premises used: toIcoDiv, Real.two_pi_pos, Exists.intro, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
refine : toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
⊢ ∃ (k : ℤ), toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)

Tactic:
refine ⟨-toIcoDiv two_pi_pos ψ θ, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
rw : -toIcoDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
rw₁ : (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ) * (2 * π) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
rw₂ rw₃ : 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)

Tactic:
rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]

Premises used: zsmul_eq_mul, toIcoMod_sub_self, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
rw : ∃ (k : ℤ), toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)
⊢ (↑(toIocMod two_pi_pos ψ θ) : Angle) = (↑θ : Angle)

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub]

Premises used: Real.Angle.angle_eq_iff_two_pi_dvd_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
⊢ ∃ (k : ℤ), toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)

Tactic:
⟨-toIocDiv two_pi_pos ψ θ, ?_⟩

Premises used: Real.two_pi_pos, Exists.intro, toIocDiv, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
refine : toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
⊢ ∃ (k : ℤ), toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)

Tactic:
refine ⟨-toIocDiv two_pi_pos ψ θ, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
rw : -toIocDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
rw₁ : (↑(-toIocDiv two_pi_pos ψ θ) : ℝ) * (2 * π) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
rw₂ rw₃ : 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)

Tactic:
rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]

Premises used: zsmul_eq_mul, toIocMod_sub_self, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ (↑θ : Angle).toReal = toIocMod two_pi_pos (-π) θ

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, toIocMod, Real.Angle.toReal, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
rw : θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
⊢ (↑θ : Angle).toReal = θ ↔ -π < θ ∧ θ ≤ π

Tactic:
rw [toReal_coe, toIocMod_eq_self two_pi_pos]

Premises used: toIocMod_eq_self, Real.Angle.toReal_coe, Real.two_pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
ring_nf : θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
rw : -π < θ ∧ θ ≤ π ↔ θ ∈ Set.Ioc (-π) π
rw₁ rw₂ : θ ∈ Set.Ioc (-π) π ↔ θ ∈ Set.Ioc (-π) π
⊢ (↑θ : Angle).toReal = θ ↔ θ ∈ Set.Ioc (-π) π

Tactic:
rw [toReal_coe_eq_self_iff, ← Set.mem_Ioc]

Premises used: Real.Angle.toReal_coe_eq_self_iff, Set.mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : θ.toReal = ψ.toReal
h₁ : ∀ (x : ℝ) (h : (↑x : Angle).toReal = ψ.toReal), (↑x : Angle) = ψ
⊢ θ = ψ

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
ψ : Angle
x : ℝ
h : (↑x : Angle).toReal = ψ.toReal
h₁ : ∀ (x_1 : ℝ) (h : (↑x : Angle).toReal = (↑x_1 : Angle).toReal), (↑x : Angle) = (↑x_1 : Angle)
⊢ (↑x : Angle) = ψ

Tactic:
induction ψ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x x_1 : ℝ
h : (↑x : Angle).toReal = (↑x_1 : Angle).toReal
⊢ (↑x : Angle) = (↑x_1 : Angle)

Tactic:
simpa [toReal_coe, toIocMod_eq_toIocMod, zsmul_eq_mul, mul_comm _ (2 * π), ←
    angle_eq_iff_two_pi_dvd_sub, eq_comm] using h

Premises used: zsmul_eq_mul, Real.pi, HMul.hMul, Real.Angle.toReal_coe, Real.Angle.angle_eq_iff_two_pi_dvd_sub, eq_comm, toIocMod_eq_toIocMod, mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
⊢ θ.toReal = ψ.toReal ↔ θ = ψ

Tactic:
toReal_injective.eq_iff

Premises used: Function.Injective.eq_iff, Real.Angle.toReal_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), (↑(↑x : Angle).toReal : Angle) = (↑x : Angle)
⊢ (↑θ.toReal : Angle) = θ

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

Tactic:
coe_toIocMod _ _

Premises used: Quotient.liftOn', Function.Periodic.lift, Real.Angle.coe_toIocMod, toIocMod, Real.Angle.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ (↑(↑x : Angle).toReal : Angle) = (↑x : Angle)

Tactic:
exact coe_toIocMod _ _

Premises used: Real.Angle.coe_toIocMod
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), -π < (↑x : Angle).toReal
⊢ -π < θ.toReal

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ -π < (↑x : Angle).toReal

Tactic:
left_lt_toIocMod _ _ _

Premises used: Quotient.liftOn', left_lt_toIocMod, Function.Periodic.lift, toIocMod, Real.Angle.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ -π < (↑x : Angle).toReal

Tactic:
exact left_lt_toIocMod _ _ _

Premises used: left_lt_toIocMod
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), (↑x : Angle).toReal ≤ π
⊢ θ.toReal ≤ π

Tactic:
induction θ using Real.Angle.induction_on
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ toIocMod two_pi_pos (-π) x ≤ -π + 2 * π

Tactic:
toIocMod_le_right two_pi_pos _ _

Premises used: Real.two_pi_pos, toIocMod_le_right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
h : π = -π + 2 * π
⊢ (↑x : Angle).toReal ≤ π

Tactic:
convert! toIocMod_le_right two_pi_pos _ _

Premises used: Real.two_pi_pos, toIocMod_le_right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ π = -π + 2 * π

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ |θ.toReal| ≤ π

Tactic:
abs_le.2 ⟨(neg_pi_lt_toReal _).le, toReal_le_pi _⟩

Premises used: Iff.mpr, abs_le, Real.Angle.neg_pi_lt_toReal, LT.lt.le, And.intro, Real.Angle.toReal_le_pi