awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
inl : (↑π : Angle).toReal ∈ Set.Ioo 0 π ↔ (↑π : Angle).sign = 1
inr : ∀ (h : θ ≠ (↑π : Angle)), θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
rcases eq_or_ne θ π with rfl | h

Premises used: Real.pi, Real.Angle.coe, eq_or_ne, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ (↑π : Angle).toReal ∈ Set.Ioo 0 π ↔ (↑π : Angle).sign = 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
inr : 0 < θ.toReal → θ.toReal < π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
simp only [Set.mem_Ioo, ← sign_toReal h, sign_eq_one_iff, and_iff_left_iff_imp]

Premises used: Set.mem_Ioo, Real.Angle.sign_toReal, and_iff_left_iff_imp, sign_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ 0 < θ.toReal → θ.toReal < π

Tactic:
fun _ ↦ (toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)

Premises used: Iff.mpr, Real.Angle.toReal_eq_pi_iff, Iff.not, LE.le.lt_of_ne, Real.Angle.toReal_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ 0 < θ.toReal → θ.toReal < π

Tactic:
exact fun _ ↦ (toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)

Premises used: Iff.mpr, Real.Angle.toReal_eq_pi_iff, Iff.not, LE.le.lt_of_ne, Real.Angle.toReal_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : 0 ≤ θ.sign
rw : (↑θ.toReal : Angle) = θ
rw₁ rw₂ : θ = θ
⊢ (↑|θ.toReal| : Angle) = θ

Tactic:
rw [abs_eq_self.2 (toReal_nonneg_iff_sign_nonneg.2 h), coe_toReal]

Premises used: Iff.mpr, Real.Angle.toReal_nonneg_iff_sign_nonneg, Real.Angle.coe_toReal, abs_eq_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ.sign ≤ 0
⊢ θ.sign = -1 ∨ θ.sign = 0

Tactic:
rw [SignType.nonpos_iff] at h

Premises used: SignType.nonpos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
inl : ∀ (h : θ.sign = -1), -(↑|θ.toReal| : Angle) = θ
inr : ∀ (h : θ.sign = 0), -(↑|θ.toReal| : Angle) = θ
⊢ -(↑|θ.toReal| : Angle) = θ

Tactic:
rcases h with (h | h)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ.sign = -1
inl : -(↑(-θ.toReal) : Angle) = θ
inl₁ : - -(↑θ.toReal : Angle) = θ
inl₂ : (↑θ.toReal : Angle) = θ
inl₃ inl₄ : θ = θ
⊢ -(↑|θ.toReal| : Angle) = θ

Tactic:
rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]

Premises used: Iff.mpr, abs_of_neg, neg_neg, Real.Angle.coe_toReal, Real.Angle.toReal_neg_iff_sign_neg, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ.sign = 0
⊢ θ = 0 ∨ θ = (↑π : Angle)

Tactic:
rw [sign_eq_zero_iff] at h

Premises used: Real.Angle.sign_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ = 0 ∨ θ = (↑π : Angle)
inr : -(↑|toReal 0| : Angle) = 0
inr₁ : -(↑|(↑π : Angle).toReal| : Angle) = (↑π : Angle)
⊢ -(↑|θ.toReal| : Angle) = θ

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -(↑|toReal 0| : Angle) = 0

Tactic:
simp [abs_of_pos Real.pi_pos]

Premises used: Real.pi_pos, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -(↑|(↑π : Angle).toReal| : Angle) = (↑π : Angle)

Tactic:
simp [abs_of_pos Real.pi_pos]

Premises used: Real.pi_pos, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
⊢ θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|

Tactic:
grind [toReal_neg_iff_sign_neg]

Premises used: Real.Angle.toReal_neg_iff_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : θ.sign = ψ.sign
⊢ θ = ψ ↔ |θ.toReal| = |ψ.toReal|

Tactic:
simpa [h] using @eq_iff_sign_eq_and_abs_toReal_eq θ ψ

Premises used: Real.Angle.eq_iff_sign_eq_and_abs_toReal_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑(π / 2) : Angle).sin : SignType) (1 : SignType)
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin (π / 2)) : SignType) (1 : SignType)
rw₂ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 1 : SignType) (1 : SignType)
rw₃ rw₄ : Eq (α := SignType) 1 1
⊢ (↑(π / 2) : Angle).sign = 1

Tactic:
rw [sign, sin_coe, sin_pi_div_two, sign_one]

