awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
h_eq : (fun (x : ℝ) ↦ sin x / cos x) = tan
⊢ ContinuousOn tan {x : ℝ | cos x ≠ 0}
have rwa : ∀ (this : ContinuousOn tan {x : ℝ | cos x ≠ 0}) (h_eq : (fun (x : ℝ) ↦ sin x / cos x) = tan),
  ContinuousOn tan {x : ℝ | cos x ≠ 0}
Tactic: rwa [h_eq] at this
Cleared hypotheses: this, h_eq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ ContinuousOn tan {x : ℝ | cos x ≠ 0}
have suffices : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
Tactic: suffices ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0} by
    have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
    rwa [h_eq] at this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))
have refine : ∀ x ∈ Ioo (-(π / 2)) (π / 2), Membership.mem (γ := Set ℝ) {x : ℝ | cos x ≠ 0} x
Tactic: refine ContinuousOn.mono continuousOn_tan fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → Membership.mem (γ := Set ℝ) {x : ℝ | cos x ≠ 0} x
have simp : -(π / 2) < x → x < π / 2 → ¬cos x = 0
Tactic: simp only [and_imp, mem_Ioo, mem_setOf_eq, Ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0
have rw : -(π / 2) < x → x < π / 2 → ¬∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
Tactic: rw [cos_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
⊢ False
have inl : ∀ (h : 0 ≤ r), False
Tactic: rcases le_or_gt 0 r with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
inl : ∀ (h : 0 ≤ r), False
⊢ False
have inr : ∀ (h : r < 0), False
Tactic: rcases le_or_gt 0 r with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
⊢ False
have inl : ∀ (hx_lt : ¬π / 2 ≤ x) (r : ℤ) (hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2) (h : 0 ≤ r), False
Tactic: rw [lt_iff_not_ge] at hx_lt
Cleared hypotheses: hx_lt, r, hxr_eq, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
⊢ False
have inl : π / 2 ≤ x
Tactic: refine hx_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
⊢ π / 2 ≤ x
have inl : 1 ≤ HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1
Tactic: rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_left₀ (half_pos pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
⊢ False
have inr : ∀ (hx_gt : ¬x ≤ -(π / 2)) (hx_lt : x < π / 2) (r : ℤ) (hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2)
  (h : r < 0), False
Tactic: rw [lt_iff_not_ge] at hx_gt
Cleared hypotheses: hx_gt, hx_lt, r, hxr_eq, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
⊢ False
have inr : x ≤ -(π / 2)
Tactic: refine hx_gt ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
⊢ x ≤ -(π / 2)
have inr : HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1 ≤ -1
Tactic: rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, neg_mul_eq_neg_mul,
      mul_le_mul_iff_left₀ (half_pos pi_pos)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
⊢ r ≤ -1
have rwa : ∀ (h : r + 1 ≤ 0), r ≤ -1
Tactic: rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
rwa : ∀ (h : r + 1 ≤ 0), r ≤ -1
⊢ r ≤ -1
have rwa₁ : ∀ (h : r ≤ -1), r ≤ -1
Tactic: rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
⊢ HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1 ≤ -1
have hr_le : r ≤ -1
Tactic: have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1 ≤ -1
have inr : (↑r : ℝ) ≤ HSub.hSub (α := ℝ) (-1) 1 / 2
Tactic: rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
inr : (↑r : ℝ) ≤ HSub.hSub (α := ℝ) (-1) 1 / 2
⊢ HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1 ≤ -1
have inr₁ : LT.lt (α := ℝ) 0 2
Tactic: rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ (↑r : ℝ) ≤ HSub.hSub (α := ℝ) (-1) 1 / 2
have inr : LE.le (α := ℝ) (↑r : ℝ) (-1)
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ LE.le (α := ℝ) (↑r : ℝ) (-1)
have inr : ∀ (hxr_eq : x = (↑(2 * r + 1) : ℝ) * π / 2) (h : r < 0) (hr_le : r ≤ Int.negSucc 0), r ≤ Int.negSucc 0
Tactic: assumption_mod_cast
Cleared hypotheses: hxr_eq, h, hr_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
this : -(π / 2) < π / 2
⊢ Tendsto (β := ℝ) (fun (x : (↑(Ioo (-(π / 2)) (π / 2)) : Type)) ↦ tan (↑x : ℝ)) atBot atBot
have rw : Tendsto tan (𝓝[>] (-(π / 2))) atBot
Tactic: rw [tendsto_comp_coe_Ioo_atBot this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
this : -(π / 2) < π / 2
⊢ Tendsto (β := ℝ) (fun (x : (↑(Ioo (-(π / 2)) (π / 2)) : Type)) ↦ tan (↑x : ℝ)) atTop atTop
have rw : Tendsto tan (𝓝[<] (π / 2)) atTop
Tactic: rw [tendsto_comp_coe_Ioo_atTop this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (sin (arctan x)) 2 = HPow.hPow (β := ℕ) x 2 / (1 + HPow.hPow (β := ℕ) x 2)
have rw : HPow.hPow (β := ℕ) (tan (arctan x)) 2 / (1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2) =
  HPow.hPow (β := ℕ) x 2 / (1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← tan_sq_div_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
rw :
  HPow.hPow (β := ℕ) (tan (arctan x)) 2 / (1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2) =
    HPow.hPow (β := ℕ) x 2 / (1 + HPow.hPow (β := ℕ) x 2)
⊢ HPow.hPow (β := ℕ) (sin (arctan x)) 2 = HPow.hPow (β := ℕ) x 2 / (1 + HPow.hPow (β := ℕ) x 2)
have rw₁ : HPow.hPow (β := ℕ) x 2 / (1 + HPow.hPow (β := ℕ) x 2) = HPow.hPow (β := ℕ) x 2 / (1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← tan_sq_div_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (cos (arctan x)) 2 = 1 / (1 + HPow.hPow (β := ℕ) x 2)
have rw : HPow.hPow (β := ℕ) (cos (arctan x)) 2 = (1 + HPow.hPow (β := ℕ) x 2)⁻¹
Tactic: rw [one_div, ← inv_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
rw : HPow.hPow (β := ℕ) (cos (arctan x)) 2 = (1 + HPow.hPow (β := ℕ) x 2)⁻¹
⊢ HPow.hPow (β := ℕ) (cos (arctan x)) 2 = 1 / (1 + HPow.hPow (β := ℕ) x 2)
have rw₁ : (1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2)⁻¹ = (1 + HPow.hPow (β := ℕ) x 2)⁻¹
Tactic: rw [one_div, ← inv_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
rw : HPow.hPow (β := ℕ) (cos (arctan x)) 2 = (1 + HPow.hPow (β := ℕ) x 2)⁻¹
rw₁ : (1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2)⁻¹ = (1 + HPow.hPow (β := ℕ) x 2)⁻¹
⊢ HPow.hPow (β := ℕ) (cos (arctan x)) 2 = 1 / (1 + HPow.hPow (β := ℕ) x 2)
have rw₂ : (1 + HPow.hPow (β := ℕ) x 2)⁻¹ = (1 + HPow.hPow (β := ℕ) x 2)⁻¹
Tactic: rw [one_div, ← inv_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ sin (arctan x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
have rw : tan (arctan x) / √(1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2) = x / √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← tan_div_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
rw : tan (arctan x) / √(1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2) = x / √(1 + HPow.hPow (β := ℕ) x 2)
⊢ sin (arctan x) = x / √(1 + HPow.hPow (β := ℕ) x 2)
have rw₁ : x / √(1 + HPow.hPow (β := ℕ) x 2) = x / √(1 + HPow.hPow (β := ℕ) x 2)
Tactic: rw [← tan_div_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ cos (arctan x) = 1 / √(1 + HPow.hPow (β := ℕ) x 2)
have rw : cos (arctan x) = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
Tactic: rw [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
rw : cos (arctan x) = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
⊢ cos (arctan x) = 1 / √(1 + HPow.hPow (β := ℕ) x 2)
have rw₁ : (√(1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2))⁻¹ = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
Tactic: rw [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
rw : cos (arctan x) = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
rw₁ : (√(1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2))⁻¹ = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
⊢ cos (arctan x) = 1 / √(1 + HPow.hPow (β := ℕ) x 2)
have rw₂ : (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
Tactic: rw [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
⊢ arcsin x = arctan (x / √(1 - HPow.hPow (β := ℕ) x 2))
have hb : ∀ (h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x), 1 - HPow.hPow (β := ℕ) x 2 ≠ 0
Tactic: rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul,
    mul_div_cancel₀, sub_add_cancel, sqrt_one, div_one]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x
hb : ∀ (h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x), 1 - HPow.hPow (β := ℕ) x 2 ≠ 0
⊢ arcsin x = arctan (x / √(1 - HPow.hPow (β := ℕ) x 2))
have hx : ∀ (h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x), 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
Tactic: rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul,
    mul_div_cancel₀, sub_add_cancel, sqrt_one, div_one]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≠ 0
have h₁ : -1 < x ∧ x < 1
Tactic: simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
have h₁ : -1 < x ∧ x < 1
Tactic: simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≠ 0
have nlinarith : 1 - HPow.hPow (β := ℕ) x 2 = 0 → 1 - HPow.hPow (β := ℕ) x 2 - 0 + (0 - (-1 - x) * (x - 1)) = 0
Tactic: nlinarith [h.1, h.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : -1 < x ∧ 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.1, h.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ arctan x = 0 ↔ arctan x = arctan 0
have rw : arctan x = 0 ↔ arctan x = 0
Tactic: rw [arctan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : tan x = y
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ tan (arctan y) = tan x
have rw : y = tan x
Tactic: rw [tan_arctan, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : tan x = y
hx : x ∈ Ioo (-(π / 2)) (π / 2)
rw : y = tan x
⊢ tan (arctan y) = tan x
have rw₁ : y = y
Tactic: rw [tan_arctan, h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)
have left : -(π / 2) < π / 4
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
left : -(π / 2) < π / 4
⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)
have right : π / 4 < π / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ -(π / 2) < π / 4
have linarith : π / 4 ≤ -(π / 2) → 4 / 4 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
linarith : π / 4 ≤ -(π / 2) → 4 / 4 = 1
⊢ -(π / 2) < π / 4
have linarith₁ : π / 4 ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
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 [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
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 [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
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 [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
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
⊢ -(π / 2) < π / 4
have linarith₅ : π / 4 ≤ -(π / 2) → 1 * π - -(2 * π) + 3 * (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
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) → 1 * π - -(2 * π) + 3 * (0 - π) = 0
⊢ -(π / 2) < π / 4
have linarith₆ : π / 4 ≤ -(π / 2) → GT.gt (α := ℝ) 3 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ π / 4 < π / 2
have linarith : π / 2 ≤ π / 4 → 2 / 2 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
linarith : π / 2 ≤ π / 4 → 2 / 2 = 1
⊢ π / 4 < π / 2
have linarith₁ : π / 2 ≤ π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
linarith : π / 2 ≤ π / 4 → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
⊢ π / 4 < π / 2
have linarith₂ : π / 2 ≤ π / 4 → 4 / 4 = 1
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
linarith : π / 2 ≤ π / 4 → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : π / 2 ≤ π / 4 → 4 / 4 = 1
⊢ π / 4 < π / 2
have linarith₃ : π / 2 ≤ π / 4 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
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
⊢ π / 4 < π / 2
have linarith₄ : π / 2 ≤ π / 4 → GT.gt (α := ℝ) 4 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
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
⊢ π / 4 < π / 2
have linarith₅ : π / 2 ≤ π / 4 → 2 * π - 1 * π + (0 - π) = 0
Tactic: linarith [pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ arctan √3 = π / 3
have hx₁ : -(π / 2) < π / 3
Tactic: rw [← tan_pi_div_three, arctan_tan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
hx₁ : -(π / 2) < π / 3
⊢ arctan √3 = π / 3
have hx₂ : π / 3 < π / 2
Tactic: rw [← tan_pi_div_three, arctan_tan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ -(π / 2) < π / 3
have hx₁ : LT.lt (α := ℝ) (-3) 2
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ π / 3 < π / 2
have hx₂ : LT.lt (α := ℝ) 2 3
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ arctan (√3)⁻¹ = π / 6
have hx₁ : -(π / 2) < π / 6
Tactic: rw [inv_eq_one_div, ← tan_pi_div_six, arctan_tan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
hx₁ : -(π / 2) < π / 6
⊢ arctan (√3)⁻¹ = π / 6
have hx₂ : π / 6 < π / 2
Tactic: rw [inv_eq_one_div, ← tan_pi_div_six, arctan_tan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ -(π / 2) < π / 6
have hx₁ : LT.lt (α := ℝ) (-6) 2
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ π / 6 < π / 2
have hx₂ : LT.lt (α := ℝ) 2 6
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
⊢ arctan (-1) = -(π / 4)
have rw : -arctan 1 = -(π / 4)
Tactic: rw [arctan_neg, arctan_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
rw : -arctan 1 = -(π / 4)
⊢ arctan (-1) = -(π / 4)
have rw₁ : -(π / 4) = -(π / 4)
Tactic: rw [arctan_neg, arctan_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ arctan x = arccos (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
have rw : arcsin (x / √(1 + HPow.hPow (β := ℕ) x 2)) = arcsin √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
Tactic: rw [arctan_eq_arcsin, arccos_eq_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 ≤ x
rw : arcsin (x / √(1 + HPow.hPow (β := ℕ) x 2)) = arcsin √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
⊢ arctan x = arccos (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
have rw₁ : 0 ≤ (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
Tactic: rw [arctan_eq_arcsin, arccos_eq_arcsin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + HPow.hPow (β := ℕ) x 2)) = arcsin √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
have e_a : x / √(1 + HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 ≤ x
⊢ x / √(1 + HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
have e_a : ∀ (h : 0 ≤ x), 0 ≤ HPow.hPow (β := ℕ) x 2
Tactic: rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div,
    sqrt_sq h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 ≤ x
e_a : ∀ (h : 0 ≤ x), 0 ≤ HPow.hPow (β := ℕ) x 2
⊢ x / √(1 + HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
have e_a₁ : ∀ (h : 0 ≤ x), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
Tactic: rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div,
    sqrt_sq h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 ≤ x
e_a : ∀ (h : 0 ≤ x), 0 ≤ HPow.hPow (β := ℕ) x 2
e_a₁ : ∀ (h : 0 ≤ x), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
⊢ x / √(1 + HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
have e_a₂ : ∀ (h : 0 ≤ x), 0 ≤ (1 + HPow.hPow (β := ℕ) x 2)⁻¹
Tactic: rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div,
    sqrt_sq h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
⊢ arccos x = arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x)
have rw : arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x) = π / 2 - arcsin x
Tactic: rw [arccos, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
⊢ arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x) = π / 2 - arcsin x
have refine_1 : tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: refine arctan_eq_of_tan_eq ?_ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
refine_1 : tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
⊢ arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x) = π / 2 - arcsin x
have refine_2 : -(π / 2) < π / 2 - arcsin x
Tactic: refine arctan_eq_of_tan_eq ?_ ⟨?_, ?_⟩