awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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)
⊢ arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = arcsin x
have rw₃ : Eq (α := ℝ)
  (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 sorry x)) : ℝ)
  (↑(IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type))
        x) :
    ℝ)
Tactic: rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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) :
      ℝ)
⊢ arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = arcsin x
have rw₄ : Eq (α := ℝ)
  (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 sorry x)) : ℝ)
  (↑(((⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) ∘
          projIcc (-1) 1 arcsin._proof_2)
        x) :
    ℝ)
Tactic: rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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) :
      ℝ)
⊢ arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = arcsin x
have rw₅ : Eq (α := ℝ)
  (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 sorry x)) : ℝ)
  (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type))
        (projIcc (-1) 1 arcsin._proof_2 x)) :
    ℝ)
Tactic: rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin (arcsin (sin x)) = sin x
have rw : sin x = sin x
Tactic: rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
h₁ : sin x = y
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin y = x
have subst : arcsin (sin x) = x
Tactic: subst y
Cleared hypotheses: y, h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ arcsin x = π / 2
have rw : arcsin (↑(projIcc (-1) 1 sorry x) : ℝ) = π / 2
Tactic: rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : 1 ≤ x
rw : arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = π / 2
⊢ arcsin x = π / 2
have rw₁ : arcsin (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc (-1) 1) x) 1 sorry) : ℝ) = π / 2
Tactic: rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ arcsin x = π / 2
have rw₂ : arcsin 1 = π / 2
Tactic: rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ arcsin x = π / 2
have rw₃ : π / 2 = π / 2
Tactic: rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
⊢ sin (-(π / 2)) = -1
have rw : -sin (π / 2) = -1
Tactic: rw [sin_neg, sin_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
rw : -sin (π / 2) = -1
⊢ sin (-(π / 2)) = -1
have rw₁ : Eq (α := ℝ) (-1) (-1)
Tactic: rw [sin_neg, sin_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : x ≤ -1
⊢ arcsin x = -(π / 2)
have rw : arcsin (↑(projIcc (-1) 1 sorry x) : ℝ) = -(π / 2)
Tactic: rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx : x ≤ -1
rw : arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = -(π / 2)
⊢ arcsin x = -(π / 2)
have rw₁ : arcsin (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc (-1) 1) x) (-1) sorry) : ℝ) = -(π / 2)
Tactic: rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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)
⊢ arcsin x = -(π / 2)
have rw₂ : arcsin (-1) = -(π / 2)
Tactic: rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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)
⊢ arcsin x = -(π / 2)
have rw₃ : -(π / 2) = -(π / 2)
Tactic: rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ arcsin (-x) = -arcsin x
have inl : ∀ (hx₁ : x ≤ -1), arcsin (-x) = -arcsin x
Tactic: rcases le_total x (-1) with hx₁ | hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
inl : ∀ (hx₁ : x ≤ -1), arcsin (-x) = -arcsin x
⊢ arcsin (-x) = -arcsin x
have inr : ∀ (hx₁ : -1 ≤ x), arcsin (-x) = -arcsin x
Tactic: rcases le_total x (-1) with hx₁ | hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : x ≤ -1
⊢ arcsin (-x) = -arcsin x
have inl : arcsin (-x) = - -(π / 2)
Tactic: rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : x ≤ -1
inl : arcsin (-x) = - -(π / 2)
⊢ arcsin (-x) = -arcsin x
have inl₁ : arcsin (-x) = π / 2
Tactic: rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : x ≤ -1
inl : arcsin (-x) = - -(π / 2)
inl₁ : arcsin (-x) = π / 2
⊢ arcsin (-x) = -arcsin x
have inl₂ : π / 2 = π / 2
Tactic: rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
⊢ arcsin (-x) = -arcsin x
have inr : ∀ (hx₂ : 1 ≤ x), arcsin (-x) = -arcsin x
Tactic: rcases le_total 1 x with hx₂ | hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
inr : ∀ (hx₂ : 1 ≤ x), arcsin (-x) = -arcsin x
⊢ arcsin (-x) = -arcsin x
have inr₁ : ∀ (hx₂ : x ≤ 1), arcsin (-x) = -arcsin x
Tactic: rcases le_total 1 x with hx₂ | hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x
have inr : arcsin (-x) = -(π / 2)
Tactic: rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
inr : arcsin (-x) = -(π / 2)
⊢ arcsin (-x) = -arcsin x
have inr₁ : -(π / 2) = -(π / 2)
Tactic: rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x
have inr : sin (-arcsin x) = -x
Tactic: refine arcsin_eq_of_sin_eq ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
inr : sin (-arcsin x) = -x
⊢ arcsin (-x) = -arcsin x
have inr₁ : -arcsin x ∈ Icc (-(π / 2)) (π / 2)
Tactic: refine arcsin_eq_of_sin_eq ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x
have inr : -sin (arcsin x) = -x
Tactic: rw [sin_neg, sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
inr : -sin (arcsin x) = -x
⊢ sin (-arcsin x) = -x
have inr₁ : -x = -x
Tactic: rw [sin_neg, sin_arcsin hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (-1) 1) x
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y
have rw : arcsin x ≤ arcsin (sin y) ↔ x ≤ sin (arcsin (sin y))
Tactic: rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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))
⊢ arcsin x ≤ y ↔ x ≤ sin y
have rw₁ : x ≤ sin y ↔ x ≤ sin (arcsin (sin y))
Tactic: rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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))
⊢ arcsin x ≤ y ↔ x ≤ sin y
have rw₂ : x ≤ sin y ↔ x ≤ sin y
Tactic: rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y
have inl : ∀ (hx₁ : x ≤ -1), arcsin x ≤ y ↔ x ≤ sin y
Tactic: rcases le_total x (-1) with hx₁ | hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
inl : ∀ (hx₁ : x ≤ -1), arcsin x ≤ y ↔ x ≤ sin y
⊢ arcsin x ≤ y ↔ x ≤ sin y
have inr : ∀ (hx₁ : -1 ≤ x), arcsin x ≤ y ↔ x ≤ sin y
Tactic: rcases le_total x (-1) with hx₁ | hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
⊢ arcsin x ≤ y ↔ x ≤ sin y
have inr : ∀ (hx₂ : 1 < x), arcsin x ≤ y ↔ x ≤ sin y
Tactic: rcases lt_or_ge 1 x with hx₂ | hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
inr : ∀ (hx₂ : 1 < x), arcsin x ≤ y ↔ x ≤ sin y
⊢ arcsin x ≤ y ↔ x ≤ sin y
have inr₁ : ∀ (hx₂ : x ≤ 1), arcsin x ≤ y ↔ x ≤ sin y
Tactic: rcases lt_or_ge 1 x with hx₂ | hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : Membership.mem (γ := Set ℝ) (Icc (-1) 1) y
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw : -arcsin y ≤ -x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : Membership.mem (γ := Set ℝ) (Icc (-1) 1) y
rw : -arcsin y ≤ -x ↔ sin x ≤ y
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₁ : arcsin (-y) ≤ -x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₂ : -y ≤ sin (-x) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₃ : -y ≤ -sin x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₄ : sin x ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw : -arcsin y ≤ -x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
rw : -arcsin y ≤ -x ↔ sin x ≤ y
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₁ : arcsin (-y) ≤ -x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
rw : -arcsin y ≤ -x ↔ sin x ≤ y
rw₁ : arcsin (-y) ≤ -x ↔ sin x ≤ y
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₂ : -y ≤ sin (-x) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₃ : -y ≤ -sin x ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ x ≤ arcsin y ↔ sin x ≤ y
have rw₄ : sin x ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ sin 0 ≤ x ↔ 0 ≤ x
have rw : 0 ≤ x ↔ 0 ≤ x
Tactic: rw [sin_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ x < sin (π / 2) ↔ x < 1
have rw : x < 1 ↔ x < 1
Tactic: rw [sin_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ sin (-(π / 2)) < x ↔ -1 < x
have rw : -sin (π / 2) < x ↔ -1 < x
Tactic: rw [sin_neg, sin_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : -sin (π / 2) < x ↔ -1 < x
⊢ sin (-(π / 2)) < x ↔ -1 < x
have rw₁ : -1 < x ↔ -1 < x
Tactic: rw [sin_neg, sin_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ π / 4 ≤ arcsin x ↔ √2 / 2 ≤ x
have rw : π / 4 ∈ Ioc (-(π / 2)) (π / 2)
Tactic: rw [← sin_pi_div_four, le_arcsin_iff_sin_le']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
have this : 0 < π
Tactic: have := pi_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
have left : -(π / 2) < π / 4
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
left : -(π / 2) < π / 4
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
have right : π / 4 ≤ π / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
⊢ -(π / 2) < π / 4
have linarith : π / 4 ≤ -(π / 2) → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
this : 0 < π
linarith : π / 4 ≤ -(π / 2) → 4 / 4 = 1
⊢ -(π / 2) < π / 4
have linarith₁ : π / 4 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 4 = 4
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
⊢ -(π / 2) < π / 4
have linarith₂ : π / 4 ≤ -(π / 2) → 2 / 2 = 1
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
⊢ -(π / 2) < π / 4
have linarith₃ : π / 4 ≤ -(π / 2) → HMul.hMul (α := ℝ) 2 2 = 4
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
⊢ -(π / 2) < π / 4
have linarith₄ : π / 4 ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
Tactic: linarith