awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ θ.toReal ∈ Set.Ioc (-π) π

Tactic:
⟨neg_pi_lt_toReal _, toReal_le_pi _⟩

Premises used: Set.Ioc, Set.Mem, setOf, Real.Angle.neg_pi_lt_toReal, And.intro, Real.Angle.toReal_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : ∀ (x : ℝ), toIocMod two_pi_pos (-π) (↑x : Angle).toReal = (↑x : Angle).toReal
⊢ toIocMod two_pi_pos (-π) θ.toReal = θ.toReal

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

Tactic:
toIocMod_toIocMod _ _ _ _

Premises used: toIocMod_toIocMod
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
x : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x) = toIocMod two_pi_pos (-π) x

Tactic:
exact toIocMod_toIocMod _ _ _ _

Premises used: toIocMod_toIocMod
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : -π < 0 ∧ 0 ≤ π
⊢ toReal 0 = 0

Tactic:
rw [← coe_zero, toReal_coe_eq_self_iff]

Premises used: Real.Angle.toReal_coe_eq_self_iff, Real.Angle.coe_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -π < 0 ∧ 0 ≤ π

Tactic:
⟨Left.neg_neg_iff.2 Real.pi_pos, Real.pi_pos.le⟩

Premises used: Iff.mpr, Left.neg_neg_iff, Real.pi_pos, LT.lt.le, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -π < 0 ∧ 0 ≤ π

Tactic:
exact ⟨Left.neg_neg_iff.2 Real.pi_pos, Real.pi_pos.le⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
nth_rw : θ.toReal = toReal 0 ↔ θ = 0
⊢ θ.toReal = 0 ↔ θ = 0

Tactic:
nth_rw 1 [← toReal_zero]

Premises used: Real.Angle.toReal_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0

Tactic:
toReal_inj

Premises used: Real.Angle.toReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0

Tactic:
exact toReal_inj

Premises used: Real.Angle.toReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : -π < π ∧ π ≤ π
⊢ (↑π : Angle).toReal = π

Tactic:
rw [toReal_coe_eq_self_iff]

Premises used: Real.Angle.toReal_coe_eq_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -π < π ∧ π ≤ π

Tactic:
⟨Left.neg_lt_self Real.pi_pos, le_refl _⟩

Premises used: le_refl, Left.neg_lt_self, Real.pi_pos, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -π < π ∧ π ≤ π

Tactic:
exact ⟨Left.neg_lt_self Real.pi_pos, le_refl _⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.toReal = π ↔ θ.toReal = (↑π : Angle).toReal
rw₁ rw₂ : θ.toReal = π ↔ θ.toReal = π
⊢ θ.toReal = π ↔ θ = (↑π : Angle)

Tactic:
rw [← toReal_inj, toReal_pi]

Premises used: Real.Angle.toReal_pi, Real.Angle.toReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
nth_rw : -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ (↑π : Angle)
⊢ (-θ).toReal = -θ.toReal ↔ θ ≠ (↑π : Angle)

Tactic:
nth_rw 1 [← coe_toReal θ, ← coe_neg, toReal_coe_eq_self_iff]

Premises used: Real.Angle.toReal_coe_eq_self_iff, Real.Angle.coe_toReal, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
mp : -π < -θ.toReal ∧ -θ.toReal ≤ π → θ ≠ (↑π : Angle)
mpr : θ ≠ (↑π : Angle) → -π < -θ.toReal ∧ -θ.toReal ≤ π
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ (↑π : Angle)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
h : -π < -(↑π : Angle).toReal
h' : -(↑π : Angle).toReal ≤ π
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
mpr : θ.toReal < π ∧ -θ.toReal ≤ π
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π

Tactic:
rw [neg_lt_neg_iff]

Premises used: neg_lt_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ θ.toReal ≠ π

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ θ.toReal ≠ π

Tactic:
have h' : θ.toReal ≠ π := by simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
h' : θ.toReal ≠ π
linarith : π < -θ.toReal → π - -θ.toReal + (-π - θ.toReal) = 0
⊢ -θ.toReal ≤ π

Tactic:
linarith [neg_pi_lt_toReal θ]

Premises used: Real.Angle.neg_pi_lt_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
h' : θ.toReal ≠ π
⊢ θ.toReal < π ∧ -θ.toReal ≤ π

