awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw :
  Eq (α := ℝ)
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      (↑(projIcc (-1) 1 ⋯ x) : ℝ))
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      x)
rw₁ :
  Eq (α := ℝ)
    (↑(IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type))
          (↑(projIcc (-1) 1 ⋯ x) : ℝ)) :
      ℝ)
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      x)
rw₂ :
  Eq (α := ℝ)
    (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 ⋯ x)) : ℝ)
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      x)
rw₃ :
  Eq (α := ℝ)
    (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 ⋯ x)) : ℝ)
    (↑(IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type))
          x) :
      ℝ)
rw₄ :
  Eq (α := ℝ)
    (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 ⋯ x)) : ℝ)
    (↑(((⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) ∘
            projIcc (-1) 1 arcsin._proof_2)
          x) :
      ℝ)
rw₅ rw₆ :
  Eq (α := ℝ)
    (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 ⋯ x)) : ℝ)
    (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type))
          (projIcc (-1) 1 arcsin._proof_2 x)) :
      ℝ)
⊢ arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = arcsin x

Tactic:
rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]

Premises used: Real.arcsin, Set.IccExtend_val, Function.comp_apply, Set.IccExtend
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
⊢ sin (arcsin x) = x

Tactic:
simpa [arcsin, IccExtend_of_mem _ _ hx, -OrderIso.apply_symm_apply] using
    Subtype.ext_iff.1 (sinOrderIso.apply_symm_apply ⟨x, hx⟩)

Premises used: OrderIso.apply_symm_apply, Real.arcsin, Set.IccExtend_of_mem, Real.sinOrderIso, Subtype.ext_iff, Subtype.mk, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) = x

Tactic:
sin_arcsin' ⟨hx₁, hx₂⟩

Premises used: Real.sin_arcsin', And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
rw rw₁ : sin x = sin x
⊢ sin (arcsin (sin x)) = sin x

Tactic:
rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]

Premises used: Real.sin_le_one, Real.sin_arcsin, Real.neg_one_le_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -(π / 2) ≤ x
hx₂ : x ≤ π / 2
⊢ arcsin (sin x) = x

Tactic:
arcsin_sin' ⟨hx₁, hx₂⟩

Premises used: And.intro, Real.arcsin_sin'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ StrictMonoOn arcsin (Icc (-1) 1)

Tactic:
(Subtype.strictMono_coe _).comp_strictMonoOn <|
    sinOrderIso.symm.strictMono.strictMonoOn_IccExtend _

Premises used: OrderIso.strictMono, Real.arcsin, StrictMono.strictMonoOn_IccExtend, Real.sinOrderIso, OrderIso.symm, StrictMono.comp_strictMonoOn, Subtype.strictMono_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : -1 ≤ x
hlt : x < y
hy : y ≤ 1
⊢ arcsin x < arcsin y

Tactic:
strictMonoOn_arcsin ⟨hx, hlt.le.trans hy⟩ ⟨hx.trans hlt.le, hy⟩ hlt

Premises used: LT.lt.le, Real.strictMonoOn_arcsin, And.intro, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ Monotone arcsin

Tactic:
(Subtype.mono_coe _).comp <| sinOrderIso.symm.monotone.IccExtend _

Premises used: OrderIso.monotone, Real.arcsin, Monotone.comp, Real.sinOrderIso, Subtype.mono_coe, OrderIso.symm, Monotone.IccExtend
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
h : x ≤ y
⊢ arcsin x ≤ arcsin y

Tactic:
monotone_arcsin h

Premises used: Real.monotone_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ InjOn arcsin (Icc (-1) 1)

Tactic:
strictMonoOn_arcsin.injOn

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

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

Premises used: Set.InjOn.eq_iff, Real.injOn_arcsin, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ Continuous arcsin

Tactic:
continuous_subtype_val.comp sinOrderIso.symm.continuous.Icc_extend'

Premises used: OrderIso.continuous, Real.arcsin, continuous_subtype_val, Continuous.comp, Real.sinOrderIso, OrderIso.symm, Continuous.Icc_extend'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ ContinuousAt arcsin x

