awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan (HMul.hMul (α := ℝ) 2 2⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 2⁻¹ 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 7⁻¹ / (1 - HMul.hMul (α := ℝ) 1 7⁻¹))
rw₁ : HMul.hMul (α := ℝ) 1 7⁻¹ < 1
h₁ : LT.lt (α := ℝ) (-1) 2⁻¹
⊢ 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4
have h₂ : LT.lt (α := ℝ) 2⁻¹ 1
Tactic: rw [two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4
have rw : arctan
    ((HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) + 7⁻¹) /
      (1 - HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹)) =
  π / 4
Tactic: rw [two_mul_arctan, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      ((HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) + 7⁻¹) /
        (1 - HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹)) =
    π / 4
⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4
have rw₁ : HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹ < 1
Tactic: rw [two_mul_arctan, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      ((HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) + 7⁻¹) /
        (1 - HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹)) =
    π / 4
rw₁ : HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹ < 1
⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4
have h₁ : LT.lt (α := ℝ) (-1) 3⁻¹
Tactic: rw [two_mul_arctan, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      ((HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) + 7⁻¹) /
        (1 - HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹)) =
    π / 4
rw₁ : HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹ < 1
h₁ : LT.lt (α := ℝ) (-1) 3⁻¹
⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4
have h₂ : LT.lt (α := ℝ) 3⁻¹ 1
Tactic: rw [two_mul_arctan, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4
have rw : arctan
    (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
      (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
  arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))
Tactic: rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
        (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4
have rw₁ : HMul.hMul (α := ℝ) 1 239⁻¹ < 1
Tactic: rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
        (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))
rw₁ : HMul.hMul (α := ℝ) 1 239⁻¹ < 1
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4
have h₁ : -1 < HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)
Tactic: rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
        (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))
rw₁ : HMul.hMul (α := ℝ) 1 239⁻¹ < 1
h₁ : -1 < HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4
have h₂ : HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2) < 1
Tactic: rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
        (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))
rw₁ : HMul.hMul (α := ℝ) 1 239⁻¹ < 1
h₁ : -1 < HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)
h₂ : HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2) < 1
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4
have h₃ : LT.lt (α := ℝ) (-1) 5⁻¹
Tactic: rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan
      (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
        (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))