Tactic:
exact ⟨(toReal_le_pi θ).lt_of_ne h', by linarith [neg_pi_lt_toReal θ]⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
inl : |(-(↑π : Angle)).toReal| = |(↑π : Angle).toReal|
inr : ∀ (h : θ ≠ (↑π : Angle)), |(-θ).toReal| = |θ.toReal|
⊢ |(-θ).toReal| = |θ.toReal|

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| = |(↑π : Angle).toReal|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ |(-θ).toReal| = |θ.toReal|

Tactic:
simp [toReal_neg_eq_neg_toReal_iff.2 h]

Premises used: Iff.mpr, Real.Angle.toReal_neg_eq_neg_toReal_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : π ≠ 0
⊢ (↑π : Angle) ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_pi, toReal_zero]

Premises used: Real.Angle.toReal_pi, Function.Injective.ne_iff, Real.Angle.toReal_injective, Real.Angle.toReal_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ π ≠ 0

Tactic:
Real.pi_ne_zero

Premises used: Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ π ≠ 0

Tactic:
exact Real.pi_ne_zero

Premises used: Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
left : -π < π / 2
right : π / 2 ≤ π
⊢ -π < π / 2 ∧ π / 2 ≤ π

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

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < π / 2 → 2 * π - 1 * π + (0 - π) = 0
⊢ π / 2 ≤ π

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.toReal = π / 2 ↔ θ.toReal = (↑(π / 2) : Angle).toReal
rw₁ rw₂ : θ.toReal = π / 2 ↔ θ.toReal = π / 2
⊢ θ.toReal = π / 2 ↔ θ = (↑(π / 2) : Angle)

Tactic:
rw [← toReal_inj, toReal_pi_div_two]

Premises used: Real.Angle.toReal_inj, Real.Angle.toReal_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
left : -π < -π / 2
right : -π / 2 ≤ π
⊢ -π < -π / 2 ∧ -π / 2 ≤ π

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

Tactic:
linarith [pi_pos]

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

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.toReal = -π / 2 ↔ θ.toReal = (↑(-π / 2) : Angle).toReal
rw₁ rw₂ : θ.toReal = -π / 2 ↔ θ.toReal = -π / 2
⊢ θ.toReal = -π / 2 ↔ θ = (↑(-π / 2) : Angle)

Tactic:
rw [← toReal_inj, toReal_neg_pi_div_two]

Premises used: Real.Angle.toReal_neg_pi_div_two, Real.Angle.toReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : π / 2 ≠ 0
⊢ (↑(π / 2) : Angle) ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_pi_div_two, toReal_zero]

Premises used: Real.Angle.toReal_pi_div_two, Function.Injective.ne_iff, Real.Angle.toReal_injective, Real.Angle.toReal_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ π / 2 ≠ 0

Tactic:
div_ne_zero Real.pi_ne_zero two_ne_zero

Premises used: div_ne_zero, two_ne_zero, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ π / 2 ≠ 0

Tactic:
exact div_ne_zero Real.pi_ne_zero two_ne_zero

Premises used: div_ne_zero, two_ne_zero, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
rw : -π / 2 ≠ 0
⊢ (↑(-π / 2) : Angle) ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_neg_pi_div_two, toReal_zero]

Premises used: Real.Angle.toReal_neg_pi_div_two, Function.Injective.ne_iff, Real.Angle.toReal_injective, Real.Angle.toReal_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -π / 2 ≠ 0

Tactic:
div_ne_zero (neg_ne_zero.2 Real.pi_ne_zero) two_ne_zero

Premises used: Iff.mpr, div_ne_zero, two_ne_zero, neg_ne_zero, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
⊢ -π / 2 ≠ 0

Tactic:
exact div_ne_zero (neg_ne_zero.2 Real.pi_ne_zero) two_ne_zero

Premises used: Iff.mpr, div_ne_zero, two_ne_zero, neg_ne_zero, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ |(↑θ : Angle).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π

Tactic:
⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h =>
    (toReal_coe_eq_self_iff.2 ⟨(Left.neg_neg_iff.2 Real.pi_pos).trans_le h.1, h.2⟩).symm ▸
      abs_eq_self.2 h.1⟩

Premises used: Iff.mpr, Real.Angle.coe, Real.Angle.abs_toReal_le_pi, Left.neg_neg_iff, Real.Angle.toReal_coe_eq_self_iff, Eq.rec, Real.pi_pos, And.right, And.left, LT.lt.trans_le, And.intro, Iff.intro, Eq.symm, abs_eq_self, Real.Angle.toReal, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ |(-(↑θ : Angle)).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π