Tactic:
continuous_arcsin.continuousAt

Premises used: Real.continuous_arcsin, Continuous.continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
h₁ : sin x = y
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
subst : arcsin (sin x) = x
⊢ arcsin y = x

Tactic:
subst y
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (sin x) = x

Tactic:
injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))

Premises used: Real.sin_arcsin', Real.arcsin_mem_Icc, Real.injOn_sin, Real.sin_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (sin x) = x

Tactic:
exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))

Premises used: Real.sin_arcsin', Real.arcsin_mem_Icc, Real.injOn_sin, Real.sin_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ arcsin 0 = 0

Tactic:
arcsin_eq_of_sin_eq sin_zero ⟨neg_nonpos.2 pi_div_two_pos.le, pi_div_two_pos.le⟩

Premises used: Iff.mpr, Real.pi_div_two_pos, Real.sin_zero, neg_nonpos, LT.lt.le, Real.arcsin_eq_of_sin_eq, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ arcsin 1 = π / 2

Tactic:
arcsin_eq_of_sin_eq sin_pi_div_two <| right_mem_Icc.2 (neg_le_self pi_div_two_pos.le)

Premises used: Iff.mpr, Set.right_mem_Icc, Real.sin_pi_div_two, Real.pi_div_two_pos, LT.lt.le, neg_le_self, Real.arcsin_eq_of_sin_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx : 1 ≤ x
rw : arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = π / 2
rw₁ : arcsin (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc (-1) 1) x) 1 ⋯) : ℝ) = π / 2
rw₂ : arcsin 1 = π / 2
rw₃ rw₄ : π / 2 = π / 2
⊢ arcsin x = π / 2

Tactic:
rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]

Premises used: Subtype.coe_mk, Set.projIcc_of_right_le, Real.arcsin_projIcc, Real.arcsin_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
rw : -sin (π / 2) = -1
rw₁ rw₂ : Eq (α := ℝ) (-1) (-1)
⊢ sin (-(π / 2)) = -1

Tactic:
rw [sin_neg, sin_pi_div_two]

Premises used: Real.sin_pi_div_two, Real.sin_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx : x ≤ -1
rw : arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = -(π / 2)
rw₁ : arcsin (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc (-1) 1) x) (-1) ⋯) : ℝ) = -(π / 2)
rw₂ : arcsin (-1) = -(π / 2)
rw₃ rw₄ : -(π / 2) = -(π / 2)
⊢ arcsin x = -(π / 2)

Tactic:
rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]

Premises used: Subtype.coe_mk, Real.arcsin_neg_one, Real.arcsin_projIcc, Set.projIcc_of_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
inl : ∀ (hx₁ : x ≤ -1), arcsin (-x) = -arcsin x
inr : ∀ (hx₁ : -1 ≤ x), arcsin (-x) = -arcsin x
⊢ arcsin (-x) = -arcsin x

Tactic:
rcases le_total x (-1) with hx₁ | hx₁

Premises used: le_total, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : x ≤ -1
inl : arcsin (-x) = - -(π / 2)
inl₁ : arcsin (-x) = π / 2
inl₂ inl₃ : π / 2 = π / 2
⊢ arcsin (-x) = -arcsin x

Tactic:
rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]

Premises used: Iff.mpr, le_neg, neg_neg, Real.arcsin_of_le_neg_one, Real.arcsin_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
inr : ∀ (hx₂ : 1 ≤ x), arcsin (-x) = -arcsin x
inr₁ : ∀ (hx₂ : x ≤ 1), arcsin (-x) = -arcsin x
⊢ arcsin (-x) = -arcsin x

Tactic:
rcases le_total 1 x with hx₂ | hx₂

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
inr : arcsin (-x) = -(π / 2)
inr₁ inr₂ : -(π / 2) = -(π / 2)
⊢ arcsin (-x) = -arcsin x

Tactic:
rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]

Premises used: Real.arcsin_of_le_neg_one, Real.arcsin_of_one_le, neg_le_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x

Tactic:
arcsin_eq_of_sin_eq ?_ ?_