rw₁ : HMul.hMul (α := ℝ) 1 239⁻¹ < 1
h₁ : -1 < HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)
h₂ : HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2) < 1
h₃ : LT.lt (α := ℝ) (-1) 5⁻¹
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4
have h₄ : LT.lt (α := ℝ) 5⁻¹ 1
Tactic: rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (hypothesis)
Goal:
x : ℝ
hx : cos x = 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |tan x|) (𝓝[≠] x) atTop
have hx₁ : Complex.cos (↑x : ℂ) = 0
Tactic: have hx : Complex.cos x = 0 := mod_cast hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (goal)
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |tan x|) (𝓝[≠] x) atTop
have simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Complex.tan (↑x : ℂ)‖) (𝓝[≠] x) atTop
Tactic: simp only [← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_tan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (goal)
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Complex.tan (↑x : ℂ)‖) (𝓝[≠] x) atTop
have refine : Tendsto Complex.ofReal (𝓝[≠] x) (𝓝[≠] (↑x : ℂ))
Tactic: refine (Complex.tendsto_norm_tan_of_cos_eq_zero hx).comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (goal)
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
⊢ Tendsto Complex.ofReal (𝓝[≠] x) (𝓝[≠] (↑x : ℂ))
have refine : Tendsto Complex.ofReal (𝓟 {x}ᶜ) (𝓟 {(↑x : ℂ)}ᶜ)
Tactic: refine Tendsto.inf Complex.continuous_ofReal.continuousAt ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (goal)
Goal:
x : ℝ
⊢ ContinuousAt tan x ↔ cos x ≠ 0
have refine : ∀ (hc : ContinuousAt tan x) (h₀ : cos x = 0), False
Tactic: refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (hypothesis)
Goal:
x : ℝ
h : cos x = 0
⊢ deriv tan x = 1 / HPow.hPow (β := ℕ) (cos x) 2
have this : ¬DifferentiableAt ℝ tan x
Tactic: have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv (hypothesis)
Goal:
x : ℝ
⊢ HasStrictDerivAt arctan (1 / (1 + HPow.hPow (β := ℕ) x 2)) x
have A : cos (arctan x) ≠ 0
Tactic: have A : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos (π / 2) = 0
have rw : cos (Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero) = 0
Tactic: rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ 1 ≤ π / 2
have rw : 1 ≤ Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero
Tactic: rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ π / 2 ≤ 2
have rw : Classical.choose (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 1 2) x ∧ cos x = 0) exists_cos_eq_zero ≤ 2
Tactic: rw [Real.pi, mul_div_cancel_left₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ 2 / 2 ≤ π / 2
have rw : 1 ≤ π / 2
Tactic: rw [div_self two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ 0 < 2 * π
have linarith : 2 * π ≤ 0 → 2 * π - 0 + 2 * (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
linarith : 2 * π ≤ 0 → 2 * π - 0 + 2 * (0 - π) = 0
⊢ 0 < 2 * π
have linarith₁ : 2 * π ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ sin π = 0
have rw : sin (π / 2) * 0 + 0 * sin (π / 2) = 0
Tactic: rw [← mul_div_cancel_left₀ π two_ne_zero, two_mul, add_div, sin_add, cos_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
⊢ cos π = -1
have rw : 2 * HPow.hPow (α := ℝ) (β := ℕ) 0 2 - 1 = -1
Tactic: rw [← mul_div_cancel_left₀ π two_ne_zero, mul_div_assoc, cos_two_mul, cos_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
h0x : 0 < x
hxp : x < π
hx2 : ¬x ≤ 2
⊢ π - x ≤ 2
have linarith : 2 < π - x → 2 - x + (2 - (π - x)) + (π - 4) = 0
Tactic: linarith [pi_le_four]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (hypothesis)
Goal:
x : ℝ
hx : x ∈ Icc 0 π
⊢ 0 ≤ sin x
have hx₁ : x ∈ closure (Ioo 0 π)
Tactic: rw [← closure_Ioo pi_ne_zero.symm] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : |x| ≤ π
⊢ |sin x| = sin |x|
have inl : ∀ (h : x < 0), |sin x| = sin |x|
Tactic: rcases lt_or_ge x 0 with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : |x| ≤ π
inl : ∀ (h : x < 0), |sin x| = sin |x|
⊢ |sin x| = sin |x|
have inr : ∀ (h : 0 ≤ x), |sin x| = sin |x|
Tactic: rcases lt_or_ge x 0 with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : |x| ≤ π
h : x < 0
⊢ |sin x| = sin |x|
have inl : |sin x| = sin (-x)
Tactic: rw [abs_of_neg h, sin_neg,
      abs_of_nonpos (sin_nonpos_of_nonpos_of_neg_pi_le h.le (abs_le.1 hx).1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : |x| ≤ π
h : x < 0
inl : |sin x| = sin (-x)
⊢ |sin x| = sin |x|
have inl₁ : |sin x| = -sin x
Tactic: rw [abs_of_neg h, sin_neg,
      abs_of_nonpos (sin_nonpos_of_nonpos_of_neg_pi_le h.le (abs_le.1 hx).1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : |x| ≤ π
h : x < 0
inl : |sin x| = sin (-x)
inl₁ : |sin x| = -sin x
⊢ |sin x| = sin |x|
have inl₂ : -sin x = -sin x
Tactic: rw [abs_of_neg h, sin_neg,
      abs_of_nonpos (sin_nonpos_of_nonpos_of_neg_pi_le h.le (abs_le.1 hx).1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : |x| ≤ π
h : 0 ≤ x
⊢ |sin x| = sin |x|
have inr : |sin x| = sin x
Tactic: rw [abs_of_nonneg h, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi h (abs_le.1 hx).2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : |x| ≤ π
h : 0 ≤ x
inr : |sin x| = sin x
⊢ |sin x| = sin |x|
have inr₁ : sin x = sin x
Tactic: rw [abs_of_nonneg h, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi h (abs_le.1 hx).2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
⊢ cos (π / 2 - x) = sin x
have rw : cos (-(π / 2 - x)) = sin x
Tactic: rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : cos (-(π / 2 - x)) = sin x
⊢ cos (π / 2 - x) = sin x
have rw₁ : cos (x - π / 2) = sin x
Tactic: rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
rw : cos (-(π / 2 - x)) = sin x
rw₁ : cos (x - π / 2) = sin x
⊢ cos (π / 2 - x) = sin x
have rw₂ : sin x = sin x
Tactic: rw [← cos_neg, neg_sub, cos_sub_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ 0 ≤ x + π / 2
have linarith : x + π / 2 < 0 → 2 / 2 = 1
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : x + π / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ x + π / 2
have linarith₁ : x + π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : x + π / 2 < 0 → 2 / 2 = 1
linarith₁ : x + π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ x + π / 2
have linarith₂ : x + π / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : x + π / 2 < 0 → 2 / 2 = 1
linarith₁ : x + π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : x + π / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : x + π / 2 < 0 → 2 / 2 = 1
linarith₄ : x + π / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : x + π / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ x + π / 2
have linarith₆ : x + π / 2 < 0 → 2 * x + 1 * π - HMul.hMul (α := ℝ) 2 0 + (-(1 * π) - 2 * x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ x + π / 2 ≤ π
have linarith : π < x + π / 2 → 2 / 2 = 1
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : π < x + π / 2 → 2 / 2 = 1
⊢ x + π / 2 ≤ π
have linarith₁ : π < x + π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : π < x + π / 2 → 2 / 2 = 1
linarith₁ : π < x + π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ x + π / 2 ≤ π
have linarith₂ : π < x + π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
linarith : π < x + π / 2 → 2 / 2 = 1
linarith₁ : π < x + π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < x + π / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : π < x + π / 2 → 2 / 2 = 1
linarith₄ : π < x + π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π < x + π / 2 → GT.gt (α := ℝ) 2 0
⊢ x + π / 2 ≤ π
have linarith₆ : π < x + π / 2 → 2 * π - (2 * x + 1 * π) + (2 * x - 1 * π) = 0
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ -(π / 2) < π - x
have linarith : π - x ≤ -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π - x ≤ -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) < π - x
have linarith₁ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π - x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) < π - x
have linarith₂ : π - x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π - x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : π - x ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π - x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : π - x ≤ -(π / 2) → 2 / 2 = 1
linarith₇ : π - x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π - x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) < π - x
have linarith₉ : π - x ≤ -(π / 2) → 2 * x - (2 * π + 1 * π) + (2 * π - 2 * x - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ π - x < π / 2
have linarith : π / 2 ≤ π - x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π / 2 ≤ π - x → 2 / 2 = 1
⊢ π - x < π / 2
have linarith₁ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π / 2 ≤ π - x → 2 / 2 = 1
linarith₁ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π - x < π / 2
have linarith₂ : π / 2 ≤ π - x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
linarith : π / 2 ≤ π - x → 2 / 2 = 1
linarith₁ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ π - x → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 ≤ π - x → 2 / 2 = 1
linarith₄ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 ≤ π - x → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 ≤ π - x → 2 / 2 = 1
linarith₇ : π / 2 ≤ π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π / 2 ≤ π - x → GT.gt (α := ℝ) 2 0
⊢ π - x < π / 2
have linarith₉ : π / 2 ≤ π - x → 1 * π - 2 * x + (1 * π - (2 * π - 2 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ -(π / 2) ≤ π - x
have linarith : π - x < -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π - x < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ π - x
have linarith₁ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π - x < -(π / 2) → 2 / 2 = 1
linarith₁ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) ≤ π - x
have linarith₂ : π - x < -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π - x < -(π / 2) → 2 / 2 = 1
linarith₁ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - x < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : π - x < -(π / 2) → 2 / 2 = 1
linarith₄ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π - x < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : π - x < -(π / 2) → 2 / 2 = 1
linarith₇ : π - x < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π - x < -(π / 2) → GT.gt (α := ℝ) 2 0
⊢ -(π / 2) ≤ π - x
have linarith₉ : π - x < -(π / 2) → 2 * x - (2 * π + 1 * π) + (2 * π - 2 * x - -(1 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ π - x ≤ π / 2
have linarith : π / 2 < π - x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π / 2 < π - x → 2 / 2 = 1
⊢ π - x ≤ π / 2
have linarith₁ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π / 2 < π - x → 2 / 2 = 1
linarith₁ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π - x ≤ π / 2
have linarith₂ : π / 2 < π - x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
linarith : π / 2 < π - x → 2 / 2 = 1
linarith₁ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 < π - x → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 < π - x → 2 / 2 = 1
linarith₄ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 < π - x → GT.gt (α := ℝ) 2 0
linarith₆ : π / 2 < π - x → 2 / 2 = 1
linarith₇ : π / 2 < π - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : π / 2 < π - x → GT.gt (α := ℝ) 2 0
⊢ π - x ≤ π / 2
have linarith₉ : π / 2 < π - x → 1 * π - 2 * x + (1 * π - (2 * π - 2 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hu : x ≤ π
⊢ sin x = √(1 - HPow.hPow (β := ℕ) (cos x) 2)
have rw : sin x = |sin x|
Tactic: rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : 0 ≤ x
hu : x ≤ π
rw : sin x = |sin x|
⊢ sin x = √(1 - HPow.hPow (β := ℕ) (cos x) 2)
have rw₁ : sin x = sin x
Tactic: rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
⊢ cos x = √(1 - HPow.hPow (β := ℕ) (sin x) 2)
have rw : cos x = |cos x|
Tactic: rw [← abs_cos_eq_sqrt_one_sub_sin_sq, abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨hl, hu⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
rw : cos x = |cos x|
⊢ cos x = √(1 - HPow.hPow (β := ℕ) (sin x) 2)
have rw₁ : cos x = cos x
Tactic: rw [← abs_cos_eq_sqrt_one_sub_sin_sq, abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨hl, hu⟩)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ x / 2 ∈ Icc (-(π / 2)) (π / 2)
have left : -(π / 2) ≤ x / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
left : -(π / 2) ≤ x / 2
⊢ x / 2 ∈ Icc (-(π / 2)) (π / 2)
have right : x / 2 ≤ π / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ -(π / 2) ≤ x / 2
have linarith : x / 2 < -(π / 2) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (goal)
Goal:
x : ℝ
hl : -π ≤ x
hr : x ≤ π
linarith : x / 2 < -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) ≤ x / 2
have linarith₁ : x / 2 < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith