x : ℝ
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
x : ℝ
⊢ tan (arcsin x) = x / sqrt (1 - x ^ 2)
rw [tan_eq_sin_div_cos, cos_arcsin]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
x : ℝ
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
by_cases hx₁ : -1 ≤ x
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
swap
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
by_cases hx₂ : x ≤ 1
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
swap
no goals
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
rw [sin_arcsin hx₁ hx₂]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
have h : sqrt (1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
rw [h]
no goals
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
simp
no goals
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ 1 - x ^ 2 ≤ 0
nlinarith
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
have h : sqrt (1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
rw [h]
no goals
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
simp
no goals
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ 1 - x ^ 2 ≤ 0
nlinarith