awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
pos : ∀ (hx₁ : -1 ≤ x), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : ∀ (hx₁ : ¬-1 ≤ x), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₁ : -1 ≤ x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have hx₂ : x < -1
Tactic: rw [not_le] at hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
Tactic: rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos : ∀ (hx₂ : x ≤ 1), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₂ : x ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
pos : ∀ (hx₂ : x ≤ 1), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : ∀ (hx₂ : ¬x ≤ 1), sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases hx₂ : x ≤ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have hx₃ : 1 < x
Tactic: rw [not_le] at hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have neg : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0
Tactic: rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos : sin (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
pos : sin (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos₁ : cos (arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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)
⊢ sin (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2)
have pos₂ : √(1 - HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ arccos x ≤ π / 4 ↔ √2 / 2 ≤ x
have rw : π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
Tactic: rw [arccos, ← pi_div_four_le_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
have mp : π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
mp : π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
have mpr : π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
h : π / 2 - arcsin x ≤ π / 4
⊢ π / 4 ≤ arcsin x
have linarith : arcsin x < π / 4 → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
h : π / 2 - arcsin x ≤ π / 4
linarith : arcsin x < π / 4 → 4 / 4 = 1
⊢ π / 4 ≤ arcsin x
have linarith₁ : arcsin x < π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
h : π / 2 - arcsin x ≤ π / 4
linarith : arcsin x < π / 4 → 4 / 4 = 1
linarith₁ : arcsin x < π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ π / 4 ≤ arcsin x
have linarith₂ : arcsin x < π / 4 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ π / 4 ≤ arcsin x
have linarith₃ : arcsin x < π / 4 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ π / 4 ≤ arcsin x
have linarith₄ : arcsin x < π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ π / 4 ≤ arcsin x
have linarith₈ : arcsin x < π / 4 → 2 * π - 4 * arcsin x - 1 * π + (4 * arcsin x - 1 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
h : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4
have linarith : π / 4 < π / 2 - arcsin x → 4 / 4 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
h : π / 4 ≤ arcsin x
linarith : π / 4 < π / 2 - arcsin x → 4 / 4 = 1
⊢ π / 2 - arcsin x ≤ π / 4
have linarith₁ : π / 4 < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
h : π / 4 ≤ arcsin x
linarith : π / 4 < π / 2 - arcsin x → 4 / 4 = 1
linarith₁ : π / 4 < π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 4 = 4
⊢ π / 2 - arcsin x ≤ π / 4
have linarith₂ : π / 4 < π / 2 - arcsin x → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ π / 2 - arcsin x ≤ π / 4
have linarith₃ : π / 4 < π / 2 - arcsin x → HMul.hMul (α := ℝ) 2 2 = 4
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ π / 2 - arcsin x ≤ π / 4
have linarith₄ : π / 4 < π / 2 - arcsin x → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ π / 2 - arcsin x ≤ π / 4
have linarith₈ : π / 4 < π / 2 - arcsin x → 1 * π - 4 * arcsin x + (1 * π - (2 * π - 4 * arcsin x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ tan (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
have rw : tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
⊢ tan (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
have rw₁ : (tan (arcsin x))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw : tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
rw₁ : (tan (arcsin x))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
⊢ tan (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
have rw₂ : (x / √(1 - HPow.hPow (β := ℕ) x 2))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
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
⊢ tan (arccos x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
have rw₃ : √(1 - HPow.hPow (β := ℕ) x 2) / x = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos √(1 - HPow.hPow (β := ℕ) x 2)
have rw : arccos (cos (arcsin x)) = arcsin x
Tactic: rw [eq_comm, ← cos_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≤] x)
⊢ Tendsto (fun (x : α) ↦ arcsin (f x)) l (𝓝[≤] arcsin x)
have refine : ∀ (y : ℝ) (hy : y ∈ Iic x), arcsin y ∈ Iic (arcsin x)
Tactic: refine ((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
⊢ Tendsto (fun (x : α) ↦ arccos (f x)) l (𝓝[≤] arccos x)
have refine : ∀ (y : ℝ) (hy : y ∈ Ici x), arccos y ∈ Iic (arccos x)
Tactic: refine ((continuous_arccos.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (hypothesis)
Goal:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : y ∈ Ici x
⊢ arccos y ∈ Iic (arccos x)
have hy₁ : x ≤ y
Tactic: push _ ∈ _ at hy ⊢
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have inl : ∀ (h₁ : x < -1), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
Tactic: rcases h₁.lt_or_gt with h₁ | h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
inl : ∀ (h₁ : x < -1), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have inr : ∀ (h₁ : -1 < x), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
Tactic: rcases h₁.lt_or_gt with h₁ | h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ 1 - HPow.hPow (β := ℕ) x 2 < 0
have nlinarith : 0 ≤ 1 - HPow.hPow (β := ℕ) x 2 → 2 * (x - -1) + (0 - (1 - HPow.hPow (β := ℕ) x 2)) + (0 - (x - -1) * (x - -1)) = 0
Tactic: nlinarith [h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
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
⊢ 1 - HPow.hPow (β := ℕ) x 2 < 0
have nlinarith₁ : 0 ≤ 1 - HPow.hPow (β := ℕ) x 2 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith [h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have this : 1 - HPow.hPow (β := ℕ) x 2 < 0
Tactic: have : 1 - x ^ 2 < 0 := by nlinarith [h₁]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have inl : HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
Tactic: rw [sqrt_eq_zero'.2 this.le, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂ : x ≠ 1
h₁ : -1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have inr : ∀ (h₂ : x < 1), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
Tactic: rcases h₂.lt_or_gt with h₂ | h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
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
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have inr₁ : ∀ (h₂ : 1 < x), HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
Tactic: rcases h₂.lt_or_gt with h₂ | h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ 0 < 1 - HPow.hPow (β := ℕ) x 2
have nlinarith : 1 - HPow.hPow (β := ℕ) x 2 ≤ 0 → 1 - HPow.hPow (β := ℕ) x 2 - 0 + (0 - (-1 - x) * (x - 1)) = 0
Tactic: nlinarith [h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have this : 0 < √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: have : 0 < √(1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < √(1 - HPow.hPow (β := ℕ) x 2)
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have inr : ∀ (this : 0 < cos (arcsin x)), HasStrictDerivAt arcsin (cos (arcsin x))⁻¹ x ∧ ContDiffAt ℝ ω arcsin x
Tactic: simp only [← cos_arcsin, one_div] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ 1 - HPow.hPow (β := ℕ) x 2 < 0
have nlinarith : 0 ≤ 1 - HPow.hPow (β := ℕ) x 2 → 0 - (1 - HPow.hPow (β := ℕ) x 2) + (0 - (-1 - x) * (1 - x)) = 0
Tactic: nlinarith [h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have this : 1 - HPow.hPow (β := ℕ) x 2 < 0
Tactic: have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
⊢ HasStrictDerivAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) x ∧ ContDiffAt ℝ ω arcsin x
have inr : HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
Tactic: rw [sqrt_eq_zero'.2 this.le, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h₁_1 : x ≠ -1
h₂_1 : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - HPow.hPow (β := ℕ) x 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Ici x) x
have inl : ∀ (h : Ne (α := ℝ) 1 (-1)), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)) (Ici 1) 1
Tactic: rcases eq_or_ne x 1 with (rfl | h')
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h : x ≠ -1
inl : ∀ (h : Ne (α := ℝ) 1 (-1)), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)) (Ici 1) 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Ici x) x
have inr : ∀ (h' : x ≠ 1), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Ici x) x
Tactic: rcases eq_or_ne x 1 with (rfl | h')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
h : Ne (α := ℝ) 1 (-1)
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)) (Ici 1) 1
have h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0
Tactic: convert! (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
h : Ne (α := ℝ) 1 (-1)
h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)) (Ici 1) 1
have inl : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → arcsin x = π / 2
Tactic: convert! (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
h : Ne (α := ℝ) 1 (-1)
h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) = 0
inl : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → arcsin x = π / 2
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)) (Ici 1) 1
have inl₁ : arcsin 1 = π / 2
Tactic: convert! (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Iic x) x
have inl : ∀ (h : Ne (α := ℝ) (-1) 1), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)) (Iic (-1)) (-1)
Tactic: rcases em (x = -1) with (rfl | h')
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h : x ≠ 1
inl :
  ∀ (h : Ne (α := ℝ) (-1) 1), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)) (Iic (-1)) (-1)
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Iic x) x
have inr : ∀ (h' : ¬x = -1), HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (β := ℕ) x 2)) (Iic x) x
Tactic: rcases em (x = -1) with (rfl | h')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
h : Ne (α := ℝ) (-1) 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)) (Iic (-1)) (-1)
have h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2) = 0
Tactic: convert! (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
h : Ne (α := ℝ) (-1) 1
h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2) = 0
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)) (Iic (-1)) (-1)
have inl : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Iic (-1)) x → arcsin x = -(π / 2)
Tactic: convert! (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
h : Ne (α := ℝ) (-1) 1
h₁ : 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2) = 0
inl : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Iic (-1)) x → arcsin x = -(π / 2)
⊢ HasDerivWithinAt arcsin (1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)) (Iic (-1)) (-1)
have inl₁ : arcsin (-1) = -(π / 2)
Tactic: convert! (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1
have refine : DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1
Tactic: refine ⟨?_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
have 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
Tactic: filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
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
⊢ sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
have h₂ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Icc (-1) 1) a → (sin ∘ arcsin) a = id a
Tactic: filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ False
have this : 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'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[≥] (-1)] id
⊢ False
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1
have refine : ∀ (h : DifferentiableWithinAt ℝ arcsin (Iic x) x), x ≠ 1
Tactic: refine ⟨fun h => ?_, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1
have h₁ : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
Tactic: rw [← neg_neg x, ← image_neg_Ici] at h
Cleared hypotheses: h