awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
mp : cos θ = cos ψ → (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
mpr : (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle) → cos θ = cos ψ
⊢ cos θ = cos ψ ↔ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
⊢ (∃ (n : ℤ), (↑n : ℝ) * π = (θ + ψ) / 2) ∨ ∃ (n : ℤ), (↑n : ℝ) * π = (θ - ψ) / 2

Tactic:
rw [← sub_eq_zero, cos_sub_cos, mul_eq_zero, mul_eq_zero, neg_eq_zero,
      eq_false (two_ne_zero' ℝ), false_or, sin_eq_zero_iff, sin_eq_zero_iff] at Hcos

Premises used: Real, eq_false, sub_eq_zero, neg_eq_zero, false_or, mul_eq_zero, two_ne_zero', Real.cos_sub_cos, Real.sin_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : (∃ (n : ℤ), (↑n : ℝ) * π = (θ + ψ) / 2) ∨ ∃ (n : ℤ), (↑n : ℝ) * π = (θ - ψ) / 2
mp : ∀ (n : ℤ) (hn : (↑n : ℝ) * π = (θ + ψ) / 2), (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
mp₁ : ∀ (n : ℤ) (hn : (↑n : ℝ) * π = (θ - ψ) / 2), (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)

Tactic:
rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ + ψ) / 2
mp : (↑θ : Angle) = -(↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ + ψ) / 2
⊢ (↑n : ℝ) * π * 2 - ψ = θ

Tactic:
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), ← sub_eq_iff_eq_add] at hn

Premises used: Real, two_ne_zero', sub_eq_iff_eq_add, eq_div_iff_mul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
mp₃ : (↑((↑n : ℝ) * π * 2) : Angle) = 0
mp₄ : (↑((↑n : ℝ) * (π * 2)) : Angle) = 0
mp₅ : n • (↑(π * 2) : Angle) = 0
mp₆ : n • (↑(2 * π) : Angle) = 0
mp₇ : HSMul.hSMul (β := Angle) n 0 = 0
mp₈ mp₉ : Eq (α := Angle) 0 0
⊢ (↑θ : Angle) = -(↑ψ : Angle)

Tactic:
rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]

Premises used: zsmul_zero, mul_assoc, Real.Angle.coe_sub, Real.Angle.intCast_mul_eq_zsmul, mul_comm, Real.Angle.coe_two_pi, eq_neg_iff_add_eq_zero, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ - ψ) / 2
mp : (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ - ψ) / 2
⊢ (↑n : ℝ) * π * 2 + ψ = θ

Tactic:
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn

Premises used: Real, eq_sub_iff_add_eq, two_ne_zero', eq_div_iff_mul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * (π * 2)) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₃ : n • (↑(π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₄ : n • (↑(2 * π) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₅ : HSMul.hSMul (β := Angle) n 0 + (↑ψ : Angle) = (↑ψ : Angle)
mp₆ : 0 + (↑ψ : Angle) = (↑ψ : Angle)
mp₇ mp₈ : (↑ψ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]

Premises used: zsmul_zero, mul_assoc, Real.Angle.coe_add, Real.Angle.intCast_mul_eq_zsmul, zero_add, mul_comm, Real.Angle.coe_two_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
mpr : ((∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)) ∨ ∃ (k : ℤ), θ - -ψ = 2 * π * (↑k : ℝ)) → cos θ = cos ψ
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle) → cos θ = cos ψ

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub]

Premises used: Real.Angle.angle_eq_iff_two_pi_dvd_sub, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ + ψ) / 2) * sin (2 * π * (↑k : ℝ) / 2) = 0
mpr₃ : -2 * sin ((θ + ψ) / 2) * sin (2 * (π * (↑k : ℝ)) / 2) = 0
mpr₄ : -2 * sin ((θ + ψ) / 2) * sin (π * (↑k : ℝ)) = 0
mpr₅ : -2 * sin ((θ + ψ) / 2) * sin ((↑k : ℝ) * π) = 0
mpr₆ : -2 * sin ((θ + ψ) / 2) * 0 = 0
mpr₇ mpr₈ : Eq (α := ℝ) 0 0
⊢ cos θ = cos ψ