Premises used: Real.sin_pi_div_two, sign_one, Real.Angle.sin_coe, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑(-π / 2) : Angle).sin : SignType) (-1 : SignType)
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin (-π / 2)) : SignType) (-1 : SignType)
rw₂ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin (-(π / 2))) : SignType) (-1 : SignType)
rw₃ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-Real.sin (π / 2)) : SignType) (-1 : SignType)
rw₄ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-1) : SignType) (-1 : SignType)
rw₅ : Eq (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) 1 : SignType) (-1 : SignType)
rw₆ rw₇ : Eq (α := SignType) (-1) (-1)
⊢ (↑(-π / 2) : Angle).sign = -1

Tactic:
rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]

Premises used: Real.sin_pi_div_two, neg_div, Real.sin_neg, sign_one, Real.Angle.sin_coe, Real.Angle.sign, Left.sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
rw : 0 ≤ (↑θ : Angle).sin
⊢ 0 ≤ (↑θ : Angle).sign

Tactic:
rw [sign, sign_nonneg_iff]

Premises used: sign_nonneg_iff, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ : Angle).sin

Tactic:
sin_nonneg_of_nonneg_of_le_pi h0 hpi

Premises used: Quotient.liftOn', Real.sin_nonneg_of_nonneg_of_le_pi, Function.Periodic.lift, Real.Angle.sin, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ : Angle).sin

Tactic:
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi

Premises used: Real.sin_nonneg_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
rw : 0 ≤ (↑θ : Angle).sin
⊢ (-(↑θ : Angle)).sign ≤ 0

Tactic:
rw [sign, sign_nonpos_iff, sin_neg, Left.neg_nonpos_iff]

Premises used: Real.Angle.sin_neg, Left.neg_nonpos_iff, Real.Angle.sign, sign_nonpos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
simp : |θ.toReal| < π / 2 ∨ θ = 0 ∨ θ = (↑π : Angle) ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
⊢ (HSMul.hSMul (α := ℕ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2

Tactic:
simp only [sign, sin_two_nsmul, nsmul_eq_mul, Nat.cast_ofNat, sign_mul, Nat.ofNat_pos, sign_pos,
    one_mul, mul_right_eq_self₀, _root_.sign_eq_zero_iff, sign_eq_one_iff, sin_eq_zero_iff,
    cos_pos_iff_abs_toReal_lt_pi_div_two]

Premises used: Nat.cast_ofNat, Real.Angle.sin_eq_zero_iff, sign_pos, Real.Angle.sin_two_nsmul, Nat.ofNat_pos, sign_mul, Real.Angle.sign, sign_eq_zero_iff, Real.Angle.cos_pos_iff_abs_toReal_lt_pi_div_two, nsmul_eq_mul, mul_right_eq_self₀, one_mul, sign_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
this : 0 < π / 2
⊢ |θ.toReal| < π / 2 ∨ θ = 0 ∨ θ = (↑π : Angle) ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : (θ + θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
rw₂ rw₃ : θ = (↑π : Angle) ∨ |θ.toReal| < π / 2 ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2

Tactic:
rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]

Premises used: Real.Angle.sign_two_nsmul_eq_sign_iff, two_zsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|

Tactic:
simpa [← cos_pos_iff_abs_toReal_lt_pi_div_two, ← cos_neg_iff_pi_div_two_lt_abs_toReal]
    using sign_two_nsmul_eq_sign_iff (θ := θ + π)

Premises used: Real.Angle.sign_two_nsmul_eq_sign_iff, Real.Angle.cos_pos_iff_abs_toReal_lt_pi_div_two, Real.Angle.cos_neg_iff_pi_div_two_lt_abs_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : (θ + θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
rw₂ rw₃ : θ = 0 ∨ π / 2 < |θ.toReal| ↔ θ = 0 ∨ π / 2 < |θ.toReal|
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|

Tactic:
rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_neg_sign_iff]

Premises used: Real.Angle.sign_two_nsmul_eq_neg_sign_iff, two_zsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 b
h_sign : a.sign = -b.sign
h_ne : b.sign ≠ 0
⊢ a = b ∨ a = b + (↑π : Angle)

Tactic:
have h1 := Real.Angle.two_zsmul_eq_iff.mp h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 b
h_sign : a.sign = -b.sign
h_ne : b.sign ≠ 0
h1 : a = b ∨ a = b + (↑π : Angle)
⊢ a = b + (↑π : Angle)

Tactic:
h1.resolve_left ?_

Premises used: Or.resolve_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 b
h_sign : a.sign = -b.sign
h_ne : b.sign ≠ 0
h1 : a = b ∨ a = b + (↑π : Angle)
refine : ¬a = b
⊢ a = b + (↑π : Angle)

Tactic:
refine h1.resolve_left ?_

Premises used: Or.resolve_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 a
h_sign : a.sign = -a.sign
h_ne : a.sign ≠ 0
h1 : a = a ∨ a = a + (↑π : Angle)
⊢ a.sign = 0

Tactic:
simp only [SignType.self_eq_neg_iff] at h_sign

Premises used: SignType.self_eq_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 a
h_ne : a.sign ≠ 0
h1 : a = a ∨ a = a + (↑π : Angle)
h_sign : a.sign = 0
⊢ Ne (α := SignType) 0 0

Tactic:
rw [h_sign] at h_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 a
h_ne : a.sign ≠ 0
h1 : a = a ∨ a = a + (↑π : Angle)
h_sign : a.sign = 0
h_ne₁ : Ne (α := SignType) 0 0
⊢ a = a ∨ a = a + (↑π : Angle)

Tactic:
rw [h_sign] at h_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 a
h_ne : a.sign ≠ 0
h1 : a = a ∨ a = a + (↑π : Angle)
h_sign : a.sign = 0
h_ne₁ : Ne (α := SignType) 0 0
h1₁ : a = a ∨ a = a + (↑π : Angle)
⊢ a.sign = 0

Tactic:
rw [h_sign] at h_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a : Angle
h : HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 a
h_ne : Ne (α := SignType) 0 0
h1 : a = a ∨ a = a + (↑π : Angle)
h_sign : a.sign = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = (↑π : Angle)
⊢ a = b + (↑π : Angle)

Tactic:
simp [← h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = (↑π : Angle)
⊢ a = b + (↑π : Angle)

Tactic:
have h' : a = b + π := by
    simp [← h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = (↑π : Angle)
h' : a = b + (↑π : Angle)
⊢ a.sign = b.sign

Tactic:
have h_sign' := h_sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = (↑π : Angle)
h' : a = b + (↑π : Angle)
h_sign' : a.sign = b.sign
⊢ -b.sign = b.sign

Tactic:
rw [h', Real.Angle.sign_add_pi] at h_sign'

Premises used: Real.Angle.sign_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = (↑π : Angle)
h' : a = b + (↑π : Angle)
h_sign' : -b.sign = b.sign
⊢ b.sign = 0

Tactic:
simp only [SignType.neg_eq_self_iff] at h_sign'

Premises used: SignType.neg_eq_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = (↑π : Angle)
h' : a = b + (↑π : Angle)
h_sign' : b.sign = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
rw : a = b ∨ a = b + (↑π : Angle) ↔ a = b
⊢ HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 b ↔ a = b

Tactic:
rw [Real.Angle.two_zsmul_eq_iff]

Premises used: Real.Angle.two_zsmul_eq_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
mp : a = b ∨ a = b + (↑π : Angle) → a = b
mpr : a = b → a = b ∨ a = b + (↑π : Angle)
⊢ a = b ∨ a = b + (↑π : Angle) ↔ a = b

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h_1 : a.sign = b.sign
h : a = b ∨ a = b + (↑π : Angle)
mp : ∀ (h1 : a = b), a = b
mp₁ : ∀ (h2 : a = b + (↑π : Angle)), a = b
⊢ a = b

Tactic:
rcases h with h1 | h2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h1 : a = b
⊢ a = b

Tactic:
h1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h1 : a = b
⊢ a = b

Tactic:
exact h1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
⊢ a.sign = (b + (↑π : Angle)).sign

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
⊢ a.sign = (b + (↑π : Angle)).sign

Tactic:
have : a.sign = (b + π).sign := by aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
this : a.sign = (b + (↑π : Angle)).sign
⊢ a.sign = -b.sign

Tactic:
rw [Real.Angle.sign_add_pi] at this

Premises used: Real.Angle.sign_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
this : a.sign = -b.sign
⊢ Eq (α := Prop) ((fun (x : SignType) ↦ x = b.sign) a.sign) ((fun (x : SignType) ↦ x = b.sign) (-b.sign))

Tactic:
have := congr_arg (· = b.sign) this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
this_1 : a.sign = -b.sign
this : Eq (α := Prop) ((fun (x : SignType) ↦ x = b.sign) a.sign) ((fun (x : SignType) ↦ x = b.sign) (-b.sign))
⊢ a = b

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
a b : Angle
ha : a.sign ≠ 0
h_1 : a.sign = b.sign
h : a = b
⊢ a = b ∨ a = b + (↑π : Angle)

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
inl : ∀ (h : θ + ψ = 0), |θ.toReal| + |ψ.toReal| = π
inr : ∀ (h : θ + ψ = (↑π : Angle)), |θ.toReal| + |ψ.toReal| = π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
rcases two_nsmul_eq_zero_iff.mp h with h | h

Premises used: Real.Angle.two_nsmul_eq_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = 0
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
simp_all [add_eq_zero_iff_eq_neg.mp h]

Premises used: add_eq_zero_iff_eq_neg, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = (↑π : Angle)
⊢ (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)

Tactic:
rw [← coe_toReal θ, ← coe_toReal ψ, ← coe_add] at h

Premises used: Real.Angle.coe_add, Real.Angle.coe_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
this : |θ.toReal + ψ.toReal| = π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
grind [toReal_neg_iff_sign_neg, abs_add_eq_add_abs_iff]

Premises used: abs_add_eq_add_abs_iff, Real.Angle.toReal_neg_iff_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
inr : |θ.toReal + ψ.toReal| = π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
suffices |θ.toReal + ψ.toReal| = π by grind [toReal_neg_iff_sign_neg, abs_add_eq_add_abs_iff]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
inr : θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
⊢ |θ.toReal + ψ.toReal| = π

Tactic:
rw [abs_eq pi_nonneg]

Premises used: Real.pi_nonneg, abs_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
inr : ∀ (k : ℤ) (hk : θ.toReal + ψ.toReal - π = 2 * π * (↑k : ℝ)), θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
rcases angle_eq_iff_two_pi_dvd_sub.mp h with ⟨k, hk⟩

Premises used: Real.Angle.angle_eq_iff_two_pi_dvd_sub, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
k : ℤ
hk : θ.toReal + ψ.toReal - π = 2 * π * (↑k : ℝ)
⊢ θ.toReal + ψ.toReal = 2 * π * (↑k : ℝ) + π

Tactic:
rw [sub_eq_iff_eq_add] at hk

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
k : ℤ
hk : θ.toReal + ψ.toReal = 2 * π * (↑k : ℝ) + π
⊢ 2 * π * (↑k : ℝ) ∈ Set.Ioo (2 * π * (↑(HSub.hSub (α := ℤ) (-1) 1) : ℝ)) (2 * π * (↑(HAdd.hAdd (α := ℤ) 0 1) : ℝ))

Tactic:
grind [toReal_mem_Ioc]

Premises used: Real.Angle.toReal_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
k : ℤ
hk : θ.toReal + ψ.toReal = 2 * π * (↑k : ℝ) + π
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 0) k

Tactic:
have : k ∈ Finset.Icc (-1) 0 :=
    IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo two_pi_pos <| by grind [toReal_mem_Ioc]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
k : ℤ
hk : θ.toReal + ψ.toReal = 2 * π * (↑k : ℝ) + π
this : Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 0) k
inr :
  ∀
    (hk :
      θ.toReal + ψ.toReal =
        2 * π * (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-1)) : (a : ℕ) → ℤ) 0) : ℝ) + π),
    θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