Premises used: Real.arcsin_eq_of_sin_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
inr : sin (-arcsin x) = -x
inr₁ : -arcsin x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (-x) = -arcsin x

Tactic:
refine arcsin_eq_of_sin_eq ?_ ?_

Premises used: Real.arcsin_eq_of_sin_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
inr : -sin (arcsin x) = -x
inr₁ inr₂ : -x = -x
⊢ sin (-arcsin x) = -x

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

Premises used: Real.sin_arcsin, Real.sin_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)

Tactic:
⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩

Premises used: Iff.mpr, neg_le, Set.Mem, Real.arcsin_le_pi_div_two, setOf, Set.Icc, And.intro, neg_le_neg, Real.neg_pi_div_two_le_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)

Tactic:
exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
hy : y ∈ Icc (-(π / 2)) (π / 2)
rw : arcsin x ≤ arcsin (sin y) ↔ x ≤ sin (arcsin (sin y))
rw₁ : x ≤ sin y ↔ x ≤ sin (arcsin (sin y))
rw₂ rw₃ : x ≤ sin y ↔ x ≤ sin y
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]

Premises used: Real.strictMonoOn_arcsin, Real.arcsin_sin', StrictMonoOn.le_iff_le, Real.sin_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
inl : ∀ (hx₁ : x ≤ -1), arcsin x ≤ y ↔ x ≤ sin y
inr : ∀ (hx₁ : -1 ≤ x), arcsin x ≤ y ↔ x ≤ sin y
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
rcases le_total x (-1) with hx₁ | hx₁

Premises used: le_total, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : x ≤ -1
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
simp [arcsin_of_le_neg_one hx₁, hy.1, hx₁.trans (neg_one_le_sin _)]

Premises used: Real.arcsin_of_le_neg_one, And.left, Real.neg_one_le_sin, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
inr : ∀ (hx₂ : 1 < x), arcsin x ≤ y ↔ x ≤ sin y
inr₁ : ∀ (hx₂ : x ≤ 1), arcsin x ≤ y ↔ x ≤ sin y
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
rcases lt_or_ge 1 x with hx₂ | hx₂

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
simp [arcsin_of_one_le hx₂.le, hy.2.not_ge, (sin_le_one y).trans_lt hx₂]

Premises used: Real.sin_le_one, LT.lt.le, Real.arcsin_of_one_le, And.right, LT.lt.not_ge, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
arcsin_le_iff_le_sin ⟨hx₁, hx₂⟩ (mem_Icc_of_Ico hy)

Premises used: Set.mem_Icc_of_Ico, And.intro, Real.arcsin_le_iff_le_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
exact arcsin_le_iff_le_sin ⟨hx₁, hx₂⟩ (mem_Icc_of_Ico hy)

Premises used: Set.mem_Icc_of_Ico, And.intro, Real.arcsin_le_iff_le_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : Membership.mem (γ := Set ℝ) (Icc (-1) 1) y
rw : -arcsin y ≤ -x ↔ sin x ≤ y
rw₁ : arcsin (-y) ≤ -x ↔ sin x ≤ y
rw₂ : -y ≤ sin (-x) ↔ sin x ≤ y
rw₃ : -y ≤ -sin x ↔ sin x ≤ y
rw₄ rw₅ : sin x ≤ y ↔ sin x ≤ y
⊢ x ≤ arcsin y ↔ sin x ≤ y

Tactic:
rw [← neg_le_neg_iff, ← arcsin_neg,
    arcsin_le_iff_le_sin ⟨neg_le_neg hy.2, neg_le.2 hy.1⟩ ⟨neg_le_neg hx.2, neg_le.2 hx.1⟩, sin_neg,
    neg_le_neg_iff]

Premises used: Iff.mpr, neg_le, Real.sin_neg, Real.arcsin_neg, And.right, And.left, And.intro, neg_le_neg, Real.arcsin_le_iff_le_sin, neg_le_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
rw : -arcsin y ≤ -x ↔ sin x ≤ y
rw₁ : arcsin (-y) ≤ -x ↔ sin x ≤ y
rw₂ : -y ≤ sin (-x) ↔ sin x ≤ y
rw₃ : -y ≤ -sin x ↔ sin x ≤ y
rw₄ rw₅ : sin x ≤ y ↔ sin x ≤ y
⊢ x ≤ arcsin y ↔ sin x ≤ y