Tactic:
rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]

Premises used: Int.cast, Real, Real.pi, sub_eq_zero, mul_assoc, mul_div_cancel_left₀, MulZeroClass.mul_zero, two_ne_zero', Real.cos_sub_cos, mul_comm, OfNat.ofNat, Real.sin_int_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₄ : -2 * sin (2 * (π * (↑k : ℝ)) / 2) * sin ((θ - ψ) / 2) = 0
mpr₅ : -2 * sin (π * (↑k : ℝ)) * sin ((θ - ψ) / 2) = 0
mpr₆ : -2 * sin ((↑k : ℝ) * π) * sin ((θ - ψ) / 2) = 0
mpr₇ : HMul.hMul (α := ℝ) (-2) 0 * sin ((θ - ψ) / 2) = 0
mpr₈ : 0 * sin ((θ - ψ) / 2) = 0
mpr₉ mpr₁₀ : Eq (α := ℝ) 0 0
⊢ cos θ = cos ψ

Tactic:
rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]

Premises used: Int.cast, Real, Real.pi, sub_eq_zero, MulZeroClass.zero_mul, mul_assoc, mul_div_cancel_left₀, MulZeroClass.mul_zero, two_ne_zero', Real.cos_sub_cos, mul_comm, OfNat.ofNat, sub_neg_eq_add, Real.sin_int_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
mp : sin θ = sin ψ → (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
mpr : (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle) → sin θ = sin ψ
⊢ sin θ = sin ψ ↔ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : sin θ = sin ψ
⊢ cos (π / 2 - θ) = cos (π / 2 - ψ)

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin

Premises used: Real.cos_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
mp :
  ∀ (h : (↑(π / 2 - θ) : Angle) = (↑(π / 2 - ψ) : Angle)),
    (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
mp₁ :
  ∀ (h : (↑(π / 2 - θ) : Angle) = -(↑(π / 2 - ψ) : Angle)),
    (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)

Tactic:
rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h | h

Premises used: Real.Angle.cos_eq_iff_coe_eq_or_eq_neg, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = (↑(π / 2 - ψ) : Angle)
mp : (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = (↑(π / 2 - ψ) : Angle)
⊢ (↑(π / 2) : Angle) - (↑θ : Angle) = (↑(π / 2) : Angle) - (↑ψ : Angle)

Tactic:
rw [coe_sub, coe_sub] at h

Premises used: Real.Angle.coe_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2) : Angle) - (↑θ : Angle) = (↑(π / 2) : Angle) - (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
sub_right_inj.1 h

Premises used: sub_right_inj, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2) : Angle) - (↑θ : Angle) = (↑(π / 2) : Angle) - (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
exact sub_right_inj.1 h

Premises used: sub_right_inj, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = -(↑(π / 2 - ψ) : Angle)
mp : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)

Tactic:
right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = -(↑(π / 2 - ψ) : Angle)
⊢ (↑π : Angle) = (↑θ : Angle) + (↑ψ : Angle)

Tactic:
rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add,
      add_halves, sub_sub, sub_eq_zero] at h

Premises used: add_halves, sub_eq_zero, add_sub, Real.Angle.coe_add, Real.Angle.coe_sub, sub_sub, eq_neg_iff_add_eq_zero, sub_add_eq_add_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑π : Angle) = (↑θ : Angle) + (↑ψ : Angle)
⊢ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑π : Angle) = (↑θ : Angle) + (↑ψ : Angle)
⊢ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
mpr : ((∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)) ∨ ∃ (k : ℤ), θ - (π - ψ) = 2 * π * (↑k : ℝ)) → sin θ = sin ψ
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle) → sin θ = sin ψ

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub, ← eq_sub_iff_add_eq, ← coe_sub, angle_eq_iff_two_pi_dvd_sub]