inr₁ :
  ∀
    (hk :
      θ.toReal + ψ.toReal =
        2 * π * (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-1)) : (a : ℕ) → ℤ) 1) : ℝ) + π),
    θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
fin_cases this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
hk :
  θ.toReal + ψ.toReal =
    2 * π * (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-1)) : (a : ℕ) → ℤ) 0) : ℝ) + π
⊢ θ.toReal + ψ.toReal = -(2 * π) + π

Tactic:
simp at hk
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
hk : θ.toReal + ψ.toReal = -(2 * π) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
hk :
  θ.toReal + ψ.toReal =
    2 * π * (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-1)) : (a : ℕ) → ℤ) 1) : ℝ) + π
⊢ θ.toReal + ψ.toReal = π

Tactic:
simp at hk
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
hk : θ.toReal + ψ.toReal = π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0

Tactic:
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 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h₁ : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
⊢ θ.sign = ψ.sign

Tactic:
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 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h₁ : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs₁ : θ.sign = ψ.sign
⊢ θ.sign ≠ 0

Tactic:
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 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq h hs h0

Premises used: Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
exact abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq h hs h0

Premises used: Real.Angle.abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
this : (↑(θ.toReal + ψ.toReal) : Angle).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
simpa using this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
suffices : (↑(θ.toReal + ψ.toReal) : Angle).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
suffices ((θ.toReal + ψ.toReal : ℝ) : Angle).toReal = θ.toReal + ψ.toReal by simpa using this