awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 y hy ↦ ?_).comp h

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

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

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

Tactic:
push _ ∈ _ at hy ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : x ≤ y
⊢ arccos y ≤ arccos x

Tactic:
antitone_arccos hy

Premises used: Real.antitone_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : x ≤ y
⊢ arccos y ≤ arccos x

Tactic:
exact antitone_arccos hy

Premises used: Real.antitone_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
s : Set X
x : X
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : X) ↦ arcsin (f x)) s x

Tactic:
h.arcsin

Premises used: ContinuousWithinAt, Filter.Tendsto.arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
s : Set X
x : X
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : X) ↦ arccos (f x)) s x

Tactic:
h.arccos

Premises used: ContinuousWithinAt, Filter.Tendsto.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
x : X
h : ContinuousAt f x
⊢ ContinuousAt (Y := ℝ) (fun (x : X) ↦ arcsin (f x)) x

Tactic:
h.arcsin

Premises used: Filter.Tendsto.arcsin, ContinuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
x : X
h : ContinuousAt f x
⊢ ContinuousAt (Y := ℝ) (fun (x : X) ↦ arccos (f x)) x

Tactic:
h.arccos

Premises used: Filter.Tendsto.arccos, ContinuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
s : Set X
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ) (fun (x : X) ↦ arcsin (f x)) s

Tactic:
fun x hx ↦ (h x hx).arcsin

Premises used: ContinuousWithinAt.arcsin, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
s : Set X
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ) (fun (x : X) ↦ arccos (f x)) s

Tactic:
fun x hx ↦ (h x hx).arccos

Premises used: ContinuousWithinAt.arccos, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
h : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (x : X) ↦ arcsin (f x)

Tactic:
continuous_arcsin.comp h

Premises used: Real.continuous_arcsin, Real.arcsin, Continuous.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℝ
h : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (x : X) ↦ arccos (f x)

Tactic:
continuous_arccos.comp h

Premises used: Continuous.comp, Real.continuous_arccos, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
inl : ∀ (h₁ : x < -1), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
inr : ∀ (h₁ : -1 < x), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
rcases h₁.lt_or_gt with h₁ | h₁

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : 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 [h₁]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ 1 - HPow.hPow (β := ℕ) x 2 < 0

Tactic:
have : 1 - x ^ 2 < 0 := by nlinarith [h₁]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
inl : HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
rw [sqrt_eq_zero'.2 this.le, div_zero]

Premises used: Iff.mpr, LT.lt.le, div_zero, Real.sqrt_eq_zero'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
⊢ arcsin =ᶠ[𝓝 x] fun (x : ℝ) ↦ -(π / 2)

Tactic:
have : arcsin =ᶠ[𝓝 x] fun _ => -(π / 2) :=
      (gt_mem_nhds h₁).mono fun y hy => arcsin_of_le_neg_one hy.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this_1 : 1 - HPow.hPow (β := ℕ) x 2 < 0
this : arcsin =ᶠ[𝓝 x] fun (x : ℝ) ↦ -(π / 2)
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩

Premises used: hasStrictDerivAt_const, And.intro, contDiffAt_const, ContDiffAt.congr_of_eventuallyEq, HasStrictDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this_1 : 1 - HPow.hPow (β := ℕ) x 2 < 0
this : arcsin =ᶠ[𝓝 x] fun (x : ℝ) ↦ -(π / 2)
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : -1 < x
inr : ∀ (h₂ : x < 1), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
inr₁ : ∀ (h₂ : 1 < x), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
rcases h₂.lt_or_gt with h₂ | h₂

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
nlinarith : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0 → 1 - HPow.hPow (β := ℕ) x 2 - 0 + (0 - (-1 - x) * (x - 1)) = 0
⊢ 0 < 1 - HPow.hPow (β := ℕ) x 2

Tactic:
nlinarith [h₁, h₂]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ 0 < √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
have : 0 < √(1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < √(1 - HPow.hPow (β := ℕ) x 2)
inr : ∀ (this : 0 < cos (arcsin x)), HasStrictDerivAt arcsin (cos (arcsin x))⁻¹ x ∧ ContDiffAt ℝ ω arcsin x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
simp only [← cos_arcsin, one_div] at this ⊢

Premises used: Real.cos_arcsin, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < cos (arcsin x)
⊢ HasStrictDerivAt arcsin (cos (arcsin x))⁻¹ x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
⟨sinPartialHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
      sinPartialHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _)
        contDiff_sin.contDiffAt⟩

Premises used: Real.sinPartialHomeomorph, Real.hasDerivAt_sin, OpenPartialHomeomorph.contDiffAt_symm_deriv, Real.contDiff_sin, LT.lt.ne', And.intro, Real.hasStrictDerivAt_sin, OpenPartialHomeomorph.hasStrictDerivAt_symm, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < cos (arcsin x)
⊢ HasStrictDerivAt arcsin (cos (arcsin x))⁻¹ x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
exact ⟨sinPartialHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
      sinPartialHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _)
        contDiff_sin.contDiffAt⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 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 [h₂]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ 1 - HPow.hPow (β := ℕ) x 2 < 0

