awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℕ) 2 θ = HSMul.hSMul (α := ℕ) 2 ψ
⊢ |θ.cos| = |ψ.cos|
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)
⊢ |θ.cos| = |ψ.cos|
have inl : |θ.cos| = |θ.cos|
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 : |θ.cos| = |θ.cos|
⊢ |θ.cos| = |ψ.cos|
have inr : |(ψ + (↑π : Angle)).cos| = |ψ.cos|
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: θ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ : Angle
⊢ |(ψ + (↑π : Angle)).cos| = |ψ.cos|
have inr : |(-ψ.cos)| = |ψ.cos|
Tactic: rw [cos_add_pi, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
ψ : Angle
inr : |(-ψ.cos)| = |ψ.cos|
⊢ |(ψ + (↑π : Angle)).cos| = |ψ.cos|
have inr₁ : |ψ.cos| = |ψ.cos|
Tactic: rw [cos_add_pi, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ ψ : Angle
h : HSMul.hSMul (α := ℤ) 2 θ = HSMul.hSMul (α := ℤ) 2 ψ
⊢ |θ.cos| = |ψ.cos|
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:
θ ψ : ℝ
⊢ (↑(toIcoMod two_pi_pos ψ θ) : Angle) = (↑θ : Angle)
have rw : ∃ (k : ℤ), toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)
Tactic: rw [angle_eq_iff_two_pi_dvd_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ ∃ (k : ℤ), toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)
have refine : toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
Tactic: refine ⟨-toIcoDiv two_pi_pos ψ θ, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
have rw : -toIcoDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
Tactic: rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
rw : -toIcoDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
have rw₁ : (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ) * (2 * π) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
Tactic: rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
rw : -toIcoDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
rw₁ : (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ) * (2 * π) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
have rw₂ : 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ) = 2 * π * (↑(-toIcoDiv two_pi_pos ψ θ) : ℝ)
Tactic: rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ (↑(toIocMod two_pi_pos ψ θ) : Angle) = (↑θ : Angle)
have rw : ∃ (k : ℤ), toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)
Tactic: rw [angle_eq_iff_two_pi_dvd_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ ∃ (k : ℤ), toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑k : ℝ)
have refine : toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
Tactic: refine ⟨-toIocDiv two_pi_pos ψ θ, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
have rw : -toIocDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
Tactic: rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
rw : -toIocDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
have rw₁ : (↑(-toIocDiv two_pi_pos ψ θ) : ℝ) * (2 * π) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
Tactic: rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : ℝ
rw : -toIocDiv two_pi_pos ψ θ • (2 * π) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
rw₁ : (↑(-toIocDiv two_pi_pos ψ θ) : ℝ) * (2 * π) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
have rw₂ : 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ) = 2 * π * (↑(-toIocDiv two_pi_pos ψ θ) : ℝ)
Tactic: rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ (↑θ : Angle).toReal = θ ↔ -π < θ ∧ θ ≤ π
have rw : θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
Tactic: rw [toReal_coe, toIocMod_eq_self two_pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
have ring_nf : θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ (↑θ : Angle).toReal = θ ↔ θ ∈ Set.Ioc (-π) π
have rw : -π < θ ∧ θ ≤ π ↔ θ ∈ Set.Ioc (-π) π
Tactic: rw [toReal_coe_eq_self_iff, ← Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
rw : -π < θ ∧ θ ≤ π ↔ θ ∈ Set.Ioc (-π) π
⊢ (↑θ : Angle).toReal = θ ↔ θ ∈ Set.Ioc (-π) π
have rw₁ : θ ∈ Set.Ioc (-π) π ↔ θ ∈ Set.Ioc (-π) π
Tactic: rw [toReal_coe_eq_self_iff, ← Set.mem_Ioc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ ψ : Angle
h : θ.toReal = ψ.toReal
⊢ θ = ψ
have h₁ : ∀ (x : ℝ) (h : (↑x : Angle).toReal = ψ.toReal), (↑x : Angle) = ψ
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 : (↑x : Angle).toReal = ψ.toReal
⊢ (↑x : Angle) = ψ
have h₁ : ∀ (x_1 : ℝ) (h : (↑x : Angle).toReal = (↑x_1 : Angle).toReal), (↑x : Angle) = (↑x_1 : Angle)
Tactic: induction ψ using Real.Angle.induction_on
Cleared hypotheses: ψ, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (↑θ.toReal : Angle) = θ
have h : ∀ (x : ℝ), (↑(↑x : Angle).toReal : 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
⊢ -π < θ.toReal
have h : ∀ (x : ℝ), -π < (↑x : Angle).toReal
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.toReal ≤ π
have h : ∀ (x : ℝ), (↑x : Angle).toReal ≤ π
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
x : ℝ
⊢ (↑x : Angle).toReal ≤ π
have h : π = -π + 2 * π
Tactic: convert! toIocMod_le_right two_pi_pos _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ toIocMod two_pi_pos (-π) θ.toReal = θ.toReal
have h : ∀ (x : ℝ), toIocMod two_pi_pos (-π) (↑x : Angle).toReal = (↑x : Angle).toReal
Tactic: induction θ using Real.Angle.induction_on
Cleared hypotheses: θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ toReal 0 = 0
have rw : -π < 0 ∧ 0 ≤ π
Tactic: rw [← coe_zero, toReal_coe_eq_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.toReal = 0 ↔ θ = 0
have nth_rw : θ.toReal = toReal 0 ↔ θ = 0
Tactic: nth_rw 1 [← toReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑π : Angle).toReal = π
have rw : -π < π ∧ π ≤ π
Tactic: rw [toReal_coe_eq_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.toReal = π ↔ θ = (↑π : Angle)
have rw : θ.toReal = π ↔ θ.toReal = (↑π : Angle).toReal
Tactic: rw [← toReal_inj, toReal_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.toReal = π ↔ θ.toReal = (↑π : Angle).toReal
⊢ θ.toReal = π ↔ θ = (↑π : Angle)
have rw₁ : θ.toReal = π ↔ θ.toReal = π
Tactic: rw [← toReal_inj, toReal_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ (-θ).toReal = -θ.toReal ↔ θ ≠ (↑π : Angle)
have nth_rw : -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ (↑π : Angle)
Tactic: nth_rw 1 [← coe_toReal θ, ← coe_neg, toReal_coe_eq_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ (↑π : Angle)
have mp : -π < -θ.toReal ∧ -θ.toReal ≤ π → θ ≠ (↑π : Angle)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
mp : -π < -θ.toReal ∧ -θ.toReal ≤ π → θ ≠ (↑π : Angle)
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ (↑π : Angle)
have mpr : θ ≠ (↑π : Angle) → -π < -θ.toReal ∧ -θ.toReal ≤ π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π
have mpr : θ.toReal < π ∧ -θ.toReal ≤ π
Tactic: rw [neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
⊢ θ.toReal < π ∧ -θ.toReal ≤ π
have h' : θ.toReal ≠ π
Tactic: have h' : θ.toReal ≠ π := by simp [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
h : θ ≠ (↑π : Angle)
h' : θ.toReal ≠ π
⊢ -θ.toReal ≤ π
have linarith : π < -θ.toReal → π - -θ.toReal + (-π - θ.toReal) = 0
Tactic: linarith [neg_pi_lt_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ |(-θ).toReal| = |θ.toReal|
have inl : |(-(↑π : Angle)).toReal| = |(↑π : Angle).toReal|
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| = |(↑π : Angle).toReal|
⊢ |(-θ).toReal| = |θ.toReal|
have inr : ∀ (h : θ ≠ (↑π : Angle)), |(-θ).toReal| = |θ.toReal|
Tactic: rcases eq_or_ne θ π with rfl | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑π : Angle) ≠ 0
have rw : π ≠ 0
Tactic: rw [← toReal_injective.ne_iff, toReal_pi, toReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ -π < π / 2 ∧ π / 2 ≤ π
have left : -π < π / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
left : -π < π / 2
⊢ -π < π / 2 ∧ π / 2 ≤ π
have right : π / 2 ≤ π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ -π < π / 2
have linarith : π / 2 ≤ -π → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π / 2 ≤ -π → 2 / 2 = 1
⊢ -π < π / 2
have linarith₁ : π / 2 ≤ -π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π / 2 ≤ -π → 2 / 2 = 1
linarith₁ : π / 2 ≤ -π → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -π < π / 2
have linarith₂ : π / 2 ≤ -π → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π / 2 ≤ -π → 2 / 2 = 1
linarith₁ : π / 2 ≤ -π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ -π → GT.gt (α := ℝ) 2 0
⊢ -π < π / 2
have linarith₃ : π / 2 ≤ -π → 1 * π - -(2 * π) + 3 * (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π / 2 ≤ -π → 2 / 2 = 1
linarith₁ : π / 2 ≤ -π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ -π → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 ≤ -π → 1 * π - -(2 * π) + 3 * (0 - π) = 0
⊢ -π < π / 2
have linarith₄ : π / 2 ≤ -π → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ π / 2 ≤ π
have linarith : π < π / 2 → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π < π / 2 → 2 / 2 = 1
⊢ π / 2 ≤ π
have linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 ≤ π
have linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π < π / 2 → 2 / 2 = 1
linarith₁ : π < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 → GT.gt (α := ℝ) 2 0
⊢ π / 2 ≤ π
have linarith₃ : π < π / 2 → 2 * π - 1 * π + (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.toReal = π / 2 ↔ θ = (↑(π / 2) : Angle)
have rw : θ.toReal = π / 2 ↔ θ.toReal = (↑(π / 2) : Angle).toReal
Tactic: rw [← toReal_inj, toReal_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.toReal = π / 2 ↔ θ.toReal = (↑(π / 2) : Angle).toReal
⊢ θ.toReal = π / 2 ↔ θ = (↑(π / 2) : Angle)
have rw₁ : θ.toReal = π / 2 ↔ θ.toReal = π / 2
Tactic: rw [← toReal_inj, toReal_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ -π < -π / 2 ∧ -π / 2 ≤ π
have left : -π < -π / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
left : -π < -π / 2
⊢ -π < -π / 2 ∧ -π / 2 ≤ π
have right : -π / 2 ≤ π
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ -π < -π / 2
have linarith : -π / 2 ≤ -π → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : -π / 2 ≤ -π → 2 / 2 = 1
⊢ -π < -π / 2
have linarith₁ : -π / 2 ≤ -π → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : -π / 2 ≤ -π → 2 / 2 = 1
linarith₁ : -π / 2 ≤ -π → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -π < -π / 2
have linarith₂ : -π / 2 ≤ -π → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : -π / 2 ≤ -π → 2 / 2 = 1
linarith₁ : -π / 2 ≤ -π → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : -π / 2 ≤ -π → GT.gt (α := ℝ) 2 0
⊢ -π < -π / 2
have linarith₃ : -π / 2 ≤ -π → -(1 * π) - -(2 * π) + (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ -π / 2 ≤ π
have linarith : π < -π / 2 → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π < -π / 2 → 2 / 2 = 1
⊢ -π / 2 ≤ π
have linarith₁ : π < -π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π < -π / 2 → 2 / 2 = 1
linarith₁ : π < -π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -π / 2 ≤ π
have linarith₂ : π < -π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π < -π / 2 → 2 / 2 = 1
linarith₁ : π < -π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < -π / 2 → GT.gt (α := ℝ) 2 0
⊢ -π / 2 ≤ π
have linarith₃ : π < -π / 2 → 2 * π - -(1 * π) + 3 * (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
linarith : π < -π / 2 → 2 / 2 = 1
linarith₁ : π < -π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < -π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < -π / 2 → 2 * π - -(1 * π) + 3 * (0 - π) = 0
⊢ -π / 2 ≤ π
have linarith₄ : π < -π / 2 → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ θ.toReal = -π / 2 ↔ θ = (↑(-π / 2) : Angle)
have rw : θ.toReal = -π / 2 ↔ θ.toReal = (↑(-π / 2) : Angle).toReal
Tactic: rw [← toReal_inj, toReal_neg_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.toReal = -π / 2 ↔ θ.toReal = (↑(-π / 2) : Angle).toReal
⊢ θ.toReal = -π / 2 ↔ θ = (↑(-π / 2) : Angle)
have rw₁ : θ.toReal = -π / 2 ↔ θ.toReal = -π / 2
Tactic: rw [← toReal_inj, toReal_neg_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑(π / 2) : Angle) ≠ 0
have rw : π / 2 ≠ 0
Tactic: rw [← toReal_injective.ne_iff, toReal_pi_div_two, toReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
⊢ (↑(-π / 2) : Angle) ≠ 0
have rw : -π / 2 ≠ 0
Tactic: rw [← toReal_injective.ne_iff, toReal_neg_pi_div_two, toReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
⊢ |(-(↑θ : Angle)).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π
have refine : ∀ (h : 0 ≤ θ ∧ θ ≤ π), |(-(↑θ : Angle)).toReal| = θ
Tactic: refine ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
⊢ |(-(↑θ : Angle)).toReal| = θ
have pos : ∀ (hnegpi : θ = π), |(-(↑θ : Angle)).toReal| = θ
Tactic: by_cases hnegpi : θ = π
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
pos : ∀ (hnegpi : θ = π), |(-(↑θ : Angle)).toReal| = θ
⊢ |(-(↑θ : Angle)).toReal| = θ
have neg : ∀ (hnegpi : ¬θ = π), |(-(↑θ : Angle)).toReal| = θ
Tactic: by_cases hnegpi : θ = π
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(-(↑θ : Angle)).toReal| = θ
have neg : |(↑(-θ) : Angle).toReal| = θ
Tactic: rw [← coe_neg,
    toReal_coe_eq_self_iff.2
      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
    abs_neg, abs_eq_self.2 h.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
neg : |(↑(-θ) : Angle).toReal| = θ
⊢ |(-(↑θ : Angle)).toReal| = θ
have neg₁ : |(-θ)| = θ
Tactic: rw [← coe_neg,
    toReal_coe_eq_self_iff.2
      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
    abs_neg, abs_eq_self.2 h.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
neg : |(↑(-θ) : Angle).toReal| = θ
neg₁ : |(-θ)| = θ
⊢ |(-(↑θ : Angle)).toReal| = θ
have neg₂ : |θ| = θ
Tactic: rw [← coe_neg,
    toReal_coe_eq_self_iff.2
      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
    abs_neg, abs_eq_self.2 h.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
neg : |(↑(-θ) : Angle).toReal| = θ
neg₁ : |(-θ)| = θ
neg₂ : |θ| = θ
⊢ |(-(↑θ : Angle)).toReal| = θ
have neg₃ : θ = θ
Tactic: rw [← coe_neg,
    toReal_coe_eq_self_iff.2
      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
    abs_neg, abs_eq_self.2 h.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
⊢ |θ.toReal| = π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw : θ.toReal = π / 2 ∨ θ.toReal = -(π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff,
    toReal_eq_neg_pi_div_two_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.toReal = π / 2 ∨ θ.toReal = -(π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ |θ.toReal| = π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₁ : θ.toReal = π / 2 ∨ θ.toReal = -π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff,
    toReal_eq_neg_pi_div_two_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.toReal = π / 2 ∨ θ.toReal = -(π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : θ.toReal = π / 2 ∨ θ.toReal = -π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ |θ.toReal| = π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₂ : θ = (↑(π / 2) : Angle) ∨ θ.toReal = -π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff,
    toReal_eq_neg_pi_div_two_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
θ : Angle
rw : θ.toReal = π / 2 ∨ θ.toReal = -(π / 2) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₁ : θ.toReal = π / 2 ∨ θ.toReal = -π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
rw₂ : θ = (↑(π / 2) : Angle) ∨ θ.toReal = -π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
⊢ |θ.toReal| = π / 2 ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
have rw₃ : θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle) ↔ θ = (↑(π / 2) : Angle) ∨ θ = (↑(-π / 2) : Angle)
Tactic: rw [abs_eq (div_nonneg Real.pi_pos.le two_pos.le), ← neg_div, toReal_eq_pi_div_two_iff,
    toReal_eq_neg_pi_div_two_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
⊢ (n • θ).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have nth_rw : (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
Tactic: nth_rw 1 [← coe_toReal θ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (hypothesis)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have h' : 0 < (n : ℝ) := mod_cast Nat.pos_of_ne_zero h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (goal)
Goal:
n : ℕ
h : n ≠ 0
θ : Angle
h' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (n • (↑θ.toReal : Angle)).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
have rw : (↑(n • θ.toReal) : Angle).toReal = (↑n : ℝ) * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / (↑n : ℝ)) (π / (↑n : ℝ))
Tactic: rw [← coe_nsmul, nsmul_eq_mul, toReal_coe_eq_self_iff, Set.mem_Ioc, div_lt_iff₀' h',
    le_div_iff₀' h']