awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 4 ≤ -(π / 2) → 4 / 4 = 1
linarith₁ : π / 4 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : π / 4 ≤ -(π / 2) → 2 / 2 = 1
linarith₃ : π / 4 ≤ -(π / 2) → HMul.hMul (α := ℝ) 2 2 = 4
linarith₄ : π / 4 ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
⊢ -(π / 2) < π / 4
have linarith₅ : π / 4 ≤ -(π / 2) → 3 * (0 - π) + (1 * π - -(2 * π)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 4 ≤ -(π / 2) → 4 / 4 = 1
linarith₁ : π / 4 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : π / 4 ≤ -(π / 2) → 2 / 2 = 1
linarith₃ : π / 4 ≤ -(π / 2) → HMul.hMul (α := ℝ) 2 2 = 4
linarith₄ : π / 4 ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
linarith₅ : π / 4 ≤ -(π / 2) → 3 * (0 - π) + (1 * π - -(2 * π)) = 0
⊢ -(π / 2) < π / 4
have linarith₆ : π / 4 ≤ -(π / 2) → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
⊢ π / 4 ≤ π / 2
have linarith : π / 2 < π / 4 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 2 < π / 4 → 2 / 2 = 1
⊢ π / 4 ≤ π / 2
have linarith₁ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 2 < π / 4 → 2 / 2 = 1
linarith₁ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
⊢ π / 4 ≤ π / 2
have linarith₂ : π / 2 < π / 4 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 2 < π / 4 → 2 / 2 = 1
linarith₁ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : π / 2 < π / 4 → 4 / 4 = 1
⊢ π / 4 ≤ π / 2
have linarith₃ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 2 < π / 4 → 2 / 2 = 1
linarith₁ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : π / 2 < π / 4 → 4 / 4 = 1
linarith₃ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ π / 4 ≤ π / 2
have linarith₄ : π / 2 < π / 4 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 2 < π / 4 → 2 / 2 = 1
linarith₁ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : π / 2 < π / 4 → 4 / 4 = 1
linarith₃ : π / 2 < π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : π / 2 < π / 4 → GT.gt (α := ℝ) 4 0
⊢ π / 4 ≤ π / 2
have linarith₅ : π / 2 < π / 4 → 0 - π + (2 * π - 1 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos : ∀ (hx₁ : -1 ≤ x), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₁ : -1 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
pos : ∀ (hx₁ : -1 ≤ x), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : ∀ (hx₁ : ¬-1 ≤ x), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₁ : -1 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have hx₂ : x < -1
Tactic: rw [not_le] at hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
Tactic: rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : x < -1
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
have nlinarith : 0 < 1 - HPow.hPow (β := ℕ) x 2 → 2 * (x - -1) + (0 - (1 - HPow.hPow (β := ℕ) x 2)) + (0 - (x - -1) * (x - -1)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : x < -1
nlinarith :
  0 < 1 - HPow.hPow (β := ℕ) x 2 → 2 * (x - -1) + (0 - (1 - HPow.hPow (β := ℕ) x 2)) + (0 - (x - -1) * (x - -1)) = 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
have nlinarith₁ : 0 < 1 - HPow.hPow (β := ℕ) x 2 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos : ∀ (hx₂ : x ≤ 1), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₂ : x ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
pos : ∀ (hx₂ : x ≤ 1), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : ∀ (hx₂ : ¬x ≤ 1), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₂ : x ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have hx₃ : 1 < x
Tactic: rw [not_le] at hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
Tactic: rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
have nlinarith : 0 < 1 - HPow.hPow (β := ℕ) x 2 → 0 - (1 - HPow.hPow (β := ℕ) x 2) + (0 - (-1 - x) * (1 - x)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have this : HPow.hPow (β := ℕ) (sin (arcsin x)) 2 + HPow.hPow (β := ℕ) (cos (arcsin x)) 2 = 1
Tactic: have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : HPow.hPow (β := ℕ) (sin (arcsin x)) 2 + HPow.hPow (β := ℕ) (cos (arcsin x)) 2 = 1
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have this₁ : cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) (sin (arcsin x)) 2)
Tactic: rw [← eq_sub_iff_add_eq', ← sqrt_inj (sq_nonneg _) (sub_nonneg.2 (sin_sq_le_one (arcsin x))), sq,
    sqrt_mul_self (cos_arcsin_nonneg _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) (sin (arcsin x)) 2)
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos : √(1 - HPow.hPow (β := ℕ) (sin (arcsin x)) 2) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [this, sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) (sin (arcsin x)) 2)
pos : √(1 - HPow.hPow (β := ℕ) (sin (arcsin x)) 2) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos₁ : √(1 - HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [this, sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ tan (arcsin x) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have rw : sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [tan_eq_sin_div_cos, cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have pos : ∀ (hx₁ : -1 ≤ x), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₁ : -1 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
pos : ∀ (hx₁ : -1 ≤ x), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have neg : ∀ (hx₁ : ¬-1 ≤ x), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₁ : -1 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
have nlinarith : 0 < 1 - HPow.hPow (β := ℕ) x 2 → 2 * (x - -1) + (0 - (1 - HPow.hPow (β := ℕ) x 2)) + (0 - (x - -1) * (x - -1)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
nlinarith :
  0 < 1 - HPow.hPow (β := ℕ) x 2 → 2 * (x - -1) + (0 - (1 - HPow.hPow (β := ℕ) x 2)) + (0 - (x - -1) * (x - -1)) = 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
have nlinarith₁ : 0 < 1 - HPow.hPow (β := ℕ) x 2 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
Tactic: have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have neg : sin (arcsin x) / 0 = x / 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have pos : ∀ (hx₂ : x ≤ 1), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₂ : x ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
pos : ∀ (hx₂ : x ≤ 1), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have neg : ∀ (hx₂ : ¬x ≤ 1), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₂ : x ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
have nlinarith : 0 < 1 - HPow.hPow (β := ℕ) x 2 → 0 - (1 - HPow.hPow (β := ℕ) x 2) + (0 - (-1 - x) * (1 - x)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
Tactic: have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have neg : sin (arcsin x) / 0 = x / 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
have pos : x / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ π / 2 - arcsin x ≤ π
have linarith : π < π / 2 - arcsin x → 2 / 2 = 1
Tactic: linarith [neg_pi_div_two_le_arcsin x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
linarith : π < π / 2 - arcsin x → 2 / 2 = 1
⊢ π / 2 - arcsin x ≤ π
have linarith₁ : π < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [neg_pi_div_two_le_arcsin x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
linarith : π < π / 2 - arcsin x → 2 / 2 = 1
linarith₁ : π < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π / 2 - arcsin x ≤ π
have linarith₂ : π < π / 2 - arcsin x → GT.gt (α := ℝ) 2 0
Tactic: linarith [neg_pi_div_two_le_arcsin x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
linarith : π < π / 2 - arcsin x → 2 / 2 = 1
linarith₁ : π < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π < π / 2 - arcsin x → GT.gt (α := ℝ) 2 0
linarith₃ : π < π / 2 - arcsin x → 2 / 2 = 1
linarith₄ : π < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π < π / 2 - arcsin x → GT.gt (α := ℝ) 2 0
⊢ π / 2 - arcsin x ≤ π
have linarith₆ : π < π / 2 - arcsin x → 2 * π - (1 * π - 2 * arcsin x) + (-(1 * π) - 2 * arcsin x) = 0
Tactic: linarith [neg_pi_div_two_le_arcsin x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ 0 ≤ π / 2 - arcsin x
have linarith : π / 2 - arcsin x < 0 → 2 / 2 = 1
Tactic: linarith [arcsin_le_pi_div_two x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
linarith : π / 2 - arcsin x < 0 → 2 / 2 = 1
⊢ 0 ≤ π / 2 - arcsin x
have linarith₁ : π / 2 - arcsin x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [arcsin_le_pi_div_two x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
linarith : π / 2 - arcsin x < 0 → 2 / 2 = 1
linarith₁ : π / 2 - arcsin x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ π / 2 - arcsin x
have linarith₂ : π / 2 - arcsin x < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [arcsin_le_pi_div_two x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
linarith : π / 2 - arcsin x < 0 → 2 / 2 = 1
linarith₁ : π / 2 - arcsin x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 - arcsin x < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 - arcsin x < 0 → 2 / 2 = 1
linarith₄ : π / 2 - arcsin x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 - arcsin x < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ π / 2 - arcsin x
have linarith₆ : π / 2 - arcsin x < 0 → 1 * π - 2 * arcsin x - HMul.hMul (α := ℝ) 2 0 + (2 * arcsin x - 1 * π) = 0
Tactic: linarith [arcsin_le_pi_div_two x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arccos x) = x
have rw : cos (π / 2 - arcsin x) = x
Tactic: rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
rw : cos (π / 2 - arcsin x) = x
⊢ cos (arccos x) = x
have rw₁ : sin (arcsin x) = x
Tactic: rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
rw : cos (π / 2 - arcsin x) = x
rw₁ : sin (arcsin x) = x
⊢ cos (arccos x) = x
have rw₂ : x = x
Tactic: rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ arccos (cos x) = x
have rw : π / 2 - (π / 2 - x) = x
Tactic: rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
rw : π / 2 - (π / 2 - x) = x
⊢ arccos (cos x) = x
have hx₃ : -(π / 2) ≤ π / 2 - x
Tactic: rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
rw : π / 2 - (π / 2 - x) = x
hx₃ : -(π / 2) ≤ π / 2 - x
⊢ arccos (cos x) = x
have hx₄ : π / 2 - x ≤ π / 2
Tactic: rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ x ≤ π
have linarith : π < x → x - π + (π - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ 0 ≤ x
have linarith : x < 0 → 0 - x + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
⊢ arccos x = y
have rw : arccos (cos y) = y
Tactic: rw [hxy, arccos_cos hy₀ hy₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
rw : arccos (cos y) = y
⊢ arccos x = y
have rw₁ : y = y
Tactic: rw [hxy, arccos_cos hy₀ hy₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ arccos x = π ↔ x ≤ -1
have rw : π / 2 - arcsin x = π ↔ x ≤ -1
Tactic: rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : π / 2 - arcsin x = π ↔ x ≤ -1
⊢ arccos x = π ↔ x ≤ -1
have rw₁ : π / 2 = π + arcsin x ↔ x ≤ -1
Tactic: rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : π / 2 - arcsin x = π ↔ x ≤ -1
rw₁ : π / 2 = π + arcsin x ↔ x ≤ -1
⊢ arccos x = π ↔ x ≤ -1
have rw₂ : π / 2 - π = arcsin x ↔ x ≤ -1
Tactic: rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : π / 2 - arcsin x = π ↔ x ≤ -1
rw₁ : π / 2 = π + arcsin x ↔ x ≤ -1
rw₂ : π / 2 - π = arcsin x ↔ x ≤ -1
⊢ arccos x = π ↔ x ≤ -1
have rw₃ : -(π / 2) = arcsin x ↔ x ≤ -1
Tactic: rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : π / 2 - arcsin x = π ↔ x ≤ -1
rw₁ : π / 2 = π + arcsin x ↔ x ≤ -1
rw₂ : π / 2 - π = arcsin x ↔ x ≤ -1
rw₃ : -(π / 2) = arcsin x ↔ x ≤ -1
⊢ arccos x = π ↔ x ≤ -1
have rw₄ : x ≤ -1 ↔ x ≤ -1
Tactic: rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ arccos (-x) = π - arccos x
have rw : arccos (-x) = π / 2 + π / 2 - arccos x
Tactic: rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : arccos (-x) = π / 2 + π / 2 - arccos x
⊢ arccos (-x) = π - arccos x
have rw₁ : π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x
Tactic: rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : arccos (-x) = π / 2 + π / 2 - arccos x
rw₁ : π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x
⊢ arccos (-x) = π - arccos x
have rw₂ : π / 2 - -arcsin x = π / 2 + π / 2 - arccos x
Tactic: rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : arccos (-x) = π / 2 + π / 2 - arccos x
rw₁ : π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x
rw₂ : π / 2 - -arcsin x = π / 2 + π / 2 - arccos x
⊢ arccos (-x) = π - arccos x
have rw₃ : π / 2 - -arcsin x = π / 2 + π / 2 - (π / 2 - arcsin x)
Tactic: rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : arccos (-x) = π / 2 + π / 2 - arccos x
rw₁ : π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x
rw₂ : π / 2 - -arcsin x = π / 2 + π / 2 - arccos x
rw₃ : π / 2 - -arcsin x = π / 2 + π / 2 - (π / 2 - arcsin x)
⊢ arccos (-x) = π - arccos x
have rw₄ : π / 2 - -arcsin x = π / 2 + (π / 2 - (π / 2 - arcsin x))
Tactic: rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : arccos (-x) = π / 2 + π / 2 - arccos x
rw₁ : π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x
rw₂ : π / 2 - -arcsin x = π / 2 + π / 2 - arccos x
rw₃ : π / 2 - -arcsin x = π / 2 + π / 2 - (π / 2 - arcsin x)
rw₄ : π / 2 - -arcsin x = π / 2 + (π / 2 - (π / 2 - arcsin x))
⊢ arccos (-x) = π - arccos x
have rw₅ : π / 2 - -arcsin x = π / 2 + arcsin x
Tactic: rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : arccos (-x) = π / 2 + π / 2 - arccos x
rw₁ : π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x
rw₂ : π / 2 - -arcsin x = π / 2 + π / 2 - arccos x
rw₃ : π / 2 - -arcsin x = π / 2 + π / 2 - (π / 2 - arcsin x)
rw₄ : π / 2 - -arcsin x = π / 2 + (π / 2 - (π / 2 - arcsin x))
rw₅ : π / 2 - -arcsin x = π / 2 + arcsin x
⊢ arccos (-x) = π - arccos x
have rw₆ : π / 2 + arcsin x = π / 2 + arcsin x
Tactic: rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ arccos x = 0
have rw : π / 2 - arcsin x = 0
Tactic: rw [arccos, arcsin_of_one_le hx, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : 1 ≤ x
rw : π / 2 - arcsin x = 0
⊢ arccos x = 0
have rw₁ : π / 2 - π / 2 = 0
Tactic: rw [arccos, arcsin_of_one_le hx, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : 1 ≤ x
rw : π / 2 - arcsin x = 0
rw₁ : π / 2 - π / 2 = 0
⊢ arccos x = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [arccos, arcsin_of_one_le hx, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : x ≤ -1
⊢ arccos x = π
have rw : π / 2 - arcsin x = π
Tactic: rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : x ≤ -1
rw : π / 2 - arcsin x = π
⊢ arccos x = π
have rw₁ : π / 2 - -(π / 2) = π
Tactic: rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : x ≤ -1
rw : π / 2 - arcsin x = π
rw₁ : π / 2 - -(π / 2) = π
⊢ arccos x = π
have rw₂ : π / 2 + π / 2 = π
Tactic: rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : x ≤ -1
rw : π / 2 - arcsin x = π
rw₁ : π / 2 - -(π / 2) = π
rw₂ : π / 2 + π / 2 = π
⊢ arccos x = π
have rw₃ : π = π
Tactic: rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos : ∀ (hx₁ : -1 ≤ x), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₁ : -1 ≤ x