awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
mp₆ : 0 + (↑ψ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have mp₇ : (↑ψ : 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:
θ ψ : ℝ
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) = -(↑ψ : Angle) → cos θ = cos ψ
have mpr : ((∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)) ∨ ∃ (k : ℤ), θ - -ψ = 2 * π * (↑k : ℝ)) → cos θ = cos ψ
Tactic: rw [angle_eq_iff_two_pi_dvd_sub, ← coe_neg, angle_eq_iff_two_pi_dvd_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
⊢ cos θ = cos ψ
have mpr : cos θ - cos ψ = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
⊢ cos θ = cos ψ
have mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₂ : -2 * sin ((θ + ψ) / 2) * sin (2 * π * (↑k : ℝ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ + ψ) / 2) * sin (2 * π * (↑k : ℝ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₃ : -2 * sin ((θ + ψ) / 2) * sin (2 * (π * (↑k : ℝ)) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ + ψ) / 2) * sin (2 * π * (↑k : ℝ) / 2) = 0
mpr₃ : -2 * sin ((θ + ψ) / 2) * sin (2 * (π * (↑k : ℝ)) / 2) = 0
⊢ cos θ = cos ψ
have mpr₄ : -2 * sin ((θ + ψ) / 2) * sin (π * (↑k : ℝ)) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ + ψ) / 2) * sin (2 * π * (↑k : ℝ) / 2) = 0
mpr₃ : -2 * sin ((θ + ψ) / 2) * sin (2 * (π * (↑k : ℝ)) / 2) = 0
mpr₄ : -2 * sin ((θ + ψ) / 2) * sin (π * (↑k : ℝ)) = 0
⊢ cos θ = cos ψ
have mpr₅ : -2 * sin ((θ + ψ) / 2) * sin ((↑k : ℝ) * π) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ + ψ) / 2) * sin (2 * π * (↑k : ℝ) / 2) = 0
mpr₃ : -2 * sin ((θ + ψ) / 2) * sin (2 * (π * (↑k : ℝ)) / 2) = 0
mpr₄ : -2 * sin ((θ + ψ) / 2) * sin (π * (↑k : ℝ)) = 0
mpr₅ : -2 * sin ((θ + ψ) / 2) * sin ((↑k : ℝ) * π) = 0
⊢ cos θ = cos ψ
have mpr₆ : -2 * sin ((θ + ψ) / 2) * 0 = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ + ψ) / 2) * sin (2 * π * (↑k : ℝ) / 2) = 0
mpr₃ : -2 * sin ((θ + ψ) / 2) * sin (2 * (π * (↑k : ℝ)) / 2) = 0
mpr₄ : -2 * sin ((θ + ψ) / 2) * sin (π * (↑k : ℝ)) = 0
mpr₅ : -2 * sin ((θ + ψ) / 2) * sin ((↑k : ℝ) * π) = 0
mpr₆ : -2 * sin ((θ + ψ) / 2) * 0 = 0
⊢ cos θ = cos ψ
have mpr₇ : Eq (α := ℝ) 0 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
⊢ cos θ = cos ψ
have mpr : cos θ - cos ψ = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
⊢ cos θ = cos ψ
have mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₄ : -2 * sin (2 * (π * (↑k : ℝ)) / 2) * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₄ : -2 * sin (2 * (π * (↑k : ℝ)) / 2) * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₅ : -2 * sin (π * (↑k : ℝ)) * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₄ : -2 * sin (2 * (π * (↑k : ℝ)) / 2) * sin ((θ - ψ) / 2) = 0
mpr₅ : -2 * sin (π * (↑k : ℝ)) * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₆ : -2 * sin ((↑k : ℝ) * π) * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₄ : -2 * sin (2 * (π * (↑k : ℝ)) / 2) * sin ((θ - ψ) / 2) = 0
mpr₅ : -2 * sin (π * (↑k : ℝ)) * sin ((θ - ψ) / 2) = 0
mpr₆ : -2 * sin ((↑k : ℝ) * π) * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₇ : HMul.hMul (α := ℝ) (-2) 0 * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₄ : -2 * sin (2 * (π * (↑k : ℝ)) / 2) * sin ((θ - ψ) / 2) = 0
mpr₅ : -2 * sin (π * (↑k : ℝ)) * sin ((θ - ψ) / 2) = 0
mpr₆ : -2 * sin ((↑k : ℝ) * π) * sin ((θ - ψ) / 2) = 0
mpr₇ : HMul.hMul (α := ℝ) (-2) 0 * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₈ : 0 * sin ((θ - ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * (↑k : ℝ)
mpr : cos θ - cos ψ = 0
mpr₁ : -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₂ : -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₃ : -2 * sin (2 * π * (↑k : ℝ) / 2) * sin ((θ - ψ) / 2) = 0
mpr₄ : -2 * sin (2 * (π * (↑k : ℝ)) / 2) * sin ((θ - ψ) / 2) = 0
mpr₅ : -2 * sin (π * (↑k : ℝ)) * sin ((θ - ψ) / 2) = 0
mpr₆ : -2 * sin ((↑k : ℝ) * π) * sin ((θ - ψ) / 2) = 0
mpr₇ : HMul.hMul (α := ℝ) (-2) 0 * sin ((θ - ψ) / 2) = 0
mpr₈ : 0 * sin ((θ - ψ) / 2) = 0
⊢ cos θ = cos ψ
have mpr₉ : Eq (α := ℝ) 0 0
Tactic: rw [← sub_eq_zero, cos_sub_cos, ← sub_neg_eq_add, H, mul_assoc 2 π k,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), mul_comm π _, sin_int_mul_pi, mul_zero,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ sin θ = sin ψ ↔ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have mp : sin θ = sin ψ → (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
mp : sin θ = sin ψ → (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ sin θ = sin ψ ↔ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have mpr : (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle) → sin θ = sin ψ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hsin : sin θ = sin ψ
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have Hsin₁ : cos (π / 2 - θ) = cos (π / 2 - ψ)
Tactic: rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin
Cleared hypotheses: Hsin
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have mp : ∀ (h : (↑(π / 2 - θ) : Angle) = (↑(π / 2 - ψ) : Angle)),
  (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
Tactic: rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
mp :
  ∀ (h : (↑(π / 2 - θ) : Angle) = (↑(π / 2 - ψ) : Angle)),
    (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have mp₁ : ∀ (h : (↑(π / 2 - θ) : Angle) = -(↑(π / 2 - ψ) : Angle)),
  (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
Tactic: rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = (↑(π / 2 - ψ) : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have mp : (↑θ : Angle) = (↑ψ : Angle)
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = (↑(π / 2 - ψ) : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have h₁ : (↑(π / 2) : Angle) - (↑θ : Angle) = (↑(π / 2) : Angle) - (↑ψ : Angle)
Tactic: rw [coe_sub, coe_sub] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = -(↑(π / 2 - ψ) : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have mp : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : (↑(π / 2 - θ) : Angle) = -(↑(π / 2 - ψ) : Angle)
⊢ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
have h₁ : (↑π : Angle) = (↑θ : Angle) + (↑ψ : Angle)
Tactic: rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add,
      add_halves, sub_sub, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ (↑θ : Angle) = (↑ψ : Angle) ∨ (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle) → sin θ = sin ψ
have mpr : ((∃ (k : ℤ), θ - ψ = 2 * π * (↑k : ℝ)) ∨ ∃ (k : ℤ), θ - (π - ψ) = 2 * π * (↑k : ℝ)) → sin θ = sin ψ
Tactic: rw [angle_eq_iff_two_pi_dvd_sub, ← eq_sub_iff_add_eq, ← coe_sub, angle_eq_iff_two_pi_dvd_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
⊢ sin θ = sin ψ
have mpr : sin θ - sin ψ = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
⊢ sin θ = sin ψ
have mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₃ : 2 * sin (2 * (π * (↑k : ℝ)) / 2) * cos ((θ + ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₃ : 2 * sin (2 * (π * (↑k : ℝ)) / 2) * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₄ : 2 * sin (π * (↑k : ℝ)) * cos ((θ + ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₃ : 2 * sin (2 * (π * (↑k : ℝ)) / 2) * cos ((θ + ψ) / 2) = 0
mpr₄ : 2 * sin (π * (↑k : ℝ)) * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₅ : 2 * sin ((↑k : ℝ) * π) * cos ((θ + ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₃ : 2 * sin (2 * (π * (↑k : ℝ)) / 2) * cos ((θ + ψ) / 2) = 0
mpr₄ : 2 * sin (π * (↑k : ℝ)) * cos ((θ + ψ) / 2) = 0
mpr₅ : 2 * sin ((↑k : ℝ) * π) * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₆ : HMul.hMul (α := ℝ) 2 0 * cos ((θ + ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₃ : 2 * sin (2 * (π * (↑k : ℝ)) / 2) * cos ((θ + ψ) / 2) = 0
mpr₄ : 2 * sin (π * (↑k : ℝ)) * cos ((θ + ψ) / 2) = 0
mpr₅ : 2 * sin ((↑k : ℝ) * π) * cos ((θ + ψ) / 2) = 0
mpr₆ : HMul.hMul (α := ℝ) 2 0 * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₇ : 0 * cos ((θ + ψ) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * (↑k : ℝ)
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin (2 * π * (↑k : ℝ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₃ : 2 * sin (2 * (π * (↑k : ℝ)) / 2) * cos ((θ + ψ) / 2) = 0
mpr₄ : 2 * sin (π * (↑k : ℝ)) * cos ((θ + ψ) / 2) = 0
mpr₅ : 2 * sin ((↑k : ℝ) * π) * cos ((θ + ψ) / 2) = 0
mpr₆ : HMul.hMul (α := ℝ) 2 0 * cos ((θ + ψ) / 2) = 0
mpr₇ : 0 * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₈ : Eq (α := ℝ) 0 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
have rwa : ∀ (H : θ - π + ψ = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
Tactic: rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
rwa : ∀ (H : θ - π + ψ = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
have rwa₁ : ∀ (H : θ + ψ - π = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
Tactic: rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
rwa : ∀ (H : θ - π + ψ = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₁ : ∀ (H : θ + ψ - π = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
have rwa₂ : ∀ (H : θ + ψ = 2 * π * (↑k : ℝ) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
Tactic: rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
rwa : ∀ (H : θ - π + ψ = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₁ : ∀ (H : θ + ψ - π = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₂ : ∀ (H : θ + ψ = 2 * π * (↑k : ℝ) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
have rwa₃ : ∀ (H : θ + ψ = 2 * (π * (↑k : ℝ)) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
Tactic: rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
rwa : ∀ (H : θ - π + ψ = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₁ : ∀ (H : θ + ψ - π = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₂ : ∀ (H : θ + ψ = 2 * π * (↑k : ℝ) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₃ : ∀ (H : θ + ψ = 2 * (π * (↑k : ℝ)) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
have rwa₄ : ∀ (H : θ + ψ = 2 * ((↑k : ℝ) * π) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
Tactic: rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
rwa : ∀ (H : θ - π + ψ = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₁ : ∀ (H : θ + ψ - π = 2 * π * (↑k : ℝ)), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₂ : ∀ (H : θ + ψ = 2 * π * (↑k : ℝ) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₃ : ∀ (H : θ + ψ = 2 * (π * (↑k : ℝ)) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
rwa₄ : ∀ (H : θ + ψ = 2 * ((↑k : ℝ) * π) + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
⊢ θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
have rwa₅ : ∀ (H : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π), θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
Tactic: rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
Cleared hypotheses: H