Tactic:
have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
inr : HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
rw [sqrt_eq_zero'.2 this.le, div_zero]

Premises used: Iff.mpr, LT.lt.le, div_zero, Real.sqrt_eq_zero'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
⊢ arcsin =ᶠ[𝓝 x] fun (x : ℝ) ↦ π / 2

Tactic:
have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this_1 : 1 - HPow.hPow (β := ℕ) x 2 < 0
this : arcsin =ᶠ[𝓝 x] fun (x : ℝ) ↦ π / 2
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩

Premises used: hasStrictDerivAt_const, And.intro, contDiffAt_const, ContDiffAt.congr_of_eventuallyEq, HasStrictDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this_1 : 1 - HPow.hPow (β := ℕ) x 2 < 0
this : arcsin =ᶠ[𝓝 x] fun (x : ℝ) ↦ π / 2
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x

Tactic:
(deriv_arcsin_aux h₁ h₂).1

Premises used: And.left, Real.deriv_arcsin_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x

Tactic:
(hasStrictDerivAt_arcsin h₁ h₂).hasDerivAt

Premises used: Real.hasStrictDerivAt_arcsin, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
n : ℕ∞ω
⊢ ContDiffAt ℝ n arcsin x

Tactic:
(deriv_arcsin_aux h₁ h₂).2.of_le le_top

Premises used: And.right, le_top, ContDiffAt.of_le, Real.deriv_arcsin_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ -1
inl : ∀ (h : Ne (α := ℝ) 1 (-1)), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)) (Ici 1) 1
inr : ∀ (h' : x ≠ 1), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Ici x) x
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Ici x) x

Tactic:
rcases eq_or_ne x 1 with (rfl | h')

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) 1 (-1)
⊢ HasDerivWithinAt arcsin 0 (Ici 1) 1

Tactic:
(hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _

Premises used: Real.pi, HDiv.hDiv, hasDerivWithinAt_const, HasDerivWithinAt.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) 1 (-1)
h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0
inl : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → arcsin x = π / 2
inl₁ : arcsin 1 = π / 2
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)) (Ici 1) 1

Tactic:
convert! (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _

Premises used: Real.pi, HDiv.hDiv, hasDerivWithinAt_const, HasDerivWithinAt.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) 1 (-1)
⊢ 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0

Tactic:
simp +contextual [arcsin_of_one_le]

Premises used: Real.arcsin_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) 1 (-1)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → arcsin x = π / 2

Tactic:
simp +contextual [arcsin_of_one_le]

Premises used: Real.arcsin_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) 1 (-1)
⊢ arcsin 1 = π / 2

Tactic:
simp +contextual [arcsin_of_one_le]

Premises used: Real.arcsin_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Ici x) x

Tactic:
(hasDerivAt_arcsin h h').hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, Real.hasDerivAt_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Ici x) x

Tactic:
exact (hasDerivAt_arcsin h h').hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, Real.hasDerivAt_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ 1
inl :
  ∀ (h : Ne (α := ℝ) (-1) 1), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)) (Iic (-1)) (-1)
inr : ∀ (h' : ¬x = -1), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Iic x) x
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Iic x) x

Tactic:
rcases em (x = -1) with (rfl | h')

Premises used: em, OfNat.ofNat, Eq, Neg.neg, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) (-1) 1
⊢ HasDerivWithinAt arcsin 0 (Iic (-1)) (-1)

Tactic:
(hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _

Premises used: Real.pi, HDiv.hDiv, hasDerivWithinAt_const, HasDerivWithinAt.congr, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) (-1) 1
h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2) = 0
inl : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Iic (-1)) x → arcsin x = -(π / 2)
inl₁ : arcsin (-1) = -(π / 2)
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)) (Iic (-1)) (-1)

Tactic:
convert! (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _

Premises used: Real.pi, HDiv.hDiv, hasDerivWithinAt_const, HasDerivWithinAt.congr, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) (-1) 1
⊢ 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2) = 0

Tactic:
simp +contextual [arcsin_of_le_neg_one]

Premises used: Real.arcsin_of_le_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) (-1) 1
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Iic (-1)) x → arcsin x = -(π / 2)

Tactic:
simp +contextual [arcsin_of_le_neg_one]

Premises used: Real.arcsin_of_le_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : Ne (α := ℝ) (-1) 1
⊢ arcsin (-1) = -(π / 2)

Tactic:
simp +contextual [arcsin_of_le_neg_one]

