awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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 (β := ℕ) (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

Premises used: Iff.mpr, eq_sub_iff_add_eq', Real.arcsin, Real.sqrt_mul_self, sq, Real.cos_arcsin_nonneg, Real.sin_sq_le_one, sq_nonneg, sub_nonneg, Real.sqrt_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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)
pos₁ pos₂ : √(1 - HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [this, sin_arcsin hx₁ hx₂]

Premises used: Real.sin_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw : sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
⊢ tan (arcsin x) = x / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [tan_eq_sin_div_cos, cos_arcsin]

Premises used: Real.cos_arcsin, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
pos : ∀ (hx₁ : -1 ≤ x), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
neg : ∀ (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)

Tactic:
by_cases hx₁ : -1 ≤ x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
nlinarith₁ : 0 < 1 - HPow.hPow (β := ℕ) x 2 → GT.gt (α := ℝ) 2 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ √(1 - HPow.hPow (β := ℕ) x 2) = 0

Tactic:
have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
neg : sin (arcsin x) / 0 = x / 0
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
⊢ sin (arcsin x) / 0 = x / 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
pos : ∀ (hx₂ : x ≤ 1), sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)
neg : ∀ (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)

Tactic:
by_cases hx₂ : x ≤ 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
nlinarith : 0 < 1 - HPow.hPow (β := ℕ) x 2 → 0 - (1 - HPow.hPow (β := ℕ) x 2) + (0 - (-1 - x) * (1 - x)) = 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 0

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ √(1 - HPow.hPow (β := ℕ) x 2) = 0

Tactic:
have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
neg : sin (arcsin x) / 0 = x / 0
⊢ sin (arcsin x) / √(1 - HPow.hPow (β := ℕ) x 2) = x / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : √(1 - HPow.hPow (β := ℕ) x 2) = 0
⊢ sin (arcsin x) / 0 = x / 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
pos pos₁ : 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)

Tactic:
rw [sin_arcsin hx₁ hx₂]

Premises used: Real.sin_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arccos x = π / 2 - arcsin x

Tactic:
rfl

Premises used: rfl, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x = π / 2 - arccos x

Tactic:
simp [arccos]

Premises used: Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
linarith₆ : π < π / 2 - arcsin x → 2 * π - (1 * π - 2 * arcsin x) + (-(1 * π) - 2 * arcsin x) = 0
⊢ π / 2 - arcsin x ≤ π

Tactic:
linarith [neg_pi_div_two_le_arcsin x]

Premises used: Real.neg_pi_div_two_le_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
linarith₆ : π / 2 - arcsin x < 0 → 1 * π - 2 * arcsin x - HMul.hMul (α := ℝ) 2 0 + (2 * arcsin x - 1 * π) = 0
⊢ 0 ≤ π / 2 - arcsin x

Tactic:
linarith [arcsin_le_pi_div_two x]

Premises used: Real.arcsin_le_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ 0 < arccos x ↔ x < 1

Tactic:
simp [arccos]

Premises used: Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
rw : cos (π / 2 - arcsin x) = x
rw₁ : sin (arcsin x) = x
rw₂ rw₃ : x = x
⊢ cos (arccos x) = x

Tactic:
rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]

Premises used: Real.sin_arcsin, Real.cos_pi_div_two_sub, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
rw : π / 2 - (π / 2 - x) = x
hx₃ : -(π / 2) ≤ π / 2 - x
hx₄ : π / 2 - x ≤ π / 2
⊢ arccos (cos x) = x

Tactic:
rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]

Premises used: Real.sin_pi_div_two_sub, Real.arcsin_sin, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - (π / 2 - x) = x

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ hx₃ : x ≤ π
⊢ -(π / 2) ≤ π / 2 - x

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
hx₃ : 0 ≤ x
⊢ π / 2 - x ≤ π / 2

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
linarith : π < x → x - π + (π - x) = 0
⊢ x ≤ π

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
linarith : x < 0 → 0 - x + (x - 0) = 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
rw : arccos (cos y) = y
rw₁ rw₂ : y = y
⊢ arccos x = y

Tactic:
rw [hxy, arccos_cos hy₀ hy₁]

Premises used: Real.arccos_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ StrictAntiOn arccos (Icc (-1) 1)

Tactic:
fun _ hx _ hy h =>
  sub_lt_sub_left (strictMonoOn_arcsin hx hy h) _

