awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
hx : Ne (α := ℝ) (↑n : ℝ) 0
hy : rexp 1 ≠ 0
hx₁ : 2 * π ≠ 0
hy₁ : Ne (α := ℝ) (↑n : ℝ) 0
⊢ (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
have rw : 0 ≤ 2 * π * (↑n : ℝ)
Tactic: rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
hx : Ne (α := ℝ) (↑n : ℝ) 0
hy : rexp 1 ≠ 0
hx₁ : 2 * π ≠ 0
hy₁ : Ne (α := ℝ) (↑n : ℝ) 0
rw : 0 ≤ 2 * π * (↑n : ℝ)
⊢ (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
have hx₂ : √(2 * π * (↑n : ℝ)) ≠ 0
Tactic: rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
hx : Ne (α := ℝ) (↑n : ℝ) 0
hy : rexp 1 ≠ 0
hx₁ : 2 * π ≠ 0
hy₁ : Ne (α := ℝ) (↑n : ℝ) 0
rw : 0 ≤ 2 * π * (↑n : ℝ)
hx₂ : √(2 * π * (↑n : ℝ)) ≠ 0
⊢ (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
have hy₂ : ((↑n : ℝ) / rexp 1) ^ n ≠ 0
Tactic: rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n : ℝ) * log (↑n : ℝ) - (↑n : ℝ) + log (↑n : ℝ) / 2 + log (2 * π) / 2 ≤ log (↑n ! : ℝ)
have _ : (↑n : ℝ) * log (↑n : ℝ) - (↑n : ℝ) + log (↑n : ℝ) / 2 + log (2 * π) / 2 =
  (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1)
Tactic: calc
    _ = (log (2 * π) + log n) / 2 + n * (log n - 1) := by ring
    _ = log (√(2 * π * n) * (n / rexp 1) ^ n) := by
      rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp] <;>
      positivity
    _ ≤ _ := log_le_log (by positivity) (le_factorial_stirling n)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
_ :
  (↑n : ℝ) * log (↑n : ℝ) - (↑n : ℝ) + log (↑n : ℝ) / 2 + log (2 * π) / 2 =
    (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1)
⊢ (↑n : ℝ) * log (↑n : ℝ) - (↑n : ℝ) + log (↑n : ℝ) / 2 + log (2 * π) / 2 ≤ log (↑n ! : ℝ)
have _₁ : (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
Tactic: calc
    _ = (log (2 * π) + log n) / 2 + n * (log n - 1) := by ring
    _ = log (√(2 * π * n) * (n / rexp 1) ^ n) := by
      rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp] <;>
      positivity
    _ ≤ _ := log_le_log (by positivity) (le_factorial_stirling n)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : ℝ
⊢ (↑θ : Angle) = (↑ψ : Angle) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)
have simp : (↑ψ : Angle) = (↑θ : Angle) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)
Tactic: simp only [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : ℝ
⊢ (↑ψ : Angle) = (↑θ : Angle) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)
have rw : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)) (-ψ + θ) ↔ ∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)
Tactic: rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ 2 * π - 0 = 2 * π * (↑1 : ℝ)
have rw : 2 * π = 2 * π * (↑1 : ℝ)
Tactic: rw [sub_zero, Int.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : 2 * π = 2 * π * (↑1 : ℝ)
⊢ 2 * π - 0 = 2 * π * (↑1 : ℝ)
have rw₁ : 2 * π = 2 * π * 1
Tactic: rw [sub_zero, Int.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : 2 * π = 2 * π * (↑1 : ℝ)
rw₁ : 2 * π = 2 * π * 1
⊢ 2 * π - 0 = 2 * π * (↑1 : ℝ)
have rw₂ : 2 * π = 2 * π
Tactic: rw [sub_zero, Int.cast_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ -(↑π : Angle) = (↑π : Angle)
have rw : ∃ (k : ℤ), -π - π = 2 * π * (↑k : ℝ)
Tactic: rw [← coe_neg, angle_eq_iff_two_pi_dvd_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ ∃ (k : ℤ), -π - π = 2 * π * (↑k : ℝ)
have h : -π - π = 2 * π * (↑(-1) : ℝ)
Tactic: use -1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ HSMul.hSMul (α := ℕ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)
have rw : (↑(HSMul.hSMul (α := ℕ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
Tactic: rw [← coe_nsmul, two_nsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
rw : (↑(HSMul.hSMul (α := ℕ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)
have rw₁ : (↑(θ / 2 + θ / 2) : Angle) = (↑θ : Angle)
Tactic: rw [← coe_nsmul, two_nsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
rw : (↑(HSMul.hSMul (α := ℕ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
rw₁ : (↑(θ / 2 + θ / 2) : Angle) = (↑θ : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)
have rw₂ : (↑θ : Angle) = (↑θ : Angle)
Tactic: rw [← coe_nsmul, two_nsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ HSMul.hSMul (α := ℤ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)
have rw : (↑(HSMul.hSMul (α := ℤ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
Tactic: rw [← coe_zsmul, two_zsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
rw : (↑(HSMul.hSMul (α := ℤ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)
have rw₁ : (↑(θ / 2 + θ / 2) : Angle) = (↑θ : Angle)
Tactic: rw [← coe_zsmul, two_zsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
rw : (↑(HSMul.hSMul (α := ℤ) 2 (θ / 2)) : Angle) = (↑θ : Angle)
rw₁ : (↑(θ / 2 + θ / 2) : Angle) = (↑θ : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (↑(θ / 2) : Angle) = (↑θ : Angle)
have rw₂ : (↑θ : Angle) = (↑θ : Angle)
Tactic: rw [← coe_zsmul, two_zsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ HSMul.hSMul (α := ℕ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
have rw : (↑(-π) : Angle) = (↑π : Angle)
Tactic: rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑(-π) : Angle) = (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
have rw₁ : -(↑π : Angle) = (↑π : Angle)
Tactic: rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑(-π) : Angle) = (↑π : Angle)
rw₁ : -(↑π : Angle) = (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
have rw₂ : (↑π : Angle) = (↑π : Angle)
Tactic: rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ HSMul.hSMul (α := ℤ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
have rw : (↑(-π / 2) : Angle) + (↑(-π / 2) : Angle) = (↑π : Angle)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_neg_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑(-π / 2) : Angle) + (↑(-π / 2) : Angle) = (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
have rw₁ : HSMul.hSMul (α := ℕ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_neg_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑(-π / 2) : Angle) + (↑(-π / 2) : Angle) = (↑π : Angle)
rw₁ : HSMul.hSMul (α := ℕ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (↑(-π / 2) : Angle) = (↑π : Angle)
have rw₂ : (↑π : Angle) = (↑π : Angle)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_neg_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ - (↑π : Angle) = θ + (↑π : Angle)
have rw : θ + -(↑π : Angle) = θ + (↑π : Angle)
Tactic: rw [sub_eq_add_neg, neg_coe_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ + -(↑π : Angle) = θ + (↑π : Angle)
⊢ θ - (↑π : Angle) = θ + (↑π : Angle)
have rw₁ : θ + (↑π : Angle) = θ + (↑π : Angle)
Tactic: rw [sub_eq_add_neg, neg_coe_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑π : Angle) + (↑π : Angle) = 0
have rw : HSMul.hSMul (α := ℕ) 2 (↑π : Angle) = 0
Tactic: rw [← two_nsmul, two_nsmul_coe_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : HSMul.hSMul (α := ℕ) 2 (↑π : Angle) = 0
⊢ (↑π : Angle) + (↑π : Angle) = 0
have rw₁ : Eq (α := Angle) 0 0
Tactic: rw [← two_nsmul, two_nsmul_coe_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
ψ θ : Angle
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have this : Int.natAbs 2 = 2
Tactic: have : Int.natAbs 2 = 2 := rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₂ : ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
  ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₃ : ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
  ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₃ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₄ : ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨
    ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
  ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₃ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₄ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨
      ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₅ : ψ = θ + 0 ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₃ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₄ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨
      ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₅ : ψ = θ + 0 ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₆ : ψ = θ ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₃ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₄ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨
      ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₅ : ψ = θ + 0 ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₆ : ψ = θ ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₇ : ψ = θ ∨ ψ = θ + (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₃ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₄ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨
      ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₅ : ψ = θ + 0 ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₆ : ψ = θ ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₇ : ψ = θ ∨ ψ = θ + (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₈ : ψ = θ ∨ ψ = θ + (↑(2 * π / 2) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
this : Int.natAbs 2 = 2
rw : (∃ (k : Fin (Int.natAbs 2)), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₁ : (∃ (k : Fin 2), ψ = θ + (↑k : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle)) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₂ :
  ψ = θ + (↑0 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₃ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨ ψ = θ + (↑1 : ℕ) • (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₄ :
  ψ = θ + HSMul.hSMul (α := ℕ) 0 (↑(2 * π / (↑2 : ℝ)) : Angle) ∨
      ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔
    ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₅ : ψ = θ + 0 ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₆ : ψ = θ ∨ ψ = θ + HSMul.hSMul (α := ℕ) 1 (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₇ : ψ = θ ∨ ψ = θ + (↑(2 * π / (↑2 : ℝ)) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
rw₈ : ψ = θ ∨ ψ = θ + (↑(2 * π / 2) : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have rw₉ : ψ = θ ∨ ψ = θ + (↑π : Angle) ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
⊢ HSMul.hSMul (α := ℕ) 2 ψ = HSMul.hSMul (α := ℕ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have simp_rw : HSMul.hSMul (α := ℤ) (↑2 : ℤ) ψ = HSMul.hSMul (α := ℤ) (↑2 : ℤ) θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: simp_rw [← natCast_zsmul, Nat.cast_ofNat, two_zsmul_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ θ : Angle
simp_rw : HSMul.hSMul (α := ℤ) (↑2 : ℤ) ψ = HSMul.hSMul (α := ℤ) (↑2 : ℤ) θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 ψ = HSMul.hSMul (α := ℕ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
have simp_rw₁ : HSMul.hSMul (α := ℤ) 2 ψ = HSMul.hSMul (α := ℤ) 2 θ ↔ ψ = θ ∨ ψ = θ + (↑π : Angle)
Tactic: simp_rw [← natCast_zsmul, Nat.cast_ofNat, two_zsmul_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have h : 0 = HSMul.hSMul (α := ℕ) (β := Angle) 2 0
Tactic: convert! two_nsmul_eq_iff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : 0 = HSMul.hSMul (α := ℕ) (β := Angle) 2 0
⊢ HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have h₁ : (↑π : Angle) = 0 + (↑π : Angle)
Tactic: convert! two_nsmul_eq_iff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw : HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
Tactic: rw [← not_or, ← two_nsmul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
⊢ HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw₁ : HSMul.hSMul (α := ℕ) 2 θ ≠ 0 ↔ ¬HSMul.hSMul (α := ℕ) 2 θ = 0
Tactic: rw [← not_or, ← two_nsmul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ HSMul.hSMul (α := ℤ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have simp_rw : θ + θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
simp_rw : θ + θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have simp_rw₁ : HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw : HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
Tactic: rw [← not_or, ← two_zsmul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
⊢ HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw₁ : HSMul.hSMul (α := ℤ) 2 θ ≠ 0 ↔ ¬HSMul.hSMul (α := ℤ) 2 θ = 0
Tactic: rw [← not_or, ← two_zsmul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ = -θ ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw : θ + θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [← add_eq_zero_iff_eq_neg, ← two_nsmul, two_nsmul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ + θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ = -θ ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw₁ : HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [← add_eq_zero_iff_eq_neg, ← two_nsmul, two_nsmul_eq_zero_iff]