Premises used: Real.arcsin_of_le_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Iic x) x

Tactic:
(hasDerivAt_arcsin h' h).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, Real.hasDerivAt_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Iic x) x

Tactic:
exact (hasDerivAt_arcsin h' h).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, Real.hasDerivAt_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1

Tactic:
⟨?_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩

Premises used: HasDerivWithinAt.differentiableWithinAt, Real.hasDerivWithinAt_arcsin_Ici, Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
refine : DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1

Tactic:
refine ⟨?_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Icc (-1) 1) x → (sin ∘ arcsin) x = id x

Tactic:
sin_arcsin'

Premises used: Set.Mem, Real.sin_arcsin', Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Icc (-1) 1) x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ (sin ∘ arcsin) x = id x) x} x}
      a
h₂ h₃ : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Icc (-1) 1) x → (sin ∘ arcsin) x = id x
⊢ sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id

Tactic:
filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'

Premises used: Icc_mem_nhdsGE, Real.sin_arcsin', zero_lt_one, neg_lt_self
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id

Tactic:
have : sin ∘ arcsin =ᶠ[𝓝[≥] (-1 : ℝ)] id := by
    filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
⊢ id (-1) = sin (arcsin (-1))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
⊢ HasDerivWithinAt id (cos (arcsin (-1)) * derivWithin arcsin (Ici (-1)) (-1)) (Ici (-1)) (-1)

Tactic:
have := h.hasDerivWithinAt.sin.congr_of_eventuallyEq this.symm (by simp)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this_1 : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
this : HasDerivWithinAt id (cos (arcsin (-1)) * derivWithin arcsin (Ici (-1)) (-1)) (Ici (-1)) (-1)
⊢ False

Tactic:
simpa using (uniqueDiffOn_Ici _ _ self_mem_Ici).eq_deriv _ this (hasDerivWithinAt_id _ _)

Premises used: UniqueDiffWithinAt.eq_deriv, hasDerivWithinAt_id, uniqueDiffOn_Ici, Set.self_mem_Ici
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1

Tactic:
⟨fun h => ?_, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩

Premises used: HasDerivWithinAt.differentiableWithinAt, Iff.intro, Real.hasDerivWithinAt_arcsin_Iic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
refine : ∀ (h : DifferentiableWithinAt ℝ arcsin (Iic x) x), x ≠ 1
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1

Tactic:
refine ⟨fun h => ?_, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)

Tactic:
rw [← neg_neg x, ← image_neg_Ici] at h

Premises used: Set.image_neg_Ici, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (i : ℝ) ↦ -(arcsin ∘ Neg.neg) i) (Ici (-x)) (-x)

Tactic:
have := (h.comp (-x) differentiableWithinAt_id.fun_neg (mapsTo_image _ _)).fun_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
this : DifferentiableWithinAt ℝ (F := ℝ) (fun (i : ℝ) ↦ -(arcsin ∘ Neg.neg) i) (Ici (-x)) (-x)
⊢ x ≠ 1

Tactic:
simpa [(· ∘ ·), differentiableWithinAt_arcsin_Ici] using this

Premises used: Function.comp, Real.differentiableWithinAt_arcsin_Ici
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ arcsin x ↔ x ≠ -1 ∧ x ≠ 1

Tactic:
⟨fun h => ⟨differentiableWithinAt_arcsin_Ici.1 h.differentiableWithinAt,
      differentiableWithinAt_arcsin_Iic.1 h.differentiableWithinAt⟩,
    fun h => (hasDerivAt_arcsin h.1 h.2).differentiableAt⟩

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt, Real.hasDerivAt_arcsin, Real.differentiableWithinAt_arcsin_Ici, Real.differentiableWithinAt_arcsin_Iic, And.right, And.left, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
h : ∀ (x : ℝ), deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
⊢ deriv arcsin = fun (x : ℝ) ↦ 1 / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
funext x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
pos : ∀ (h : x ≠ -1 ∧ x ≠ 1), deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
neg : ∀ (h : ¬(x ≠ -1 ∧ x ≠ 1)), deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
⊢ deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
by_cases h : x ≠ -1 ∧ x ≠ 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
(hasDerivAt_arcsin h.1 h.2).deriv

Premises used: HasDerivAt.deriv, Real.hasDerivAt_arcsin, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
exact (hasDerivAt_arcsin h.1 h.2).deriv

Premises used: HasDerivAt.deriv, Real.hasDerivAt_arcsin, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
neg : 0 = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
⊢ deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]

Premises used: Real.differentiableAt_arcsin, deriv_zero_of_not_differentiableAt, mt, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ x = -1 ∨ x = 1

Tactic:
simp only [not_and_or, Ne, Classical.not_not] at h

Premises used: Classical.not_not, Ne, not_and_or