Premises used: Real.pi, StrictAntiOn, HDiv.hDiv, Real.strictMonoOn_arcsin, OfNat.ofNat, sub_lt_sub_left, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
h : -1 ≤ x
h₁ : y ≤ 1
⊢ π / 2 - arcsin y < π / 2 - arcsin x

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hlt : x ≤ y
⊢ π / 2 - arcsin y ≤ π / 2 - arcsin x

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ Antitone arccos

Tactic:
fun _ _ ↦ arccos_le_arccos

Premises used: Antitone, Real.arccos_le_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ InjOn arccos (Icc (-1) 1)

Tactic:
strictAntiOn_arccos.injOn

Premises used: Real.strictAntiOn_arccos, StrictAntiOn.injOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
hy₁ : -1 ≤ y
hy₂ : y ≤ 1
⊢ arccos x = arccos y ↔ x = y

Tactic:
arccos_injOn.eq_iff ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩

Premises used: Set.InjOn.eq_iff, And.intro, Real.arccos_injOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ arccos 0 = π / 2

Tactic:
simp [arccos]

Premises used: Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ arccos 1 = 0

Tactic:
simp [arccos]

Premises used: Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ arccos (-1) = π

Tactic:
simp [arccos, add_halves]

Premises used: add_halves, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arccos x = 0 ↔ 1 ≤ x

Tactic:
simp [arccos, sub_eq_zero]

Premises used: sub_eq_zero, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arccos x = π / 2 ↔ x = 0

Tactic:
simp [arccos]

Premises used: Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
rw₄ rw₅ : x ≤ -1 ↔ x ≤ -1
⊢ arccos 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]

Premises used: Real.neg_pi_div_two_eq_arcsin, div_two_sub_self, sub_eq_iff_eq_add, sub_eq_iff_eq_add', Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arccos x < π ↔ -1 < x

Tactic:
grind [arccos_le_pi, arccos_eq_pi]

Premises used: Real.arccos_le_pi, Real.arccos_eq_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
rw₆ rw₇ : π / 2 + arcsin x = π / 2 + arcsin x
⊢ arccos (-x) = π - arccos x

Tactic:
rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]

Premises used: add_sub_assoc, Real.pi, add_halves, Real.arcsin_neg, sub_sub_self, sub_neg_eq_add, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx : 1 ≤ x
rw : π / 2 - arcsin x = 0
rw₁ : π / 2 - π / 2 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ arccos x = 0

Tactic:
rw [arccos, arcsin_of_one_le hx, sub_self]

Premises used: sub_self, Real.arcsin_of_one_le, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx : x ≤ -1
rw : π / 2 - arcsin x = π
rw₁ : π / 2 - -(π / 2) = π
rw₂ : π / 2 + π / 2 = π
rw₃ rw₄ : π = π
⊢ arccos x = π

Tactic:
rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]

Premises used: add_halves, Real.arcsin_of_le_neg_one, sub_neg_eq_add, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
pos : ∀ (hx₁ : -1 ≤ x), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
neg : ∀ (hx₁ : ¬-1 ≤ x), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
by_cases hx₁ : -1 ≤ x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : x < -1
neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]

Premises used: Real.sin_pi, Real.sqrt_eq_zero_of_nonpos, LT.lt.le, Real.arccos_of_le_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
pos : ∀ (hx₂ : x ≤ 1), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
neg : ∀ (hx₂ : ¬x ≤ 1), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
by_cases hx₂ : x ≤ 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]

