awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑(π / 2) : Angle).sin : SignType) (1 : SignType)
⊢ (↑(π / 2) : Angle).sign = 1
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin (π / 2)) : SignType) (1 : SignType)
Tactic: rw [sign, sin_coe, sin_pi_div_two, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
⊢ (↑(π / 2) : Angle).sign = 1
have rw₂ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 1 : SignType) (1 : SignType)
Tactic: rw [sign, sin_coe, sin_pi_div_two, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
⊢ (↑(π / 2) : Angle).sign = 1
have rw₃ : Eq (α := SignType) 1 1
Tactic: rw [sign, sin_coe, sin_pi_div_two, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑(-π / 2) : Angle).sign = -1
have rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑(-π / 2) : Angle).sin : SignType) (-1 : SignType)
Tactic: rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑(-π / 2) : Angle).sin : SignType) (-1 : SignType)
⊢ (↑(-π / 2) : Angle).sign = -1
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin (-π / 2)) : SignType) (-1 : SignType)
Tactic: rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
⊢ (↑(-π / 2) : Angle).sign = -1
have rw₂ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin (-(π / 2))) : SignType) (-1 : SignType)
Tactic: rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
⊢ (↑(-π / 2) : Angle).sign = -1
have rw₃ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-Real.sin (π / 2)) : SignType) (-1 : SignType)
Tactic: rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
⊢ (↑(-π / 2) : Angle).sign = -1
have rw₄ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-1) : SignType) (-1 : SignType)
Tactic: rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
⊢ (↑(-π / 2) : Angle).sign = -1
have rw₅ : Eq (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) 1 : SignType) (-1 : SignType)
Tactic: rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
⊢ (↑(-π / 2) : Angle).sign = -1
have rw₆ : Eq (α := SignType) (-1) (-1)
Tactic: rw [sign, sin_coe, neg_div, Real.sin_neg, sin_pi_div_two, Left.sign_neg, sign_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ : Angle).sign
have rw : 0 ≤ (↑θ : Angle).sin
Tactic: rw [sign, sign_nonneg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ (-(↑θ : Angle)).sign ≤ 0
have rw : 0 ≤ (↑θ : Angle).sin
Tactic: rw [sign, sign_nonpos_iff, sin_neg, Left.neg_nonpos_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℕ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
have simp : |θ.toReal| < π / 2 ∨ θ = 0 ∨ θ = (↑π : Angle) ↔ θ = (↑π : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ : Angle
⊢ |θ.toReal| < π / 2 ∨ θ = 0 ∨ θ = (↑π : Angle) ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
have this : 0 < π / 2
Tactic: have : 0 < π / 2 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
have rw : (θ + θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
Tactic: rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
have rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
Tactic: rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = θ.sign ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
have rw₂ : θ = (↑π : Angle) ∨ |θ.toReal| < π / 2 ↔ θ = (↑π : Angle) ∨ |θ.toReal| < π / 2
Tactic: rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_sign_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
have rw : (θ + θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
Tactic: rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_neg_sign_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
have rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
Tactic: rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_neg_sign_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
rw₁ : (HSMul.hSMul (α := ℕ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
⊢ (HSMul.hSMul (α := ℤ) 2 θ).sign = -θ.sign ↔ θ = 0 ∨ π / 2 < |θ.toReal|
have rw₂ : θ = 0 ∨ π / 2 < |θ.toReal| ↔ θ = 0 ∨ π / 2 < |θ.toReal|
Tactic: rw [two_zsmul, ← two_nsmul, sign_two_nsmul_eq_neg_sign_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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 + (↑π : Angle)
have h1 : a = b ∨ a = b + (↑π : Angle)
Tactic: have h1 := Real.Angle.two_zsmul_eq_iff.mp h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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)
have refine : ¬a = b
Tactic: refine h1.resolve_left ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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)
⊢ False
have h_sign₁ : a.sign = 0
Tactic: simp only [SignType.self_eq_neg_iff] at h_sign
Cleared hypotheses: h_sign
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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
⊢ False
have h_ne₁ : Ne (α := SignType) 0 0
Tactic: rw [h_sign] at h_ne
Cleared hypotheses: h_ne, h1, h_sign
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
a b : Angle
h_sign : a.sign = b.sign
h_ne : b.sign ≠ 0
h : a - b = (↑π : Angle)
⊢ False
have h' : a = b + (↑π : Angle)
Tactic: have h' : a = b + π := by
    simp [← h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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
⊢ False
have h_sign'₁ : -b.sign = b.sign
Tactic: rw [h', Real.Angle.sign_add_pi] at h_sign'
Cleared hypotheses: h_sign'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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
⊢ False
have h_sign'₁ : b.sign = 0
Tactic: simp only [SignType.neg_eq_self_iff] at h_sign'
Cleared hypotheses: h_sign'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ HSMul.hSMul (α := ℤ) 2 a = HSMul.hSMul (α := ℤ) 2 b ↔ a = b
have rw : a = b ∨ a = b + (↑π : Angle) ↔ a = b
Tactic: rw [Real.Angle.two_zsmul_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + (↑π : Angle) ↔ a = b
have mp : a = b ∨ a = b + (↑π : Angle) → a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
mp : a = b ∨ a = b + (↑π : Angle) → a = b
⊢ a = b ∨ a = b + (↑π : Angle) ↔ a = b
have mpr : a = b → a = b ∨ a = b + (↑π : Angle)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
a b : Angle
ha : a.sign ≠ 0
h_1 : a.sign = b.sign
h : a = b ∨ a = b + (↑π : Angle)
⊢ a = b
have mp : ∀ (h1 : a = b), a = b
Tactic: rcases h with h1 | h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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
⊢ a = b
have mp₁ : ∀ (h2 : a = b + (↑π : Angle)), a = b
Tactic: rcases h with h1 | h2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
⊢ a = b
have this : a.sign = (b + (↑π : Angle)).sign
Tactic: have : a.sign = (b + π).sign := by aesop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
this : a.sign = (b + (↑π : Angle)).sign
⊢ a = b
have this₁ : a.sign = -b.sign
Tactic: rw [Real.Angle.sign_add_pi] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + (↑π : Angle)
this : a.sign = -b.sign
⊢ a = b
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π
have inl : ∀ (h : θ + ψ = 0), |θ.toReal| + |ψ.toReal| = π
Tactic: rcases two_nsmul_eq_zero_iff.mp h with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
inl : ∀ (h : θ + ψ = 0), |θ.toReal| + |ψ.toReal| = π
⊢ |θ.toReal| + |ψ.toReal| = π
have inr : ∀ (h : θ + ψ = (↑π : Angle)), |θ.toReal| + |ψ.toReal| = π
Tactic: rcases two_nsmul_eq_zero_iff.mp h with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = (↑π : Angle)
⊢ |θ.toReal| + |ψ.toReal| = π
have h₁ : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
Tactic: rw [← coe_toReal θ, ← coe_toReal ψ, ← coe_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
⊢ |θ.toReal| + |ψ.toReal| = π
have inr : |θ.toReal + ψ.toReal| = π
Tactic: suffices |θ.toReal + ψ.toReal| = π by grind [toReal_neg_iff_sign_neg, abs_add_eq_add_abs_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
⊢ |θ.toReal + ψ.toReal| = π
have inr : θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Tactic: rw [abs_eq pi_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h_1 : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : (↑(θ.toReal + ψ.toReal) : Angle) = (↑π : Angle)
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
have inr : ∀ (k : ℤ) (hk : θ.toReal + ψ.toReal - π = 2 * π * (↑k : ℝ)), θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Tactic: rcases angle_eq_iff_two_pi_dvd_sub.mp h with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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 = π ∨ θ.toReal + ψ.toReal = -π
have hk₁ : θ.toReal + ψ.toReal = 2 * π * (↑k : ℝ) + π
Tactic: rw [sub_eq_iff_eq_add] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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 = π ∨ θ.toReal + ψ.toReal = -π
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
have inr : ∀
  (hk :
    θ.toReal + ψ.toReal =
      2 * π * (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-1)) : (a : ℕ) → ℤ) 0) : ℝ) + π),
  θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Tactic: fin_cases this
Cleared hypotheses: k, hk, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
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 = -π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
have inr₁ : ∀
  (hk :
    θ.toReal + ψ.toReal =
      2 * π * (↑((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (-1)) : (a : ℕ) → ℤ) 1) : ℝ) + π),
  θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Tactic: fin_cases this
Cleared hypotheses: k, hk, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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 = π ∨ θ.toReal + ψ.toReal = -π
have hk₁ : θ.toReal + ψ.toReal = -(2 * π) + π
Tactic: simp at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
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 = π ∨ θ.toReal + ψ.toReal = -π
have hk₁ : θ.toReal + ψ.toReal = π
Tactic: simp at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
⊢ |θ.toReal| + |ψ.toReal| = π
have h₁ : HSMul.hSMul (α := ℕ) 2 (θ + ψ) = 0
Tactic: rw [two_zsmul, ← two_nsmul] at h
Cleared hypotheses: h, hs, h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have suffices : (↑(θ.toReal + ψ.toReal) : Angle).toReal = θ.toReal + ψ.toReal
Tactic: suffices ((θ.toReal + ψ.toReal : ℝ) : Angle).toReal = θ.toReal + ψ.toReal by simpa using this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ.sign = 1
hψ : ψ.sign = -1
⊢ (↑(θ.toReal + ψ.toReal) : Angle).toReal = θ.toReal + ψ.toReal
have rw : -π < θ.toReal + ψ.toReal ∧ θ.toReal + ψ.toReal ≤ π
Tactic: rw [toReal_coe_eq_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hψ : θ ≠ (↑π : Angle) ∨ ψ ≠ (↑π : Angle)
hs : θ.sign = -ψ.sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := ψ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hψ : θ ≠ (↑π : Angle) ∨ ψ ≠ (↑π : Angle)
hs : θ.sign = -ψ.sign
inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inr : ∀ (h : ψ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := ψ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hψ : θ ≠ (↑π : Angle) ∨ ψ ≠ (↑π : Angle)
hs : θ.sign = -ψ.sign
inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inr : ∀ (h : ψ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inr₁ : ∀ (h : ψ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := ψ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl : ∀ (hs : θ.sign ≠ ψ.sign), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (hs | hs) := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign
inl : ∀ (hs : θ.sign ≠ ψ.sign), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inr : ∀ (hs : θ.sign = (θ + ψ).sign), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (hs | hs) := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := ψ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₁ : ∀ (h : ψ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := ψ.sign.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
hθ : θ ≠ (↑π : Angle)
hψ : ψ ≠ (↑π : Angle)
hs : θ.sign ≠ ψ.sign
inl : ∀ (h : ψ.sign = -1), (θ + ψ).toReal = θ.toReal + ψ.toReal
inl₁ : ∀ (h : ψ.sign = 0), (θ + ψ).toReal = θ.toReal + ψ.toReal
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
have inl₂ : ∀ (h : ψ.sign = 1), (θ + ψ).toReal = θ.toReal + ψ.toReal
Tactic: obtain (h | h | h) := ψ.sign.trichotomy