awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ + θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
rw₁ : HSMul.hSMul (α := ℕ) 2 θ = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ = -θ ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw₂ : θ = 0 ∨ θ = (↑π : Angle) ↔ θ = 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
⊢ θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw : θ ≠ -θ ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
Tactic: rw [← not_or, ← eq_neg_self_iff.not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ ≠ -θ ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
⊢ θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw₁ : θ ≠ -θ ↔ ¬θ = -θ
Tactic: rw [← not_or, ← eq_neg_self_iff.not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ -θ = θ ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw : θ = -θ ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [eq_comm, eq_neg_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ = -θ ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ -θ = θ ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw₁ : θ = 0 ∨ θ = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [eq_comm, eq_neg_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw : -θ ≠ θ ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
Tactic: rw [← not_or, ← neg_eq_self_iff.not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : -θ ≠ θ ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
⊢ -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw₁ : -θ ≠ θ ↔ ¬-θ = θ
Tactic: rw [← not_or, ← neg_eq_self_iff.not]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
have rw : (↑π : Angle) = (↑(π / 2 + π / 2) : Angle)
Tactic: rw [two_nsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (↑π : Angle) = (↑(π / 2 + π / 2) : Angle)
⊢ (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
have rw₁ : (↑π : Angle) = (↑π : Angle)
Tactic: rw [two_nsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ : Angle
⊢ HSMul.hSMul (α := ℕ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
Tactic: have h : (π : Angle) = ((2 : ℕ) • (π / 2 : ℝ) :) := by rw [two_nsmul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have nth_rw : HSMul.hSMul (α := ℕ) 2 θ = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle) ↔
  θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: nth_rw 1 [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
⊢ HSMul.hSMul (α := ℕ) 2 θ = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle) ↔
    θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw : θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [coe_nsmul, two_nsmul_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
⊢ θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have a : (θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle)) = (θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle))
Tactic: apply iff_of_eq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
⊢ (θ = (↑(π / 2) : Angle) ∨ θ = (↑(π / 2) : Angle) + (↑π : Angle)) = (θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle))
have a : (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₄ : (↑(π + π / 2 - -(π / 2)) : Angle) = 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
a₄ : (↑(π + π / 2 - -(π / 2)) : Angle) = 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₅ : (↑(π + π / 2 + π / 2) : Angle) = 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
a₄ : (↑(π + π / 2 - -(π / 2)) : Angle) = 0
a₅ : (↑(π + π / 2 + π / 2) : Angle) = 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₆ : (↑(π + (π / 2 + π / 2)) : Angle) = 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
a₄ : (↑(π + π / 2 - -(π / 2)) : Angle) = 0
a₅ : (↑(π + π / 2 + π / 2) : Angle) = 0
a₆ : (↑(π + (π / 2 + π / 2)) : Angle) = 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₇ : (↑(π + π) : Angle) = 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
a₄ : (↑(π + π / 2 - -(π / 2)) : Angle) = 0
a₅ : (↑(π + π / 2 + π / 2) : Angle) = 0
a₆ : (↑(π + (π / 2 + π / 2)) : Angle) = 0
a₇ : (↑(π + π) : Angle) = 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₈ : (↑(2 * π) : Angle) = 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : (↑π : Angle) = (↑(HSMul.hSMul (α := ℕ) 2 (π / 2)) : Angle)
a : (↑π : Angle) + (↑(π / 2) : Angle) = (↑(-π / 2) : Angle)
a₁ : (↑(π + π / 2) : Angle) = (↑(-π / 2) : Angle)
a₂ : (↑(π + π / 2) : Angle) - (↑(-π / 2) : Angle) = 0
a₃ : (↑(π + π / 2 - -π / 2) : Angle) = 0
a₄ : (↑(π + π / 2 - -(π / 2)) : Angle) = 0
a₅ : (↑(π + π / 2 + π / 2) : Angle) = 0
a₆ : (↑(π + (π / 2 + π / 2)) : Angle) = 0
a₇ : (↑(π + π) : Angle) = 0
a₈ : (↑(2 * π) : Angle) = 0
⊢ (↑(π / 2) : Angle) + (↑π : Angle) = (↑(-π / 2) : Angle)
have a₉ : Eq (α := Angle) 0 0
Tactic: rw [add_comm, ← coe_add, ← sub_eq_zero, ← coe_sub, neg_div, sub_neg_eq_add, add_assoc,
    add_halves, ← two_mul, coe_two_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ HSMul.hSMul (α := ℤ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw : θ + θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ + θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₁ : HSMul.hSMul (α := ℕ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ + θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : HSMul.hSMul (α := ℕ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ HSMul.hSMul (α := ℤ) 2 θ = (↑π : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₂ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [two_zsmul, ← two_nsmul, two_nsmul_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ cos θ = cos ψ ↔ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
have mp : cos θ = cos ψ → (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
mp : cos θ = cos ψ → (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
⊢ cos θ = cos ψ ↔ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
have mpr : (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle) → cos θ = cos ψ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
have Hcos₁ : (∃ (n : ℤ), (↑n : ℝ) * π = (θ + ψ) / 2) ∨ ∃ (n : ℤ), (↑n : ℝ) * π = (θ - ψ) / 2
Tactic: rw [← sub_eq_zero, cos_sub_cos, mul_eq_zero, mul_eq_zero, neg_eq_zero,
      eq_false (two_ne_zero' ℝ), false_or, sin_eq_zero_iff, sin_eq_zero_iff] at Hcos
Cleared hypotheses: Hcos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hcos : (∃ (n : ℤ), (↑n : ℝ) * π = (θ + ψ) / 2) ∨ ∃ (n : ℤ), (↑n : ℝ) * π = (θ - ψ) / 2
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
have mp : ∀ (n : ℤ) (hn : (↑n : ℝ) * π = (θ + ψ) / 2), (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
Tactic: rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)
Cleared hypotheses: Hcos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hcos : (∃ (n : ℤ), (↑n : ℝ) * π = (θ + ψ) / 2) ∨ ∃ (n : ℤ), (↑n : ℝ) * π = (θ - ψ) / 2
mp : ∀ (n : ℤ) (hn : (↑n : ℝ) * π = (θ + ψ) / 2), (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
have mp₁ : ∀ (n : ℤ) (hn : (↑n : ℝ) * π = (θ - ψ) / 2), (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
Tactic: rcases Hcos with (⟨n, hn⟩ | ⟨n, hn⟩)
Cleared hypotheses: Hcos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ + ψ) / 2
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
have mp : (↑θ : Angle) = -(↑ψ : Angle)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ + ψ) / 2
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have hn₁ : (↑n : ℝ) * π * 2 - ψ = θ
Tactic: rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), ← sub_eq_iff_eq_add] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₃ : (↑((↑n : ℝ) * π * 2) : Angle) = 0
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
mp₃ : (↑((↑n : ℝ) * π * 2) : Angle) = 0
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₄ : (↑((↑n : ℝ) * (π * 2)) : Angle) = 0
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
mp₃ : (↑((↑n : ℝ) * π * 2) : Angle) = 0
mp₄ : (↑((↑n : ℝ) * (π * 2)) : Angle) = 0
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₅ : n • (↑(π * 2) : Angle) = 0
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
mp₃ : (↑((↑n : ℝ) * π * 2) : Angle) = 0
mp₄ : (↑((↑n : ℝ) * (π * 2)) : Angle) = 0
mp₅ : n • (↑(π * 2) : Angle) = 0
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₆ : n • (↑(2 * π) : Angle) = 0
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
mp₃ : (↑((↑n : ℝ) * π * 2) : Angle) = 0
mp₄ : (↑((↑n : ℝ) * (π * 2)) : Angle) = 0
mp₅ : n • (↑(π * 2) : Angle) = 0
mp₆ : n • (↑(2 * π) : Angle) = 0
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₇ : HSMul.hSMul (β := Angle) n 0 = 0
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 - ψ = θ
mp : (↑((↑n : ℝ) * π * 2 - ψ) : Angle) = -(↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) = -(↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * π * 2) : Angle) - (↑ψ : Angle) + (↑ψ : Angle) = 0
mp₃ : (↑((↑n : ℝ) * π * 2) : Angle) = 0
mp₄ : (↑((↑n : ℝ) * (π * 2)) : Angle) = 0
mp₅ : n • (↑(π * 2) : Angle) = 0
mp₆ : n • (↑(2 * π) : Angle) = 0
mp₇ : HSMul.hSMul (β := Angle) n 0 = 0
⊢ (↑θ : Angle) = -(↑ψ : Angle)
have mp₈ : Eq (α := Angle) 0 0
Tactic: rw [← hn, coe_sub, eq_neg_iff_add_eq_zero, sub_add_cancel, mul_assoc, intCast_mul_eq_zsmul,
        mul_comm, coe_two_pi, zsmul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ - ψ) / 2
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle)
have mp : (↑θ : Angle) = (↑ψ : Angle)
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π = (θ - ψ) / 2
⊢ (↑θ : Angle) = (↑ψ : Angle)
have hn₁ : (↑n : ℝ) * π * 2 + ψ = θ
Tactic: rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
Tactic: rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
Tactic: rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp₂ : (↑((↑n : ℝ) * (π * 2)) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
Tactic: rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * (π * 2)) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp₃ : n • (↑(π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
Tactic: rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * (π * 2)) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₃ : n • (↑(π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp₄ : n • (↑(2 * π) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
Tactic: rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * (π * 2)) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₃ : n • (↑(π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₄ : n • (↑(2 * π) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp₅ : HSMul.hSMul (β := Angle) n 0 + (↑ψ : Angle) = (↑ψ : Angle)
Tactic: rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
n : ℤ
hn : (↑n : ℝ) * π * 2 + ψ = θ
mp : (↑((↑n : ℝ) * π * 2 + ψ) : Angle) = (↑ψ : Angle)
mp₁ : (↑((↑n : ℝ) * π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₂ : (↑((↑n : ℝ) * (π * 2)) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₃ : n • (↑(π * 2) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₄ : n • (↑(2 * π) : Angle) + (↑ψ : Angle) = (↑ψ : Angle)
mp₅ : HSMul.hSMul (β := Angle) n 0 + (↑ψ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp₆ : 0 + (↑ψ : Angle) = (↑ψ : Angle)
Tactic: rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]