awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
rw : -π < θ.toReal + ψ.toReal ∧ θ.toReal + ψ.toReal ≤ π
⊢ (↑(θ.toReal + ψ.toReal) : Angle).toReal = θ.toReal + ψ.toReal

Tactic:
rw [toReal_coe_eq_self_iff]

Premises used: Real.Angle.toReal_coe_eq_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ -π < θ.toReal + ψ.toReal ∧ θ.toReal + ψ.toReal ≤ π

Tactic:
grind [toReal_mem_Ioc, toReal_neg_iff_sign_neg, toReal_mem_Ioo_iff_sign_pos]

Premises used: Real.Angle.toReal_mem_Ioc, Real.Angle.toReal_mem_Ioo_iff_sign_pos, Real.Angle.toReal_neg_iff_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hψ : θ ≠ (↑π : Angle) ∨ ψ ≠ (↑π : Angle)
hs : θ.sign = -ψ.sign
inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inr : ∀ (h : ψ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
inr₁ : ∀ (h : ψ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (h | h | h) := ψ.sign.trichotomy

Premises used: SignType.trichotomy, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hψ : θ ≠ (↑π : Angle) ∨ ψ ≠ (↑π : Angle)
hs : θ.sign = -ψ.sign
h : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [neg_neg, add_comm, toReal_add_of_sign_pos_sign_neg]

Premises used: neg_neg, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hψ : θ ≠ (↑π : Angle) ∨ ψ ≠ (↑π : Angle)
hs : θ.sign = -ψ.sign
h : ψ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [neg_neg, add_comm, toReal_add_of_sign_pos_sign_neg]

Premises used: neg_neg, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hψ : θ ≠ (↑π : Angle) ∨ ψ ≠ (↑π : Angle)
hs : θ.sign = -ψ.sign
h : ψ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [neg_neg, add_comm, toReal_add_of_sign_pos_sign_neg]

Premises used: neg_neg, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign
inl : ∀ (hs : θ.sign ≠ ψ.sign), (θ + ψ).toReal = θ.toReal + ψ.toReal
inr : ∀ (hs : θ.sign = (θ + ψ).sign), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (hs | hs) := hs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : ψ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₂ : ∀ (h : ψ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (h | h | h) := ψ.sign.trichotomy

Premises used: SignType.trichotomy, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = -1
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₂ : ∀ (h : θ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (h | h | h) := θ.sign.trichotomy

Premises used: SignType.trichotomy, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 0
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₂ : ∀ (h : θ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (h | h | h) := θ.sign.trichotomy

Premises used: SignType.trichotomy, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 1
inl : ∀ (h : θ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : θ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₂ : ∀ (h : θ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
obtain (h | h | h) := θ.sign.trichotomy

Premises used: SignType.trichotomy, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = -1
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = -1
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = -1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = 0
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = 0
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = 0
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = 1
h : θ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = 1
h : θ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
h_1 : ψ.sign = 1
h : θ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]

Premises used: Real.Angle.sign_eq_zero_iff, add_comm, Real.Angle.toReal_add_of_sign_pos_sign_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign = (θ + ψ).sign
⊢ -(-θ).sign = (θ + ψ).sign

Tactic:
rw [← neg_neg θ.sign, ← sign_neg] at hs

Premises used: Real.Angle.sign_neg, neg_neg, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : -(-θ).sign = (θ + ψ).sign
⊢ -θ ≠ (↑π : Angle)

Tactic:
simpa [neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : -(-θ).sign = (θ + ψ).sign
⊢ (θ + ψ + -θ).toReal = (θ + ψ).toReal + (-θ).toReal

Tactic:
have := toReal_add_of_sign_eq_neg_sign (.inr <| by simpa [neg_eq_iff_eq_neg]) hs.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : -(-θ).sign = (θ + ψ).sign
this : (θ + ψ + -θ).toReal = (θ + ψ).toReal + (-θ).toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
simpa [toReal_neg_eq_neg_toReal_iff.mpr, hθ, ← sub_eq_add_neg, eq_sub_iff_add_eq', eq_comm]

Premises used: Iff.mpr, eq_sub_iff_add_eq', sub_eq_add_neg, Real.Angle.toReal_neg_eq_neg_toReal_iff, eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
⊢ θ.toReal ∈ Set.Ioo 0 π

Tactic:
rw [← toReal_mem_Ioo_iff_sign_pos] at hθs hψs

Premises used: Real.Angle.toReal_mem_Ioo_iff_sign_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
hθs₁ : θ.toReal ∈ Set.Ioo 0 π
⊢ ψ.toReal ∈ Set.Ioo 0 π

Tactic:
rw [← toReal_mem_Ioo_iff_sign_pos] at hθs hψs

Premises used: Real.Angle.toReal_mem_Ioo_iff_sign_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
hθs₁ : θ.toReal ∈ Set.Ioo 0 π
hψs₁ : ψ.toReal ∈ Set.Ioo 0 π
⊢ (θ + ψ).sign ≠ 1

Tactic:
rw [← toReal_mem_Ioo_iff_sign_pos] at hθs hψs

Premises used: Real.Angle.toReal_mem_Ioo_iff_sign_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
⊢ (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
⊢ (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)

Tactic:
have : ((θ + ψ).toReal : Angle) = ↑(θ.toReal + ψ.toReal) := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
obtain :
  ∀ (k : ℤ) (hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)),
    |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
obtain ⟨k, hk⟩ := angle_eq_iff_two_pi_dvd_sub.mp this

Premises used: Real.Angle.angle_eq_iff_two_pi_dvd_sub, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
⊢ (θ + ψ).sign = -1 ∨ (θ + ψ).sign = 0 ∨ (θ + ψ).sign = 1

Tactic:
have := (θ + ψ).sign.trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this_1 : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
this : (θ + ψ).sign = -1 ∨ (θ + ψ).sign = 0 ∨ (θ + ψ).sign = 1
⊢ (θ + ψ).toReal ≤ 0 ∨ θ + ψ = (↑π : Angle)

Tactic:
grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]

Premises used: Real.Angle.sign_eq_zero_iff, Real.Angle.toReal_neg_iff_sign_neg, Real.Angle.toReal_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
inl : ∀ (h : (θ + ψ).toReal ≤ 0), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
inr : ∀ (h : θ + ψ = (↑π : Angle)), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
obtain (h | h) : (θ + ψ).toReal ≤ 0 ∨ θ + ψ = π := by
    have := (θ + ψ).sign.trichotomy
    grind [sign_eq_zero_iff, toReal_eq_zero_iff, toReal_neg_iff_sign_neg]

Premises used: HAdd.hAdd, Real.Angle.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : (θ + ψ).toReal ≤ 0
⊢ 2 * π * (↑k : ℝ) ∈ Set.Ioo (2 * π * (↑(HSub.hSub (α := ℤ) (-1) 1) : ℝ)) (2 * π * (↑(HAdd.hAdd (α := ℤ) (-1) 1) : ℝ))

Tactic:
grind [toReal_mem_Ioc]

Premises used: Real.Angle.toReal_mem_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : (θ + ψ).toReal ≤ 0
⊢ (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑(-1) : ℝ)

Tactic:
obtain rfl : k = -1 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos <| by
      grind [toReal_mem_Ioc]

Premises used: Real.two_pi_pos, IsStrictOrderedRing.int_eq_of_mul_mem_Ioo, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
h : (θ + ψ).toReal ≤ 0
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑(-1) : ℝ)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
grind [abs_of_nonpos]

Premises used: abs_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : (↑(θ + ψ).toReal : Angle) = (↑(θ.toReal + ψ.toReal) : Angle)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : θ + ψ = (↑π : Angle)
inr :
  ∀ (hk : π - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)) (h : θ + ψ = (↑π : Angle)),
    π = 2 * π - (|θ.toReal| + |ψ.toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
simp_all only [sign_coe_pi, ne_eq, zero_ne_one, not_false_eq_true, toReal_pi, coe_add,
      coe_toReal, pi_pos, abs_of_pos]

Premises used: Real.Angle.toReal_pi, Real.Angle.coe_add, zero_ne_one, Real.Angle.sign_coe_pi, Real.pi_pos, ne_eq, Real.Angle.coe_toReal, abs_of_pos, not_false_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
k : ℤ
hk : π - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : θ + ψ = (↑π : Angle)
⊢ 2 * π * (↑k : ℝ) ∈ Set.Ioo (2 * π * (↑(HSub.hSub (α := ℤ) 0 1) : ℝ)) (2 * π * (↑(HAdd.hAdd (α := ℤ) 0 1) : ℝ))

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
k : ℤ
hk : π - (θ.toReal + ψ.toReal) = 2 * π * (↑k : ℝ)
h : θ + ψ = (↑π : Angle)
⊢ π - (θ.toReal + ψ.toReal) = 2 * π * (↑0 : ℝ)

Tactic:
obtain rfl : k = 0 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos (by grind)

Premises used: Real.two_pi_pos, IsStrictOrderedRing.int_eq_of_mul_mem_Ioo, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
h : θ + ψ = (↑π : Angle)
hk : π - (θ.toReal + ψ.toReal) = 2 * π * (↑0 : ℝ)
⊢ π = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
inl : ∀ (h : θ.sign = -1), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
inr : ∀ (h : θ.sign = 0), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
inr₁ : ∀ (h : θ.sign = 1), |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
obtain h | h | h := θ.sign.trichotomy

Premises used: SignType.trichotomy, Real.Angle.sign
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
⊢ (-θ).sign = 1 ∧ (-ψ).sign = 1

Tactic:
grind [sign_neg, neg_neg]

Premises used: Real.Angle.sign_neg, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
⊢ (-θ).sign = 1

Tactic:
obtain ⟨hθ', hψ'⟩ : (-θ).sign = 1 ∧ (-ψ).sign = 1 := by grind [sign_neg, neg_neg]

Premises used: Real.Angle.sign, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
⊢ (-ψ).sign = 1

Tactic:
obtain ⟨hθ', hψ'⟩ : (-θ).sign = 1 ∧ (-ψ).sign = 1 := by grind [sign_neg, neg_neg]

Premises used: Real.Angle.sign, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
rwa : (-θ + -ψ).sign ≠ (-θ).sign
rwa₁ : (-θ).sign ≠ (-θ + -ψ).sign
rwa₂ : (-θ).sign ≠ (-(θ + ψ)).sign
rwa₃ : -θ.sign ≠ (-(θ + ψ)).sign
rwa₄ : -θ.sign ≠ -(θ + ψ).sign
rwa₅ rwa₆ rwa₇ rwa₈ : θ.sign ≠ (θ + ψ).sign
⊢ (-θ + -ψ).sign ≠ 1

Tactic:
rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]

Premises used: Real.Angle.sign_neg, neg_injective, neg_add, Function.Injective.ne_iff, ne_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
⊢ (-θ + -ψ).sign ≠ 1

Tactic:
have hsa' : (-θ + -ψ).sign ≠ 1 := by
      rwa [← hθ', ne_comm, ← neg_add, sign_neg, sign_neg, neg_injective.ne_iff]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ |(-θ + -ψ).toReal| = 2 * π - (|(-θ).toReal| + |(-ψ).toReal|)

Tactic:
abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux hθ' hψ' hsa'

Premises used: _private.0.Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
h₁ : |(θ + ψ).toReal| = |(-θ + -ψ).toReal|
h₂ : 2 * π - (|θ.toReal| + |ψ.toReal|) = 2 * π - (|(-θ).toReal| + |(-ψ).toReal|)
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
convert! abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux hθ' hψ' hsa' using 1

Premises used: _private.0.Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = |(-θ + -ψ).toReal|

Tactic:
simp [-neg_add_rev, ← neg_add, abs_toReal_neg]

Premises used: neg_add_rev, Real.Angle.abs_toReal_neg, neg_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ 2 * π - (|θ.toReal| + |ψ.toReal|) = 2 * π - (|(-θ).toReal| + |(-ψ).toReal|)

Tactic:
simp [-neg_add_rev, ← neg_add, abs_toReal_neg]

Premises used: neg_add_rev, Real.Angle.abs_toReal_neg, neg_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
grind [sign_eq_zero_iff, coe_pi_add_coe_pi]

Premises used: Real.Angle.sign_eq_zero_iff, Real.Angle.coe_pi_add_coe_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux h (hs ▸ h) (h ▸ hsa.symm)

Premises used: _private.0.Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux, Eq.rec, Ne.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
exact abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux h (hs ▸ h) (h ▸ hsa.symm)

Premises used: _private.0.Real.Angle.abs_toReal_add_eq_two_pi_sub_abs_toReal_add_abs_toReal_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
θ : Angle
h0 : θ ≠ 0
hpi : θ ≠ (↑π : Angle)
⊢ ContinuousAt sign θ

Tactic:
(continuousAt_sign_of_ne_zero (sin_ne_zero_iff.2 ⟨h0, hpi⟩)).comp continuous_sin.continuousAt

Premises used: Iff.mpr, Continuous.continuousAt, Real.Angle.sign, Real.Angle.sin_ne_zero_iff, And.intro, Real.Angle.continuous_sin, ContinuousAt.comp, continuousAt_sign_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
⊢ ContinuousOn (sign ∘ f) s

Tactic:
(continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)

Premises used: continuousOn_of_forall_continuousAt, Set.mapsTo_image, ContinuousOn.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
refine : ∀ (θ : Angle) (hθ : θ ∈ f '' s), ContinuousAt sign θ
⊢ ContinuousOn (sign ∘ f) s

Tactic:
refine (continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)

Premises used: continuousOn_of_forall_continuousAt, Set.mapsTo_image, ContinuousOn.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
θ : Angle
hθ : θ ∈ f '' s
obtain : ∀ (z : α) (hz : z ∈ s), ContinuousAt sign (f z)
⊢ ContinuousAt sign θ

Tactic:
obtain ⟨z, hz, rfl⟩ := hθ

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
z : α
hz : z ∈ s
⊢ ContinuousAt sign (f z)

Tactic:
continuousAt_sign (hs _ hz).1 (hs _ hz).2

Premises used: Real.Angle.continuousAt_sign, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
z : α
hz : z ∈ s
⊢ ContinuousAt sign (f z)

Tactic:
exact continuousAt_sign (hs _ hz).1 (hs _ hz).2

Premises used: Real.Angle.continuousAt_sign, And.right, And.left