awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : θ = (↑(π / 2) : Angle) - ψ ∨ θ = (↑(π / 2) : Angle) - ψ + (↑π : Angle)
⊢ |θ.cos| = |ψ.sin|
have inl : |((↑(π / 2) : Angle) - ψ).cos| = |ψ.sin|
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : θ = (↑(π / 2) : Angle) - ψ ∨ θ = (↑(π / 2) : Angle) - ψ + (↑π : Angle)
inl : |((↑(π / 2) : Angle) - ψ).cos| = |ψ.sin|
⊢ |θ.cos| = |ψ.sin|
have inr : |((↑(π / 2) : Angle) - ψ + (↑π : Angle)).cos| = |ψ.sin|
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 θ + HSMul.hSMul (α := ℤ) 2 ψ = (↑π : Angle)
⊢ |θ.cos| = |ψ.sin|
have h₁ : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
Tactic: simp_rw [two_zsmul, ← two_nsmul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x : ℝ
⊢ (↑x : Angle).tan = Real.tan x
have rw : (↑x : Angle).sin / (↑x : Angle).cos = Real.tan x
Tactic: rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x : ℝ
rw : (↑x : Angle).sin / (↑x : Angle).cos = Real.tan x
⊢ (↑x : Angle).tan = Real.tan x
have rw₁ : Real.sin x / (↑x : Angle).cos = Real.tan x
Tactic: rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x : ℝ
rw : (↑x : Angle).sin / (↑x : Angle).cos = Real.tan x
rw₁ : Real.sin x / (↑x : Angle).cos = Real.tan x
⊢ (↑x : Angle).tan = Real.tan x
have rw₂ : Real.sin x / Real.cos x = Real.tan x
Tactic: rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x : ℝ
rw : (↑x : Angle).sin / (↑x : Angle).cos = Real.tan x
rw₁ : Real.sin x / (↑x : Angle).cos = Real.tan x
rw₂ : Real.sin x / Real.cos x = Real.tan x
⊢ (↑x : Angle).tan = Real.tan x
have rw₃ : Real.sin x / Real.cos x = Real.sin x / Real.cos x
Tactic: rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ tan 0 = 0
have rw : (↑0 : Angle).tan = 0
Tactic: rw [← coe_zero, tan_coe, Real.tan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑0 : Angle).tan = 0
⊢ tan 0 = 0
have rw₁ : Real.tan 0 = 0
Tactic: rw [← coe_zero, tan_coe, Real.tan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : (↑0 : Angle).tan = 0
rw₁ : Real.tan 0 = 0
⊢ tan 0 = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [← coe_zero, tan_coe, Real.tan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑π : Angle).tan = 0
have rw : Real.tan π = 0
Tactic: rw [tan_coe, Real.tan_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Real.tan π = 0
⊢ (↑π : Angle).tan = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [tan_coe, Real.tan_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ + (↑π : Angle)).tan = θ.tan
have h : ∀ (x : ℝ), ((↑x : Angle) + (↑π : Angle)).tan = (↑x : Angle).tan
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x : ℝ
⊢ ((↑x : Angle) + (↑π : Angle)).tan = (↑x : Angle).tan
have h : Real.tan (x + π) = Real.tan x
Tactic: rw [← coe_add, tan_coe, tan_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
| θ.tan
have rw : Real.tan θ.toReal
Tactic: rw [← coe_toReal θ, tan_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ Real.tan θ.toReal = θ.tan
have conv_rhs : Real.tan θ.toReal = θ.tan
Tactic: conv_rhs => rw [← coe_toReal θ, tan_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
conv_rhs : Real.tan θ.toReal = θ.tan
⊢ Real.tan θ.toReal = θ.tan
have conv_rhs₁ : Real.tan θ.toReal = Real.tan θ.toReal
Tactic: conv_rhs => rw [← coe_toReal θ, tan_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
⊢ θ.tan = ψ.tan
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)
⊢ θ.tan = ψ.tan
have inl : θ.tan = θ.tan
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 : θ.tan = θ.tan
⊢ θ.tan = ψ.tan
have inr : (ψ + (↑π : Angle)).tan = ψ.tan
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 θ = HSMul.hSMul (α := ℤ) 2 ψ
⊢ θ.tan = ψ.tan
have h₁ : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
Tactic: simp_rw [two_zsmul, ← two_nsmul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ ψ.tan = θ.tan⁻¹
have h₁ : ∀ (x : ℝ) (h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)),
  ψ.tan = (↑x : Angle).tan⁻¹
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ : Angle
x : ℝ
h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
⊢ ψ.tan = (↑x : Angle).tan⁻¹
have h₁ : ∀ (x_1 : ℝ) (h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 (↑x_1 : Angle) = (↑π : Angle)),
  (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
Tactic: induction ψ using Real.Angle.induction_on
Cleared hypotheses: ψ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
x x_1 : ℝ
h : HSMul.hSMul (α := ℕ) 2 (↑x : Angle) + HSMul.hSMul (α := ℕ) 2 (↑x_1 : Angle) = (↑π : Angle)
⊢ (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
have h₁ : ∃ (k : ℤ), 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)
Tactic: rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x x_1 : ℝ
h : ∃ (k : ℤ), 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)
⊢ (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
have h₁ : ∀ (k : ℤ) (h : 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)), (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
Tactic: rcases h with ⟨k, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
x x_1 : ℝ
k : ℤ
h : 2 * (x + x_1) - π = 2 * π * (↑k : ℝ)
⊢ (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
have h₁ : x_1 = (↑k : ℝ) * π + π / 2 - x
Tactic: rw [sub_eq_iff_eq_add, ← mul_inv_cancel_left₀ two_ne_zero π, mul_assoc, ← mul_add,
    mul_right_inj' (two_ne_zero' ℝ), ← eq_sub_iff_add_eq', mul_inv_cancel_left₀ two_ne_zero π,
    inv_mul_eq_div, mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x x_1 : ℝ
k : ℤ
h : x_1 = (↑k : ℝ) * π + π / 2 - x
⊢ (↑x_1 : Angle).tan = (↑x : Angle).tan⁻¹
have h₁ : Real.tan (π / 2 - x + (↑k : ℝ) * π) = Real.tan (π / 2 - x)
Tactic: rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 θ + HSMul.hSMul (α := ℤ) 2 ψ = (↑π : Angle)
⊢ ψ.tan = θ.tan⁻¹
have h₁ : HSMul.hSMul (α := ℕ) 2 θ + HSMul.hSMul (α := ℕ) 2 ψ = (↑π : Angle)
Tactic: simp_rw [two_zsmul, ← two_nsmul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ sign 0 = 0
have rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (sin 0) : SignType) (0 : SignType)
Tactic: rw [sign, sin_zero, _root_.sign_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (sin 0) : SignType) (0 : SignType)
⊢ sign 0 = 0
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 0 : SignType) (0 : SignType)
Tactic: rw [sign, sin_zero, _root_.sign_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (sin 0) : SignType) (0 : SignType)
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 0 : SignType) (0 : SignType)
⊢ sign 0 = 0
have rw₂ : Eq (α := SignType) 0 0
Tactic: rw [sign, sin_zero, _root_.sign_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑π : Angle).sign = 0
have rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑π : Angle).sin : SignType) (0 : SignType)
Tactic: rw [sign, sin_coe_pi, _root_.sign_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑π : Angle).sin : SignType) (0 : SignType)
⊢ (↑π : Angle).sign = 0
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 0 : SignType) (0 : SignType)
Tactic: rw [sign, sin_coe_pi, _root_.sign_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑π : Angle).sin : SignType) (0 : SignType)
rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) 0 : SignType) (0 : SignType)
⊢ (↑π : Angle).sign = 0
have rw₂ : Eq (α := SignType) 0 0
Tactic: rw [sign, sin_coe_pi, _root_.sign_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (-θ).sign = -θ.sign
have simp_rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ).sin : SignType)
  (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
Tactic: simp_rw [sign, sin_neg, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
simp_rw :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ).sin : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
⊢ (-θ).sign = -θ.sign
have simp_rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ.sin) : SignType)
  (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
Tactic: simp_rw [sign, sin_neg, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (θ + (↑π : Angle)).sign = -θ.sign
have rw : (SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin = -θ.sign
Tactic: rw [sign, sign, sin_add_pi, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin = -θ.sign
⊢ (θ + (↑π : Angle)).sign = -θ.sign
have rw₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin : SignType)
  (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
Tactic: rw [sign, sign, sin_add_pi, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin = -θ.sign
rw₁ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
⊢ (θ + (↑π : Angle)).sign = -θ.sign
have rw₂ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ.sin) : SignType)
  (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
Tactic: rw [sign, sign, sin_add_pi, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin = -θ.sign
rw₁ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (θ + (↑π : Angle)).sin : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
rw₂ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (-θ.sin) : SignType)
    (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
⊢ (θ + (↑π : Angle)).sign = -θ.sign
have rw₃ : Eq (α := SignType) (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
  (-(SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
Tactic: rw [sign, sign, sin_add_pi, Left.sign_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ ((↑π : Angle) + θ).sign = -θ.sign
have rw : (θ + (↑π : Angle)).sign = -θ.sign
Tactic: rw [add_comm, sign_add_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : (θ + (↑π : Angle)).sign = -θ.sign
⊢ ((↑π : Angle) + θ).sign = -θ.sign
have rw₁ : -θ.sign = -θ.sign
Tactic: rw [add_comm, sign_add_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.sign = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType) (0 : SignType) ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [sign, _root_.sign_eq_zero_iff, sin_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType) (0 : SignType) ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ.sign = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw₁ : θ.sin = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [sign, _root_.sign_eq_zero_iff, sin_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType) (0 : SignType) ↔ θ = 0 ∨ θ = (↑π : Angle)
rw₁ : θ.sin = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
⊢ θ.sign = 0 ↔ θ = 0 ∨ θ = (↑π : Angle)
have rw₂ : θ = 0 ∨ θ = (↑π : Angle) ↔ θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [sign, _root_.sign_eq_zero_iff, sin_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw : θ.sign ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
Tactic: rw [← not_or, ← sign_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.sign ≠ 0 ↔ ¬(θ = 0 ∨ θ = (↑π : Angle))
⊢ θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ (↑π : Angle)
have rw₁ : θ.sign ≠ 0 ↔ ¬θ.sign = 0
Tactic: rw [← not_or, ← sign_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.toReal < 0 ↔ θ.sign = -1
have rw : θ.toReal < 0 ↔ Real.sin θ.toReal < 0
Tactic: rw [sign, ← sin_toReal, sign_eq_neg_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ 0 ≤ θ.toReal ↔ 0 ≤ θ.sign
have simp : 0 ≤ θ.toReal ↔ 0 ≤ Real.sin θ.toReal
Tactic: simp only [sign, ← sin_toReal, sign_nonneg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
have inl : ∀ (ht : θ.toReal < 0), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
Tactic: rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
inl : ∀ (ht : θ.toReal < 0), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
have inr : ∀ (ht : θ.toReal = 0), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
Tactic: rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
inl : ∀ (ht : θ.toReal < 0), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
inr : ∀ (ht : θ.toReal = 0), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
have inr₁ : ∀ (ht : 0 < θ.toReal), (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
Tactic: rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
ht : 0 < θ.toReal
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
have inr : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
  ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
Tactic: rw [sign, ← sin_toReal, sign_pos ht,
      sign_pos
        (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
ht : 0 < θ.toReal
inr :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
    ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
have inr₁ : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
  ((SignType.sign : (a : ℝ) → SignType) (Real.sin θ.toReal) : SignType)
Tactic: rw [sign, ← sin_toReal, sign_pos ht,
      sign_pos
        (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
ht : 0 < θ.toReal
inr :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
    ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
inr₁ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (Real.sin θ.toReal) : SignType)
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
have inr₂ : Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin θ.toReal) : SignType)
Tactic: rw [sign, ← sin_toReal, sign_pos ht,
      sign_pos
        (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
ht : 0 < θ.toReal
inr :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
    ((SignType.sign : (a : ℝ) → SignType) θ.sin : SignType)
inr₁ :
  Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) θ.toReal : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (Real.sin θ.toReal) : SignType)
inr₂ : Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : ℝ) → SignType) (Real.sin θ.toReal) : SignType)
⊢ (SignType.sign : (a : ℝ) → SignType) θ.toReal = θ.sign
have inr₃ : Eq (α := SignType) 1 1
Tactic: rw [sign, ← sin_toReal, sign_pos ht,
      sign_pos
        (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1
have inl : (↑π : Angle).toReal ∈ Set.Ioo 0 π ↔ (↑π : Angle).sign = 1
Tactic: rcases eq_or_ne θ π with rfl | h
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
inl : (↑π : Angle).toReal ∈ Set.Ioo 0 π ↔ (↑π : Angle).sign = 1
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1
have inr : ∀ (h : θ ≠ (↑π : Angle)), θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1
Tactic: rcases eq_or_ne θ π with rfl | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1
have inr : 0 < θ.toReal → θ.toReal < π
Tactic: simp only [Set.mem_Ioo, ← sign_toReal h, sign_eq_one_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : 0 ≤ θ.sign
⊢ (↑|θ.toReal| : Angle) = θ
have rw : (↑θ.toReal : Angle) = θ
Tactic: rw [abs_eq_self.2 (toReal_nonneg_iff_sign_nonneg.2 h), coe_toReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : 0 ≤ θ.sign
rw : (↑θ.toReal : Angle) = θ
⊢ (↑|θ.toReal| : Angle) = θ
have rw₁ : θ = θ
Tactic: rw [abs_eq_self.2 (toReal_nonneg_iff_sign_nonneg.2 h), coe_toReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ : Angle
h : θ.sign ≤ 0
⊢ -(↑|θ.toReal| : Angle) = θ
have h₁ : θ.sign = -1 ∨ θ.sign = 0
Tactic: rw [SignType.nonpos_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
⊢ -(↑|θ.toReal| : Angle) = θ
have inl : ∀ (h : θ.sign = -1), -(↑|θ.toReal| : Angle) = θ
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
inl : ∀ (h : θ.sign = -1), -(↑|θ.toReal| : Angle) = θ
⊢ -(↑|θ.toReal| : Angle) = θ
have inr : ∀ (h : θ.sign = 0), -(↑|θ.toReal| : Angle) = θ
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.sign = -1
⊢ -(↑|θ.toReal| : Angle) = θ
have inl : -(↑(-θ.toReal) : Angle) = θ
Tactic: rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.sign = -1
inl : -(↑(-θ.toReal) : Angle) = θ
⊢ -(↑|θ.toReal| : Angle) = θ
have inl₁ : - -(↑θ.toReal : Angle) = θ
Tactic: rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.sign = -1
inl : -(↑(-θ.toReal) : Angle) = θ
inl₁ : - -(↑θ.toReal : Angle) = θ
⊢ -(↑|θ.toReal| : Angle) = θ
have inl₂ : (↑θ.toReal : Angle) = θ
Tactic: rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ.sign = -1
inl : -(↑(-θ.toReal) : Angle) = θ
inl₁ : - -(↑θ.toReal : Angle) = θ
inl₂ : (↑θ.toReal : Angle) = θ
⊢ -(↑|θ.toReal| : Angle) = θ
have inl₃ : θ = θ
Tactic: rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ : Angle
h : θ.sign = 0
⊢ -(↑|θ.toReal| : Angle) = θ
have h₁ : θ = 0 ∨ θ = (↑π : Angle)
Tactic: rw [sign_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ = 0 ∨ θ = (↑π : Angle)
⊢ -(↑|θ.toReal| : Angle) = θ
have inr : -(↑|toReal 0| : Angle) = 0
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ = 0 ∨ θ = (↑π : Angle)
inr : -(↑|toReal 0| : Angle) = 0
⊢ -(↑|θ.toReal| : Angle) = θ
have inr₁ : -(↑|(↑π : Angle).toReal| : Angle) = (↑π : Angle)
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑(π / 2) : Angle).sign = 1
have rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (↑(π / 2) : Angle).sin : SignType) (1 : SignType)
Tactic: rw [sign, sin_coe, sin_pi_div_two, sign_one]