awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
⊢ sin θ = sin ψ
have H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
Tactic: have H' : θ + ψ = 2 * k * π + π := by
      rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
⊢ sin θ = sin ψ
have mpr : sin θ - sin ψ = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 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', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
⊢ sin θ = sin ψ
have mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
⊢ sin θ = sin ψ
have mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
⊢ sin θ = sin ψ
have mpr₄ : 2 * sin ((θ - ψ) / 2) * cos (2 * ((↑k : ℝ) * π) / 2 + π / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
mpr₄ : 2 * sin ((θ - ψ) / 2) * cos (2 * ((↑k : ℝ) * π) / 2 + π / 2) = 0
⊢ sin θ = sin ψ
have mpr₅ : 2 * sin ((θ - ψ) / 2) * cos ((↑k : ℝ) * π + π / 2) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
mpr₄ : 2 * sin ((θ - ψ) / 2) * cos (2 * ((↑k : ℝ) * π) / 2 + π / 2) = 0
mpr₅ : 2 * sin ((θ - ψ) / 2) * cos ((↑k : ℝ) * π + π / 2) = 0
⊢ sin θ = sin ψ
have mpr₆ : 2 * sin ((θ - ψ) / 2) * -sin ((↑k : ℝ) * π) = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
mpr₄ : 2 * sin ((θ - ψ) / 2) * cos (2 * ((↑k : ℝ) * π) / 2 + π / 2) = 0
mpr₅ : 2 * sin ((θ - ψ) / 2) * cos ((↑k : ℝ) * π + π / 2) = 0
mpr₆ : 2 * sin ((θ - ψ) / 2) * -sin ((↑k : ℝ) * π) = 0
⊢ sin θ = sin ψ
have mpr₇ : 2 * sin ((θ - ψ) / 2) * -0 = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
mpr₄ : 2 * sin ((θ - ψ) / 2) * cos (2 * ((↑k : ℝ) * π) / 2 + π / 2) = 0
mpr₅ : 2 * sin ((θ - ψ) / 2) * cos ((↑k : ℝ) * π + π / 2) = 0
mpr₆ : 2 * sin ((θ - ψ) / 2) * -sin ((↑k : ℝ) * π) = 0
mpr₇ : 2 * sin ((θ - ψ) / 2) * -0 = 0
⊢ sin θ = sin ψ
have mpr₈ : 2 * sin ((θ - ψ) / 2) * 0 = 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * (↑k : ℝ)
H' : θ + ψ = HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π
mpr : sin θ - sin ψ = 0
mpr₁ : 2 * sin ((θ - ψ) / 2) * cos ((θ + ψ) / 2) = 0
mpr₂ : 2 * sin ((θ - ψ) / 2) * cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π + π) / 2) = 0
mpr₃ : 2 * sin ((θ - ψ) / 2) * cos (HMul.hMul (α := ℝ) 2 (↑k : ℝ) * π / 2 + π / 2) = 0
mpr₄ : 2 * sin ((θ - ψ) / 2) * cos (2 * ((↑k : ℝ) * π) / 2 + π / 2) = 0
mpr₅ : 2 * sin ((θ - ψ) / 2) * cos ((↑k : ℝ) * π + π / 2) = 0
mpr₆ : 2 * sin ((θ - ψ) / 2) * -sin ((↑k : ℝ) * π) = 0
mpr₇ : 2 * sin ((θ - ψ) / 2) * -0 = 0
mpr₈ : 2 * sin ((θ - ψ) / 2) * 0 = 0
⊢ sin θ = sin ψ
have mpr₉ : Eq (α := ℝ) 0 0
Tactic: rw [← sub_eq_zero, sin_sub_sin, H', add_div, mul_assoc 2 _ π,
      mul_div_cancel_left₀ _ (two_ne_zero' ℝ), cos_add_pi_div_two, sin_int_mul_pi, neg_zero,
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
⊢ (↑θ : Angle) = (↑ψ : Angle)
have inl : ∀ (hc : (↑θ : Angle) = (↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
Tactic: rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hcos with hc | hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
inl : ∀ (hc : (↑θ : Angle) = (↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have inr : ∀ (hc : (↑θ : Angle) = -(↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
Tactic: rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hcos with hc | hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have inr : ∀ (hs : (↑θ : Angle) = (↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
Tactic: rcases sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
inr : ∀ (hs : (↑θ : Angle) = (↑ψ : Angle)), (↑θ : Angle) = (↑ψ : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have inr₁ : ∀ (hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)), (↑θ : Angle) = (↑ψ : Angle)
Tactic: rcases sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑θ : Angle) = -(↑ψ : Angle)
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have hc₁ : (↑π : Angle) = 0
Tactic: rw [eq_neg_iff_add_eq_zero, hs] at hc
Cleared hypotheses: hc, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
⊢ (↑θ : Angle) = (↑ψ : Angle)
have inr : ∀ (n : ℤ) (hn : n • (2 * π) = -π + 0), (↑θ : Angle) = (↑ψ : Angle)
Tactic: obtain ⟨n, hn⟩ : ∃ n, n • _ = _ := QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n • (2 * π) = -π + 0
⊢ (↑θ : Angle) = (↑ψ : Angle)
have hn₁ : n * 2 + 1 = 0
Tactic: rw [← neg_one_mul, add_zero, ← sub_eq_zero, zsmul_eq_mul, ← mul_assoc, ← sub_mul, mul_eq_zero,
    eq_false (ne_of_gt pi_pos), or_false, sub_neg_eq_add, ← Int.cast_zero, ← Int.cast_one,
    ← Int.cast_ofNat, ← Int.cast_mul, ← Int.cast_add, Int.cast_inj] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n * 2 + 1 = 0
⊢ (↑θ : Angle) = (↑ψ : Angle)
have this : (n * 2 + 1) % 2 = HMod.hMod (α := ℤ) 0 2
Tactic: have : (n * 2 + 1) % (2 : ℤ) = 0 % (2 : ℤ) := congr_arg (· % (2 : ℤ)) hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : (↑π : Angle) = 0
hs : (↑θ : Angle) + (↑ψ : Angle) = (↑π : Angle)
n : ℤ
hn : n * 2 + 1 = 0
this : (n * 2 + 1) % 2 = HMod.hMod (α := ℤ) 0 2
⊢ (↑θ : Angle) = (↑ψ : Angle)
have this₁ : HMod.hMod (α := ℤ) 1 2 = HMod.hMod (α := ℤ) 0 2
Tactic: rw [add_comm, Int.add_mul_emod_self_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
ψ : ℝ
⊢ θ.cos = Real.cos ψ ↔ θ = (↑ψ : Angle) ∨ θ = -(↑ψ : Angle)
have h : ∀ (x : ℝ), (↑x : Angle).cos = Real.cos ψ ↔ (↑x : Angle) = (↑ψ : Angle) ∨ (↑x : Angle) = -(↑ψ : Angle)
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
⊢ θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ
have h : ∀ (x : ℝ), θ.cos = (↑x : Angle).cos ↔ θ = (↑x : Angle) ∨ θ = -(↑x : Angle)
Tactic: induction ψ using Real.Angle.induction_on
Cleared hypotheses: ψ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
ψ : ℝ
⊢ θ.sin = Real.sin ψ ↔ θ = (↑ψ : Angle) ∨ θ + (↑ψ : Angle) = (↑π : Angle)
have h : ∀ (x : ℝ), (↑x : Angle).sin = Real.sin ψ ↔ (↑x : Angle) = (↑ψ : Angle) ∨ (↑x : Angle) + (↑ψ : Angle) = (↑π : Angle)
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
⊢ θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = (↑π : Angle)
have h : ∀ (x : ℝ), θ.sin = (↑x : Angle).sin ↔ θ = (↑x : Angle) ∨ θ + (↑x : Angle) = (↑π : Angle)
Tactic: induction ψ using Real.Angle.induction_on
Cleared hypotheses: ψ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ sin 0 = 0
have rw : (↑0 : Angle).sin = 0
Tactic: rw [← coe_zero, sin_coe, Real.sin_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑0 : Angle).sin = 0
⊢ sin 0 = 0
have rw₁ : Real.sin 0 = 0
Tactic: rw [← coe_zero, sin_coe, Real.sin_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑0 : Angle).sin = 0
rw₁ : Real.sin 0 = 0
⊢ sin 0 = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [← coe_zero, sin_coe, Real.sin_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑π : Angle).sin = 0
have rw : Real.sin π = 0
Tactic: rw [sin_coe, Real.sin_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Real.sin π = 0
⊢ (↑π : Angle).sin = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [sin_coe, Real.sin_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.sin = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have nth_rw : θ.sin = sin 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: nth_rw 1 [← sin_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw : θ = 0 ∨ θ + 0 = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [sin_eq_iff_eq_or_add_eq_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw : θ.sin ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
Tactic: rw [← not_or, ← sin_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.sin ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
⊢ θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw₁ : θ.sin ≠ 0 ↔ ¬θ.sin = 0
Tactic: rw [← not_or, ← sin_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (-θ).sin = -θ.sin
have h : ∀ (x : ℝ), (-(↑x : Angle)).sin = -(↑x : Angle).sin
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ + (↑π : Angle)).sin = -θ.sin
have h : ∀ (x : ℝ), ((↑x : Angle) + (↑π : Angle)).sin = -(↑x : Angle).sin
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ cos 0 = 1
have rw : (↑0 : Angle).cos = 1
Tactic: rw [← coe_zero, cos_coe, Real.cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑0 : Angle).cos = 1
⊢ cos 0 = 1
have rw₁ : Real.cos 0 = 1
Tactic: rw [← coe_zero, cos_coe, Real.cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑0 : Angle).cos = 1
rw₁ : Real.cos 0 = 1
⊢ cos 0 = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [← coe_zero, cos_coe, Real.cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑π : Angle).cos = -1
have rw : Real.cos π = -1
Tactic: rw [cos_coe, Real.cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Real.cos π = -1
⊢ (↑π : Angle).cos = -1
have rw₁ : Eq (α := ℝ) (-1) (-1)
Tactic: rw [cos_coe, Real.cos_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (-θ).cos = θ.cos
have h : ∀ (x : ℝ), (-(↑x : Angle)).cos = (↑x : Angle).cos
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ + (↑π : Angle)).cos = -θ.cos
have h : ∀ (x : ℝ), ((↑x : Angle) + (↑π : Angle)).cos = -(↑x : Angle).cos
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.cos = 0 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw : θ.cos = Real.cos (π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.cos = Real.cos (π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ θ.cos = 0 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₁ : θ.cos = (↑(π / 2) : Angle).cos ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.cos = Real.cos (π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : θ.cos = (↑(π / 2) : Angle).cos ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ θ.cos = 0 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₂ : θ = (↑(π / 2) : Angle) ∨ θ = -(↑(π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.cos = Real.cos (π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : θ.cos = (↑(π / 2) : Angle).cos ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₂ : θ = (↑(π / 2) : Angle) ∨ θ = -(↑(π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ θ.cos = 0 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₃ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-(π / 2)) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.cos = Real.cos (π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : θ.cos = (↑(π / 2) : Angle).cos ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₂ : θ = (↑(π / 2) : Angle) ∨ θ = -(↑(π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₃ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-(π / 2)) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ θ.cos = 0 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₄ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
have h : ∀ (x : ℝ), ((↑x : Angle) + θ₂).sin = (↑x : Angle).sin * θ₂.cos + (↑x : Angle).cos * θ₂.sin
Tactic: induction θ₁ using Real.Angle.induction_on
Cleared hypotheses: θ₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ₂ : Angle
x : ℝ
⊢ ((↑x : Angle) + θ₂).sin = (↑x : Angle).sin * θ₂.cos + (↑x : Angle).cos * θ₂.sin
have h : ∀ (x_1 : ℝ),
  ((↑x : Angle) + (↑x_1 : Angle)).sin = (↑x : Angle).sin * (↑x_1 : Angle).cos + (↑x : Angle).cos * (↑x_1 : Angle).sin
Tactic: induction θ₂ using Real.Angle.induction_on
Cleared hypotheses: θ₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
have h : ∀ (x : ℝ), (θ₁ + (↑x : Angle)).cos = θ₁.cos * (↑x : Angle).cos - θ₁.sin * (↑x : Angle).sin
Tactic: induction θ₂ using Real.Angle.induction_on
Cleared hypotheses: θ₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ₁ : Angle
x : ℝ
⊢ (θ₁ + (↑x : Angle)).cos = θ₁.cos * (↑x : Angle).cos - θ₁.sin * (↑x : Angle).sin
have h : ∀ (x_1 : ℝ),
  ((↑x_1 : Angle) + (↑x : Angle)).cos = (↑x_1 : Angle).cos * (↑x : Angle).cos - (↑x_1 : Angle).sin * (↑x : Angle).sin
Tactic: induction θ₁ using Real.Angle.induction_on
Cleared hypotheses: θ₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ HPow.hPow (β := ℕ) θ.cos 2 + HPow.hPow (β := ℕ) θ.sin 2 = 1
have h : ∀ (x : ℝ), HPow.hPow (β := ℕ) (↑x : Angle).cos 2 + HPow.hPow (β := ℕ) (↑x : Angle).sin 2 = 1
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ + (↑(π / 2) : Angle)).sin = θ.cos
have h : ∀ (x : ℝ), ((↑x : Angle) + (↑(π / 2) : Angle)).sin = (↑x : Angle).cos
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ - (↑(π / 2) : Angle)).sin = -θ.cos
have h : ∀ (x : ℝ), ((↑x : Angle) - (↑(π / 2) : Angle)).sin = -(↑x : Angle).cos
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ ((↑(π / 2) : Angle) - θ).sin = θ.cos
have h : ∀ (x : ℝ), ((↑(π / 2) : Angle) - (↑x : Angle)).sin = (↑x : Angle).cos
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ + (↑(π / 2) : Angle)).cos = -θ.sin
have h : ∀ (x : ℝ), ((↑x : Angle) + (↑(π / 2) : Angle)).cos = -(↑x : Angle).sin
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ - (↑(π / 2) : Angle)).cos = θ.sin
have h : ∀ (x : ℝ), ((↑x : Angle) - (↑(π / 2) : Angle)).cos = (↑x : Angle).sin
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ ((↑(π / 2) : Angle) - θ).cos = θ.sin
have h : ∀ (x : ℝ), ((↑(π / 2) : Angle) - (↑x : Angle)).cos = (↑x : Angle).sin
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
⊢ |θ.sin| = |ψ.sin|
have h₁ : θ = ψ ∨ θ = ψ + (↑π : Angle)
Tactic: rw [two_nsmul_eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + (↑π : Angle)
⊢ |θ.sin| = |ψ.sin|
have inl : |θ.sin| = |θ.sin|
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: ψ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + (↑π : Angle)
inl : |θ.sin| = |θ.sin|
⊢ |θ.sin| = |ψ.sin|
have inr : |(ψ + (↑π : Angle)).sin| = |ψ.sin|
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ : Angle
⊢ |(ψ + (↑π : Angle)).sin| = |ψ.sin|
have inr : |(-ψ.sin)| = |ψ.sin|
Tactic: rw [sin_add_pi, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ : Angle
inr : |(-ψ.sin)| = |ψ.sin|
⊢ |(ψ + (↑π : Angle)).sin| = |ψ.sin|
have inr₁ : |ψ.sin| = |ψ.sin|
Tactic: rw [sin_add_pi, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 θ = HSMul.hSMul (α := ℤ) 2 ψ
⊢ |θ.sin| = |ψ.sin|
have h₁ : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
Tactic: simp_rw [two_zsmul, ← two_nsmul] at h
Cleared hypotheses: h