Tactic:
rw [← neg_le_neg_iff, ← arcsin_neg, arcsin_le_iff_le_sin' ⟨neg_le_neg hx.2, neg_lt.2 hx.1⟩,
    sin_neg, neg_le_neg_iff]

Premises used: Iff.mpr, Real.sin_neg, Real.arcsin_le_iff_le_sin', Real.arcsin_neg, And.right, And.left, And.intro, neg_le_neg, neg_lt, neg_le_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin x < y ↔ x < sin y

Tactic:
not_le.symm.trans <| (not_congr <| le_arcsin_iff_sin_le hy hx).trans not_le

Premises used: not_le, Real.le_arcsin_iff_sin_le, Iff.trans, Iff.symm, not_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ioc (-(π / 2)) (π / 2)
⊢ arcsin x < y ↔ x < sin y

Tactic:
not_le.symm.trans <| (not_congr <| le_arcsin_iff_sin_le' hy).trans not_le

Premises used: not_le, Real.le_arcsin_iff_sin_le', Iff.trans, Iff.symm, not_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : Membership.mem (γ := Set ℝ) (Icc (-1) 1) y
⊢ x < arcsin y ↔ sin x < y

Tactic:
not_le.symm.trans <| (not_congr <| arcsin_le_iff_le_sin hy hx).trans not_le

Premises used: not_le, Iff.trans, Real.arcsin_le_iff_le_sin, Iff.symm, not_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hx : x ∈ Ico (-(π / 2)) (π / 2)
⊢ x < arcsin y ↔ sin x < y

Tactic:
not_le.symm.trans <| (not_congr <| arcsin_le_iff_le_sin' hx).trans not_le

Premises used: not_le, Real.arcsin_le_iff_le_sin', Iff.trans, Iff.symm, not_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
⊢ arcsin x = y ↔ x = sin y

Tactic:
simp only [le_antisymm_iff, arcsin_le_iff_le_sin' (mem_Ico_of_Ioo hy),
    le_arcsin_iff_sin_le' (mem_Ioc_of_Ioo hy)]

Premises used: Set.mem_Ioc_of_Ioo, Real.le_arcsin_iff_sin_le', Real.arcsin_le_iff_le_sin', Set.mem_Ico_of_Ioo, le_antisymm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw rw₁ : 0 ≤ x ↔ 0 ≤ x
⊢ sin 0 ≤ x ↔ 0 ≤ x

Tactic:
rw [sin_zero]

Premises used: Real.sin_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x ≤ 0 ↔ x ≤ 0

Tactic:
neg_nonneg.symm.trans <| arcsin_neg x ▸ arcsin_nonneg.trans neg_nonneg

Premises used: Eq.rec, Real.arcsin_neg, neg_nonneg, Real.arcsin_nonneg, Iff.trans, Iff.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x = 0 ↔ x = 0

Tactic:
simp [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ 0 = arcsin x ↔ x = 0

Tactic:
eq_comm.trans arcsin_eq_zero_iff

Premises used: eq_comm, Real.arcsin_eq_zero_iff, Iff.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ 0 < arcsin x ↔ 0 < x

Tactic:
lt_iff_lt_of_le_iff_le arcsin_nonpos

Premises used: Real.arcsin_nonpos, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x < 0 ↔ x < 0

Tactic:
lt_iff_lt_of_le_iff_le arcsin_nonneg

Premises used: Real.arcsin_nonneg, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw rw₁ : x < 1 ↔ x < 1
⊢ x < sin (π / 2) ↔ x < 1

Tactic:
rw [sin_pi_div_two]

Premises used: Real.sin_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw : -sin (π / 2) < x ↔ -1 < x
rw₁ rw₂ : -1 < x ↔ -1 < x
⊢ sin (-(π / 2)) < x ↔ -1 < x

Tactic:
rw [sin_neg, sin_pi_div_two]

Premises used: Real.sin_pi_div_two, Real.sin_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x = π / 2 ↔ 1 ≤ x

Tactic:
⟨fun h => not_lt.1 fun h' => (arcsin_lt_pi_div_two.2 h').ne h, arcsin_of_one_le⟩

Premises used: Iff.mpr, Real.arcsin_of_one_le, not_lt, Iff.intro, Iff.mp, Real.arcsin_lt_pi_div_two, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ π / 2 = arcsin x ↔ 1 ≤ x

Tactic:
eq_comm.trans arcsin_eq_pi_div_two

Premises used: Real.arcsin_eq_pi_div_two, eq_comm, Iff.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ π / 2 ≤ arcsin x ↔ 1 ≤ x

Tactic:
(arcsin_le_pi_div_two x).ge_iff_eq'.trans pi_div_two_eq_arcsin

Premises used: Real.arcsin_le_pi_div_two, Real.pi_div_two_eq_arcsin, LE.le.ge_iff_eq', Iff.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x = -(π / 2) ↔ x ≤ -1

Tactic:
⟨fun h => not_lt.1 fun h' => (neg_pi_div_two_lt_arcsin.2 h').ne' h, arcsin_of_le_neg_one⟩

Premises used: Iff.mpr, Real.arcsin_of_le_neg_one, LT.lt.ne', Real.neg_pi_div_two_lt_arcsin, not_lt, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ -(π / 2) = arcsin x ↔ x ≤ -1

Tactic:
eq_comm.trans arcsin_eq_neg_pi_div_two

Premises used: eq_comm, Iff.trans, Real.arcsin_eq_neg_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x ≤ -(π / 2) ↔ x ≤ -1

Tactic:
(neg_pi_div_two_le_arcsin x).ge_iff_eq'.trans arcsin_eq_neg_pi_div_two

Premises used: LE.le.ge_iff_eq', Iff.trans, Real.neg_pi_div_two_le_arcsin, Real.arcsin_eq_neg_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
rw : π / 4 ∈ Ioc (-(π / 2)) (π / 2)
⊢ π / 4 ≤ arcsin x ↔ √2 / 2 ≤ x

Tactic:
rw [← sin_pi_div_four, le_arcsin_iff_sin_le']

Premises used: Real.le_arcsin_iff_sin_le', Real.sin_pi_div_four
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ 0 < π

Tactic:
have := pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
this : 0 < π
left : -(π / 2) < π / 4
right : π / 4 ≤ π / 2
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
linarith₆ : π / 4 ≤ -(π / 2) → GT.gt (α := ℝ) 3 0
⊢ -(π / 2) < π / 4

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
linarith₅ : π / 2 < π / 4 → 0 - π + (2 * π - 1 * π) = 0
⊢ π / 4 ≤ π / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ 0 ≤ cos (arcsin x)

Tactic:
cos_nonneg_of_mem_Icc ⟨neg_pi_div_two_le_arcsin _, arcsin_le_pi_div_two _⟩

Premises used: Real.arcsin_le_pi_div_two, Real.cos_nonneg_of_mem_Icc, And.intro, Real.neg_pi_div_two_le_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
pos : ∀ (hx₁ : -1 ≤ x), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
neg : ∀ (hx₁ : ¬-1 ≤ x), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
by_cases hx₁ : -1 ≤ x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ x < -1

Tactic:
rw [not_le] at hx₁

Premises used: not_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : x < -1
neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]

Premises used: Real.sqrt_eq_zero_of_nonpos, Real.cos_pi_div_two, LT.lt.le, Real.arcsin_of_le_neg_one, Real.cos_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
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
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
pos : ∀ (hx₂ : x ≤ 1), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
neg : ∀ (hx₂ : ¬x ≤ 1), cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ cos (arcsin 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
⊢ 1 < x

Tactic:
rw [not_le] at hx₂

Premises used: not_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
⊢ cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]

Premises used: Real.sqrt_eq_zero_of_nonpos, Real.cos_pi_div_two, LT.lt.le, Real.arcsin_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
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
⊢ 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)