Tactic:
⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩

Premises used: Real.Angle.coe, Real.Angle.abs_toReal_le_pi, Eq.rec, And.intro, Iff.intro, Real.Angle.toReal, abs_nonneg, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
refine : ∀ (h : 0 ≤ θ ∧ θ ≤ π), |(-(↑θ : Angle)).toReal| = θ
⊢ |(-(↑θ : Angle)).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π

Tactic:
refine ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
pos : ∀ (hnegpi : θ = π), |(-(↑θ : Angle)).toReal| = θ
neg : ∀ (hnegpi : ¬θ = π), |(-(↑θ : Angle)).toReal| = θ
⊢ |(-(↑θ : Angle)).toReal| = θ

Tactic:
by_cases hnegpi : θ = π
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |(-(↑θ : Angle)).toReal| = θ

Tactic:
simp [hnegpi, Real.pi_pos.le]

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
neg : |(↑(-θ) : Angle).toReal| = θ
neg₁ : |(-θ)| = θ
neg₂ : |θ| = θ
neg₃ neg₄ : θ = θ
⊢ |(-(↑θ : Angle)).toReal| = θ

Tactic:
rw [← coe_neg,
    toReal_coe_eq_self_iff.2
      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
    abs_neg, abs_eq_self.2 h.1]

Premises used: Iff.mpr, abs_neg, Real.Angle.toReal_coe_eq_self_iff, neg_lt_neg, Real.pi_pos, neg_nonpos, LT.lt.le, And.right, And.left, And.intro, LE.le.trans, abs_eq_self, lt_of_le_of_ne, Real.Angle.coe_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : θ.toReal = π / 2 ∨ θ.toReal = -(π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : θ.toReal = π / 2 ∨ θ.toReal = -π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₂ : θ = (↑(π / 2) : Angle) ∨ θ.toReal = -π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₃ rw₄ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ |θ.toReal| = π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)

Tactic:
rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff,
    toReal_eq_neg_pi_div_two_iff]

Premises used: neg_div, abs_eq, two_pos, Real.pi_pos, LT.lt.le, div_nonneg, Real.Angle.toReal_eq_pi_div_two_iff, Real.Angle.toReal_eq_neg_pi_div_two_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
nth_rw : (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
⊢ (n • θ).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))

Tactic:
nth_rw 1 [← coe_toReal θ]

Premises used: Real.Angle.coe_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have h' : 0 < (n : ℝ) := mod_cast Nat.pos_of_ne_zero h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑(n • θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₁ : (↑((↑n : ℝ) * θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₂ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
rw₃ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π / (↑n : ℝ) < θ.toReal ∧ θ.toReal ≤ π / (↑n : ℝ)
rw₄ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π < (↑n : ℝ) * θ.toReal ∧ θ.toReal ≤ π / (↑n : ℝ)
rw₅ rw₆ : -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π ↔ -π < (↑n : ℝ) * θ.toReal ∧ (↑n : ℝ) * θ.toReal ≤ π
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))

Tactic:
rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']

Premises used: le_div_iff₀', Real.Angle.toReal_coe_eq_self_iff, Real.Angle.coe_nsmul, div_lt_iff₀', nsmul_eq_mul, Set.mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
mod_cast nsmul_toReal_eq_mul two_ne_zero

Premises used: Set.Ioc, Real.pi, HMul.hMul, cast, Membership.mem, HDiv.hDiv, two_ne_zero, Iff, Eq.refl, HSMul.hSMul, Real.Angle.nsmul_toReal_eq_mul, OfNat.ofNat, Real.Angle.toReal, Eq, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : (θ + θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
rw₂ rw₃ : θ.toReal ∈ Set.Ioc (-π / 2) (π / 2) ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)
⊢ (HSMul.hSMul (α := ℤ) 2 θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]

Premises used: two_zsmul, Real.Angle.two_nsmul_toReal_eq_two_mul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
k : ℤ
rw :
  -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ∧ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π ↔
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ ∧ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π
⊢ (↑θ : Angle).toReal = θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ↔
    θ ∈ Set.Ioc ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π) ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π)

Tactic:
rw [← sub_zero (θ : Angle), ← zsmul_zero k, ← coe_two_pi, ← coe_zsmul, ← coe_sub, zsmul_eq_mul, ←
    mul_assoc, mul_comm (k : ℝ), toReal_coe_eq_self_iff, Set.mem_Ioc]

Premises used: Int.cast, zsmul_eq_mul, Real.Angle.coe, sub_zero, Real.Angle.toReal_coe_eq_self_iff, zsmul_zero, mul_assoc, Real.Angle.coe_sub, mul_comm, Set.mem_Ioc, Real.Angle.coe_two_pi, Real.Angle.coe_zsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
k : ℤ
h : -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ∧ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π
linarith :
  θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π →
    -π - (θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π) + (θ - (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π) = 0
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
k : ℤ
h : -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ∧ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π
linarith :
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π < θ →
    θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π - π + ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π - θ) = 0
⊢ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
k : ℤ
h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ ∧ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π
linarith :
  θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ -π →
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π - θ + (θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π - -π) = 0
⊢ -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
k : ℤ
h : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ ∧ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π
linarith :
  π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π →
    θ - (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π + (π - (θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π)) = 0
⊢ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
k : ℤ
⊢ -π < θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ∧ θ - HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π ≤ π ↔
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) - 1) * π < θ ∧ θ ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π

Tactic:
exact ⟨fun h => ⟨by linarith, by linarith⟩, fun h => ⟨by linarith, by linarith⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ (↑θ : Angle).toReal = θ - HMul.hMul (α := ℝ) 2 (↑1 : ℝ) * π ↔
    θ ∈ Set.Ioc ((HMul.hMul (α := ℝ) 2 (↑1 : ℝ) - 1) * π) ((HMul.hMul (α := ℝ) 2 (↑1 : ℝ) + 1) * π)

Tactic:
@toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1

Premises used: Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h : 2 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ)
h₁ : π = (HMul.hMul (α := ℝ) 2 (↑1 : ℝ) - 1) * π
h₂ : 3 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ) + 1
⊢ (↑θ : Angle).toReal = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)

Tactic:
convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ 1

Premises used: Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ 2 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ π = (HMul.hMul (α := ℝ) 2 (↑1 : ℝ) - 1) * π

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ 3 = HMul.hMul (α := ℝ) 2 (↑1 : ℝ) + 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ (↑θ : Angle).toReal = θ - HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) * π ↔
    θ ∈ Set.Ioc ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) - 1) * π) ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) + 1) * π)

Tactic:
@toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1)

Premises used: Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
h : θ + 2 * π = θ - HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) * π
h₁ :
  Set.Ioc (-3 * π) (-π) =
    Set.Ioc ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) - 1) * π) ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) + 1) * π)
⊢ (↑θ : Angle).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)

Tactic:
convert! @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2

Premises used: Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ θ + 2 * π = θ - HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) * π

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : ℝ
⊢ Set.Ioc (-3 * π) (-π) =
    Set.Ioc ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) - 1) * π) ((HMul.hMul (α := ℝ) 2 (↑(-1) : ℝ) + 1) * π)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
nth_rw : (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
⊢ (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
nth_rw 1 [← coe_toReal θ]

Premises used: Real.Angle.coe_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal
⊢ (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_sub_two_pi_iff, Set.mem_Ioc]

Premises used: two_mul, Real.Angle.coe_nsmul, Set.mem_Ioc, Real.Angle.toReal_coe_eq_self_sub_two_pi_iff, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h : π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π
linarith : θ.toReal ≤ π / 2 → 2 / 2 = 1
linarith₁ : θ.toReal ≤ π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : θ.toReal ≤ π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : θ.toReal ≤ π / 2 → π - 2 * θ.toReal + (2 * θ.toReal - 1 * π) = 0
⊢ π / 2 < θ.toReal

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

Tactic:
linarith [pi_pos, toReal_le_pi θ]

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

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

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]

Premises used: Real.Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi, two_zsmul, two_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
nth_rw : (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
⊢ (HSMul.hSMul (α := ℕ) 2 θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
nth_rw 1 [← coe_toReal θ]

Premises used: Real.Angle.coe_toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
rw : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2
⊢ (HSMul.hSMul (α := ℕ) 2 (↑θ.toReal : Angle)).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_add_two_pi_iff, Set.mem_Ioc]

Premises used: two_mul, Real.Angle.coe_nsmul, Set.mem_Ioc, Real.Angle.toReal_coe_eq_self_add_two_pi_iff, two_nsmul