Premises used: Real.sin_zero, Real.sqrt_eq_zero_of_nonpos, LT.lt.le, Real.arccos_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
pos : sin (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
pos₁ : cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
pos₂ pos₃ : √(1 - HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]

Premises used: Real.cos_arcsin, Real.arccos_eq_pi_div_two_sub_arcsin, Real.sin_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arccos x ≤ π / 2 ↔ 0 ≤ x

Tactic:
simp [arccos]

Premises used: Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arccos x < π / 2 ↔ 0 < x

Tactic:
simp [arccos]

Premises used: Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw : π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
⊢ arccos x ≤ π / 4 ↔ √2 / 2 ≤ x

Tactic:
rw [arccos, ← pi_div_four_le_arcsin]

Premises used: Real.pi_div_four_le_arcsin, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
mp : π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x
mpr : π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h : π / 2 - arcsin x ≤ π / 4
linarith : arcsin x < π / 4 → 4 / 4 = 1
linarith₁ : arcsin x < π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : arcsin x < π / 4 → GT.gt (α := ℝ) 4 0
linarith₃ : arcsin x < π / 4 → 2 / 2 = 1
linarith₄ : arcsin x < π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₅ : arcsin x < π / 4 → 4 / 4 = 1
linarith₆ : arcsin x < π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₇ : arcsin x < π / 4 → GT.gt (α := ℝ) 4 0
linarith₈ : arcsin x < π / 4 → 2 * π - 4 * arcsin x - 1 * π + (4 * arcsin x - 1 * π) = 0
⊢ π / 4 ≤ arcsin x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h : π / 4 ≤ arcsin x
linarith : π / 4 < π / 2 - arcsin x → 4 / 4 = 1
linarith₁ : π / 4 < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : π / 4 < π / 2 - arcsin x → 2 / 2 = 1
linarith₃ : π / 4 < π / 2 - arcsin x → HMul.hMul (α := ℝ) 2 2 = 4
linarith₄ : π / 4 < π / 2 - arcsin x → GT.gt (α := ℝ) 4 0
linarith₅ : π / 4 < π / 2 - arcsin x → 4 / 4 = 1
linarith₆ : π / 4 < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₇ : π / 4 < π / 2 - arcsin x → GT.gt (α := ℝ) 4 0
linarith₈ : π / 4 < π / 2 - arcsin x → 1 * π - 4 * arcsin x + (1 * π - (2 * π - 4 * arcsin x)) = 0
⊢ π / 2 - arcsin x ≤ π / 4

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ Continuous arccos

Tactic:
continuous_const.sub continuous_arcsin

Premises used: Real.continuous_arcsin, continuous_const, Continuous.sub, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw : tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
rw₁ : (tan (arcsin x))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
rw₂ : (x / √(1 - HPow.hPow (β := ℕ) x 2))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
rw₃ rw₄ : √(1 - HPow.hPow (β := ℕ) x 2) / x = √(1 - HPow.hPow (β := ℕ) x 2) / x
⊢ tan (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2) / x

Tactic:
rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]

Premises used: Real.tan_pi_div_two_sub, inv_div, Real.tan_arcsin, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h : 0 ≤ x
⊢ LE.le (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h : 0 ≤ x
rw : arccos (cos (arcsin x)) = arcsin x
⊢ arcsin x = arccos √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [eq_comm, ← cos_arcsin]

Premises used: Real.cos_arcsin, eq_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x

Tactic:
arccos_cos (arcsin_nonneg.2 h)
      ((arcsin_le_pi_div_two _).trans (div_le_self pi_pos.le one_le_two))

Premises used: Iff.mpr, Real.arcsin_le_pi_div_two, Real.pi_pos, LT.lt.le, div_le_self, Real.arccos_cos, Real.arcsin_nonneg, one_le_two, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x

Tactic:
exact
    arccos_cos (arcsin_nonneg.2 h)
      ((arcsin_le_pi_div_two _).trans (div_le_self pi_pos.le one_le_two))

Premises used: Iff.mpr, Real.arcsin_le_pi_div_two, Real.pi_pos, LT.lt.le, div_le_self, Real.arccos_cos, Real.arcsin_nonneg, one_le_two, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
⊢ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-(π / 2)) (π / 2) → Membership.mem (γ := Set ℝ) (Ioo (-1) 1) (sin x)

Tactic:
grind [arcsin_lt_pi_div_two, neg_pi_div_two_lt_arcsin, arcsin_sin]

Premises used: Real.neg_pi_div_two_lt_arcsin, Real.arcsin_sin, Real.arcsin_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x_1 y x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) (sin x)

Tactic:
simpa [← abs_le] using abs_sin_le_one x

Premises used: abs_le, Real.abs_sin_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y θ : ℝ
hθ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ -(π / 2) ≤ θ

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y θ : ℝ
hθ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ θ ≤ π / 2

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x_1 y x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
⊢ -1 ≤ x

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x_1 y x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
⊢ x ≤ 1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ MapsTo sin (Ioo (-(π / 2)) (π / 2)) (Ioo (-1) 1)

Tactic:
sinPartialHomeomorph.map_source'