Premises used: eq_sub_iff_add_eq, Real.Angle.angle_eq_iff_two_pi_dvd_sub, Real.Angle.coe_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₃ : 2 * sin (2 * (π * (↑k : ℝ)) / 2) * cos ((θ + ψ) / 2) = 0
mpr₄ : 2 * sin (π * (↑k : ℝ)) * cos ((θ + ψ) / 2) = 0
mpr₅ : 2 * sin ((↑k : ℝ) * π) * cos ((θ + ψ) / 2) = 0
mpr₆ : HMul.hMul (α := ℝ) 2 0 * cos ((θ + ψ) / 2) = 0
mpr₇ : 0 * cos ((θ + ψ) / 2) = 0
mpr₈ mpr₉ : Eq (α := ℝ) 0 0
⊢ sin θ = sin ψ

Tactic:
rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]

Premises used: Int.cast, Real, Real.pi, sub_eq_zero, MulZeroClass.zero_mul, mul_assoc, mul_div_cancel_left₀, MulZeroClass.mul_zero, two_ne_zero', Real.sin_sub_sin, mul_comm, OfNat.ofNat, Real.sin_int_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
rwa : ∀ (H : θ - π + ψ = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₁ : ∀ (H : θ + ψ - π = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₂ : ∀ (H : θ + ψ = 2 * π * (↑k : ℝ) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₃ : ∀ (H : θ + ψ = 2 * (π * (↑k : ℝ)) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₄ : ∀ (H : θ + ψ = 2 * ((↑k : ℝ) * π) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (H : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π

Tactic:
rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H

Premises used: sub_add, Real.pi, mul_assoc, sub_eq_iff_eq_add, mul_comm, sub_add_eq_add_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π

Tactic:
have H' : θ + ψ = 2 * k * π + π := by
      rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
mpr₄ : 2 * sin ((θ - ψ) / 2) * cos (2 * ((↑k : ℝ) * π) / 2 + π / 2) = 0
mpr₅ : 2 * sin ((θ - ψ) / 2) * cos ((↑k : ℝ) * π + π / 2) = 0
mpr₆ : 2 * sin ((θ - ψ) / 2) * -sin ((↑k : ℝ) * π) = 0
mpr₇ : 2 * sin ((θ - ψ) / 2) * -0 = 0
mpr₈ : 2 * sin ((θ - ψ) / 2) * 0 = 0
mpr₉ mpr₁₀ : Eq (α := ℝ) 0 0
⊢ sin θ = sin ψ

Tactic:
rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]

Premises used: Real, Real.pi, sub_eq_zero, mul_assoc, mul_div_cancel_left₀, MulZeroClass.mul_zero, two_ne_zero', Real.sin_sub_sin, Real.cos_add_pi_div_two, OfNat.ofNat, neg_zero, Real.sin_int_mul_pi, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
inl : ∀ (hc : (↑θ : Angle) = (↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
inr : ∀ (hc : (↑θ : Angle) = -(↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hcos with hc | hc

Premises used: Real.Angle.cos_eq_iff_coe_eq_or_eq_neg, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
hc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
exact hc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
inr : ∀ (hs : (↑θ : Angle) = (↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
inr₁ : ∀ (hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)), (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
rcases sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs | hs

Premises used: Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
hs : (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
hs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
hs : (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
exact hs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ (↑π : Angle) = 0

Tactic:
rw [eq_neg_iff_add_eq_zero, hs] at hc

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
hc₁ : (↑π : Angle) = 0
⊢ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)

Tactic:
rw [eq_neg_iff_add_eq_zero, hs] at hc

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ ∃ (n : ℤ), n • (2 * π) = -π + 0

Tactic:
QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)

Premises used: QuotientAddGroup.leftRel_apply, Set.Mem, setOf, Iff.mp, Quotient.exact', Set.range
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
inr : ∀ (n : ℤ) (hn : n • (2 * π) = -π + 0), (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
obtain ⟨n, hn⟩ : ∃ n, n • _ = _ := QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)

Premises used: QuotientAddGroup.leftRel_apply, Iff.mp, Quotient.exact'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n • (2 * π) = -π + 0
⊢ n * 2 + 1 = 0

Tactic:
rw [← neg_one_mul, add_zero, ← sub_eq_zero, zsmul_eq_mul, ← mul_assoc, ← sub_mul, mul_eq_zero,
    eq_false (ne_of_gt pi_pos), or_false, sub_neg_eq_add, ← Int.cast_zero, ← Int.cast_one,
    ← Int.cast_ofNat, ← Int.cast_mul, ← Int.cast_add, Int.cast_inj] at hn

Premises used: zsmul_eq_mul, eq_false, Int.cast_inj, sub_eq_zero, Int.cast_zero, mul_assoc, neg_one_mul, Int.cast_add, ne_of_gt, Real.pi_pos, Int.cast_ofNat, mul_eq_zero, sub_mul, Int.cast_mul, or_false, add_zero, Int.cast_one, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n * 2 + 1 = 0
⊢ (n * 2 + 1) % 2 = HMod.hMod (α := ℤ) 0 2

Tactic:
have : (n * 2 + 1) % (2 : ℤ) = 0 % (2 : ℤ) := congr_arg (· % (2 : ℤ)) hn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n * 2 + 1 = 0
this : (n * 2 + 1) % 2 = HMod.hMod (α := ℤ) 0 2
⊢ HMod.hMod (α := ℤ) 1 2 = HMod.hMod (α := ℤ) 0 2

Tactic:
rw [add_comm, Int.add_mul_emod_self_right] at this

Premises used: add_comm, Int.add_mul_emod_self_right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n * 2 + 1 = 0
this : HMod.hMod (α := ℤ) 1 2 = HMod.hMod (α := ℤ) 0 2
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
absurd this one_ne_zero

Premises used: absurd, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n * 2 + 1 = 0
this : HMod.hMod (α := ℤ) 1 2 = HMod.hMod (α := ℤ) 0 2
⊢ (↑θ : Angle) = (↑ψ : Angle)

Tactic:
exact absurd this one_ne_zero

Premises used: absurd, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ (↑x : Angle).sin = Real.sin x

Tactic:
rfl

Premises used: Quotient.liftOn', Function.Periodic.lift, Real.Angle.sin, Real.sin, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ Continuous sin

Tactic:
Real.continuous_sin.quotient_liftOn' _

Premises used: Real.Angle, Function.Periodic.lift, Real.continuous_sin, Real.Angle.sin, Continuous.quotient_liftOn'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ (↑x : Angle).cos = Real.cos x

Tactic:
rfl

Premises used: Quotient.liftOn', Real.cos, Function.Periodic.lift, rfl, Real.Angle.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ Continuous cos

Tactic:
Real.continuous_cos.quotient_liftOn' _

Premises used: Real.Angle, Function.Periodic.lift, Real.continuous_cos, Real.Angle.cos, Continuous.quotient_liftOn'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
ψ : ℝ
h : ∀ (x : ℝ), (↑x : Angle).cos = Real.cos ψ ↔ (↑x : Angle) = (↑ψ : Angle) ∨ (↑x : Angle) = -(↑ψ : Angle)
⊢ θ.cos = Real.cos ψ ↔ θ = (↑ψ : Angle) ∨ θ = -(↑ψ : Angle)

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

Tactic:
cos_eq_iff_coe_eq_or_eq_neg

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

Tactic:
exact cos_eq_iff_coe_eq_or_eq_neg

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

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

Tactic:
cos_eq_real_cos_iff_eq_or_eq_neg

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

Tactic:
exact cos_eq_real_cos_iff_eq_or_eq_neg

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

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

Tactic:
sin_eq_iff_coe_eq_or_add_eq_pi

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

Tactic:
exact sin_eq_iff_coe_eq_or_add_eq_pi

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

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

Tactic:
sin_eq_real_sin_iff_eq_or_add_eq_pi

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

Tactic:
exact sin_eq_real_sin_iff_eq_or_add_eq_pi

Premises used: Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : (↑0 : Angle).sin = 0
rw₁ : Real.sin 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ sin 0 = 0

Tactic:
rw [← coe_zero, sin_coe, Real.sin_zero]

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

Tactic:
rw [sin_coe, Real.sin_pi]

Premises used: Real.sin_pi, Real.Angle.sin_coe