Premises used: Real.sinPartialHomeomorph, PartialEquiv.map_source', Set.Mem, setOf, Set.MapsTo, OpenPartialHomeomorph.toPartialEquiv, Real.sin, Set.Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ arcsin '' Icc (-1) 1 = Icc (-(π / 2)) (π / 2)

Tactic:
simpa using sinPartialEquiv.symm.image_source_eq_target

Premises used: PartialEquiv.image_source_eq_target, PartialEquiv.symm, Real.sinPartialEquiv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
⊢ ∀ ⦃x : ℝ⦄, x ∈ Ioo 0 π → Membership.mem (γ := Set ℝ) (Ioo (-1) 1) (cos x)

Tactic:
grind [arccos_pos, arccos_lt_pi, arccos_cos]

Premises used: Real.arccos_pos, Real.arccos_lt_pi, Real.arccos_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x_1 y x : ℝ
hx : x ∈ Icc 0 π
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) (cos x)

Tactic:
simpa [← abs_le] using abs_cos_le_one x

Premises used: Real.abs_cos_le_one, abs_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y θ : ℝ
hθ : θ ∈ Icc 0 π
⊢ 0 ≤ θ

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y θ : ℝ
hθ : θ ∈ Icc 0 π
⊢ θ ≤ π

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ MapsTo cos (Ioo 0 π) (Ioo (-1) 1)

Tactic:
cosPartialHomeomorph.map_source'

Premises used: Real.cos, PartialEquiv.map_source', Set.Mem, setOf, Real.cosPartialHomeomorph, Set.MapsTo, OpenPartialHomeomorph.toPartialEquiv, Set.Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ arccos '' Icc (-1) 1 = Icc 0 π

Tactic:
simpa using cosPartialEquiv.symm.image_source_eq_target

Premises used: PartialEquiv.image_source_eq_target, PartialEquiv.symm, Real.cosPartialEquiv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝 x)
⊢ Tendsto (fun (x : α) ↦ arcsin (f x)) l (𝓝 (arcsin x))

Tactic:
(continuous_arcsin.tendsto _).comp h

Premises used: Real.continuous_arcsin, Real.arcsin, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
⊢ Tendsto (fun (x : α) ↦ arcsin (f x)) l (𝓝[≤] arcsin x)

Tactic:
((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h

Premises used: Set.MapsTo.tendsto, Real.continuous_arcsin, Real.arcsin, nhdsWithin, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
refine : ∀ (y : ℝ) (hy : y ∈ Iic x), arcsin y ∈ Iic (arcsin x)
⊢ Tendsto (fun (x : α) ↦ arcsin (f x)) l (𝓝[≤] arcsin x)

Tactic:
refine ((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h

Premises used: Set.MapsTo.tendsto, Real.continuous_arcsin, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
y : ℝ
hy : y ∈ Iic x
⊢ arcsin y ∈ Iic (arcsin x)

Tactic:
monotone_arcsin hy

Premises used: Real.monotone_arcsin, Set.Mem, setOf, Set.Iic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
y : ℝ
hy : y ∈ Iic x
⊢ arcsin y ∈ Iic (arcsin x)

Tactic:
exact monotone_arcsin hy

Premises used: Real.monotone_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
⊢ Tendsto (fun (x : α) ↦ arcsin (f x)) l (𝓝[≥] arcsin x)

Tactic:
((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun _ ↦ arcsin_le_arcsin).comp h

Premises used: Set.MapsTo.tendsto, Real.continuous_arcsin, Set.Ici, Real.arcsin, Set.Mem, nhdsWithin, setOf, Real.arcsin_le_arcsin, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝 x)
⊢ Tendsto (fun (x : α) ↦ arccos (f x)) l (𝓝 (arccos x))

Tactic:
(continuous_arccos.tendsto _).comp h

Premises used: Continuous.tendsto, Filter.Tendsto.comp, Real.continuous_arccos, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
⊢ Tendsto (fun (x : α) ↦ arccos (f x)) l (𝓝[≥] arccos x)

Tactic:
((continuous_arccos.tendsto _).inf <| MapsTo.tendsto fun _ ↦ arccos_le_arccos).comp h

Premises used: Set.MapsTo.tendsto, Set.Ici, Set.Mem, nhdsWithin, setOf, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.inf, Real.arccos_le_arccos, Real.continuous_arccos, Real.arccos