awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
⊢ arctan x⁻¹ + arctan y⁻¹ = arctan ((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))

Tactic:
have k := arctan_add (mul_inv x y ▸ inv_lt_one_of_one_lt₀ h)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : π / 2 - arctan x + (π / 2 - arctan y) = arctan ((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))
⊢ π / 2 - arctan x + (π / 2 - arctan y) = π - (arctan x + arctan y)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan x⁻¹ + arctan y⁻¹ = arctan ((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))
⊢ arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y

Tactic:
rw [arctan_inv_of_pos hx, arctan_inv_of_pos hy, show _ + _ = π - (arctan x + arctan y) by ring,
    sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', sub_eq_add_neg, ← arctan_neg, add_comm] at k

Premises used: sub_eq_add_neg, Real.arctan_neg, add_comm, sub_eq_iff_eq_add, Real.arctan_inv_of_pos, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : x < 0
⊢ 1 < -x * -y

Tactic:
rw [← neg_mul_neg] at h

Premises used: neg_mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : x < 0
h₁ : 1 < -x * -y
⊢ x < 0

Tactic:
rw [← neg_mul_neg] at h

Premises used: neg_mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
⊢ arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π

Tactic:
have k := arctan_add_eq_add_pi h (neg_pos.mpr hx)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
⊢ (-x + -y) / (1 - -x * -y) = -((x + y) / (1 - x * y))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
⊢ -(arctan (-x) + arctan (-y)) = -(arctan (-((x + y) / (1 - x * y))) + π)

Tactic:
rw [show _ / _ = -((x + y) / (1 - x * y)) by ring, ← neg_inj] at k

Premises used: neg_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : -(arctan (-x) + arctan (-y)) = -(arctan (-((x + y) / (1 - x * y))) + π)
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
simp only [arctan_neg, neg_add, neg_neg, ← sub_eq_add_neg _ π] at k

Premises used: Real.pi, sub_eq_add_neg, neg_add, Real.arctan_neg, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
k : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
exact k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
nlinarith : 1 ≤ x * x → 1 - x * x + (0 - (-1 - x) * (x - 1)) = 0
⊢ x * x < 1

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
rw : arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2))
⊢ 2 * arctan x = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2))

Tactic:
rw [two_mul, arctan_add (by nlinarith)]

Premises used: two_mul, Real.arctan_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
e_x : (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)
⊢ arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2))

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 1 < x
nlinarith : x * x ≤ 1 → 2 * (1 - x) + (x * x - 1) + (0 - (1 - x) * (1 - x)) = 0
nlinarith₁ : x * x ≤ 1 → GT.gt (α := ℝ) 2 0
⊢ 1 < x * x

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 1 < x
linarith : x ≤ 0 → -1 + (1 - x) + (x - 0) = 0
⊢ 0 < x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 1 < x
rw : arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) + π
⊢ 2 * arctan x = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) + π

Tactic:
rw [two_mul, arctan_add_eq_add_pi (by nlinarith) (by linarith)]

Premises used: two_mul, Real.arctan_add_eq_add_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 1 < x
e_a : (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)
⊢ arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) + π

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 1 < x
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : x < -1
nlinarith : x * x ≤ 1 → 2 * (x - -1) + (x * x - 1) + (0 - (x - -1) * (x - -1)) = 0
nlinarith₁ : x * x ≤ 1 → GT.gt (α := ℝ) 2 0
⊢ 1 < x * x

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : x < -1
linarith : 0 ≤ x → -1 + (x - -1) + (0 - x) = 0
⊢ x < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : x < -1
rw : arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) - π
⊢ 2 * arctan x = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) - π

Tactic:
rw [two_mul, arctan_add_eq_sub_pi (by nlinarith) (by linarith)]

Premises used: two_mul, Real.arctan_add_eq_sub_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : x < -1
e_a : (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)
⊢ arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) - π

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : x < -1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
rw : arctan (HAdd.hAdd (α := ℝ) 2⁻¹ 3⁻¹ / (1 - HMul.hMul (α := ℝ) 2⁻¹ 3⁻¹)) = π / 4
rw₁ : HMul.hMul (α := ℝ) 2⁻¹ 3⁻¹ < 1
⊢ arctan 2⁻¹ + arctan 3⁻¹ = π / 4

Tactic:
rw [arctan_add]

Premises used: Real.arctan_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ arctan (HAdd.hAdd (α := ℝ) 2⁻¹ 3⁻¹ / (1 - HMul.hMul (α := ℝ) 2⁻¹ 3⁻¹)) = π / 4

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ HMul.hMul (α := ℝ) 2⁻¹ 3⁻¹ < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
rw :
  arctan (HMul.hMul (α := ℝ) 2 2⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 2⁻¹ 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 7⁻¹ / (1 - HMul.hMul (α := ℝ) 1 7⁻¹))
rw₁ : HMul.hMul (α := ℝ) 1 7⁻¹ < 1
h₁ : LT.lt (α := ℝ) (-1) 2⁻¹
h₂ : LT.lt (α := ℝ) 2⁻¹ 1
⊢ 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4

Tactic:
rw [two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add, arctan_add]

Premises used: Real.two_mul_arctan, Real.arctan_one, sub_eq_iff_eq_add, Real.arctan_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ arctan (HMul.hMul (α := ℝ) 2 2⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 2⁻¹ 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 7⁻¹ / (1 - HMul.hMul (α := ℝ) 1 7⁻¹))

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ HMul.hMul (α := ℝ) 1 7⁻¹ < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) (-1) 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
rw :
  arctan
      ((HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) + 7⁻¹) /
        (1 - HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹)) =
    π / 4
rw₁ : HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹ < 1
h₁ : LT.lt (α := ℝ) (-1) 3⁻¹
h₂ : LT.lt (α := ℝ) 3⁻¹ 1
⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4

Tactic:
rw [two_mul_arctan, arctan_add]

Premises used: Real.two_mul_arctan, Real.arctan_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ arctan
      ((HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) + 7⁻¹) /
        (1 - HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹)) =
    π / 4

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ HMul.hMul (α := ℝ) 2 3⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 3⁻¹ 2) * 7⁻¹ < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) (-1) 3⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) 3⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ 4 * arctan 5⁻¹ = 2 * (2 * arctan 5⁻¹)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
rw :
  arctan
      (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
        (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))
rw₁ : HMul.hMul (α := ℝ) 1 239⁻¹ < 1
h₁ : -1 < HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)
h₂ : HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2) < 1
h₃ : LT.lt (α := ℝ) (-1) 5⁻¹
h₄ : LT.lt (α := ℝ) 5⁻¹ 1
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4

Tactic:
rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add]

Premises used: Real.two_mul_arctan, Real.arctan_one, sub_eq_iff_eq_add, Real.arctan_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ arctan
      (2 * (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) /
        (1 - HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)) 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 239⁻¹ / (1 - HMul.hMul (α := ℝ) 1 239⁻¹))

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ HMul.hMul (α := ℝ) 1 239⁻¹ < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ -1 < HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2)

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ HMul.hMul (α := ℝ) 2 5⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 5⁻¹ 2) < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) (-1) 5⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) 5⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ sin (arctan x)

Tactic:
fun x y h ↦
  strictMonoOn_sin (Ioo_subset_Icc_self <| arctan_mem_Ioo x)
    (Ioo_subset_Icc_self <| arctan_mem_Ioo y) (arctan_strictMono h)

Premises used: Set.Ioo_subset_Icc_self, StrictMono, Real.arctan_mem_Ioo, Real.arctan_strictMono, Real.strictMonoOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ 0 < sin (arctan x) ↔ 0 < x

Tactic:
simpa using sin_arctan_strictMono.lt_iff_lt (a := 0)

Premises used: StrictMono.lt_iff_lt, Real.sin_arctan_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ sin (arctan x) < 0 ↔ x < 0

Tactic:
simpa using sin_arctan_strictMono.lt_iff_lt (b := 0)

Premises used: StrictMono.lt_iff_lt, Real.sin_arctan_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ sin (arctan 0) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ 0 ≤ sin (arctan x) ↔ 0 ≤ x

Tactic:
simpa using sin_arctan_strictMono.le_iff_le (a := 0)

Premises used: Real.sin_arctan_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ sin (arctan x) ≤ 0 ↔ x ≤ 0

Tactic:
simpa using sin_arctan_strictMono.le_iff_le (b := 0)

Premises used: Real.sin_arctan_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ Continuous arctan

Tactic:
continuous_subtype_val.comp tanOrderIso.toHomeomorph.continuous_invFun

Premises used: Real.arctan, continuous_subtype_val, Continuous.comp, OrderIso.toHomeomorph, Homeomorph.continuous_invFun, Real.tanOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ ContinuousAt arctan x

Tactic:
continuous_arctan.continuousAt

Premises used: Continuous.continuousAt, Real.continuous_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ (↑tanPartialHomeomorph : ℝ → ℝ) = tan

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ (↑tanPartialHomeomorph.symm : ℝ → ℝ) = arctan

Tactic:
rfl

Premises used: Real.arctan, OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos (↑x : ℂ) ≠ 0

Tactic:
mod_cast h

Premises used: Complex.cos, Real.cos, congrArg, cast, Ne, Complex.ofReal, Nat.cast, Complex.ofReal_cos._simp_1, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Not, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos (↑x : ℂ) ≠ 0

Tactic:
exact mod_cast h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx : cos x = 0
⊢ Complex.cos (↑x : ℂ) = 0

Tactic:
have hx : Complex.cos x = 0 := mod_cast hx
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Complex.tan (↑x : ℂ)‖) (𝓝[≠] x) atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |tan x|) (𝓝[≠] x) atTop

Tactic:
simp only [← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_tan]

Premises used: Complex.norm_real, Real.norm_eq_abs, Complex.ofReal_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Complex.tan (↑x : ℂ)‖) (𝓝[≠] x) atTop

Tactic:
(Complex.tendsto_norm_tan_of_cos_eq_zero hx).comp ?_

Premises used: Complex.tendsto_norm_tan_of_cos_eq_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
refine : Tendsto Complex.ofReal (𝓝[≠] x) (𝓝[≠] (↑x : ℂ))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Complex.tan (↑x : ℂ)‖) (𝓝[≠] x) atTop

Tactic:
refine (Complex.tendsto_norm_tan_of_cos_eq_zero hx).comp ?_

Premises used: Complex.tendsto_norm_tan_of_cos_eq_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
⊢ Tendsto Complex.ofReal (𝓝[≠] x) (𝓝[≠] (↑x : ℂ))

Tactic:
Tendsto.inf Complex.continuous_ofReal.continuousAt ?_

Premises used: nhdsWithin, Continuous.continuousAt, Complex.continuous_ofReal, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
refine : Tendsto Complex.ofReal (𝓟 {x}ᶜ) (𝓟 {(↑x : ℂ)}ᶜ)
⊢ Tendsto Complex.ofReal (𝓝[≠] x) (𝓝[≠] (↑x : ℂ))

Tactic:
refine Tendsto.inf Complex.continuous_ofReal.continuousAt ?_

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
⊢ Tendsto Complex.ofReal (𝓟 {x}ᶜ) (𝓟 {(↑x : ℂ)}ᶜ)

Tactic:
tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1

Premises used: Iff.mpr, mt, Iff.mp, Complex.ofReal_inj, Filter.tendsto_principal_principal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hx_1 : cos x = 0
hx : Complex.cos (↑x : ℂ) = 0
⊢ Tendsto Complex.ofReal (𝓟 {x}ᶜ) (𝓟 {(↑x : ℂ)}ᶜ)

Tactic:
exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1

Premises used: Iff.mpr, Filter.tendsto_principal_principal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
k : ℤ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ |tan x|) (𝓝[≠] ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2)) atTop

Tactic:
tendsto_abs_tan_of_cos_eq_zero <| cos_eq_zero_iff.2 ⟨k, rfl⟩

Premises used: Iff.mpr, Real.cos_eq_zero_iff, Real.tendsto_abs_tan_of_cos_eq_zero, Exists.intro, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩

Premises used: Real.hasDerivAt_tan, HasDerivAt.continuousAt, Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
refine : ∀ (hc : ContinuousAt tan x) (h₀ : cos x = 0), False
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False

Tactic:
not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _
    (hc.norm.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atTop, Real.tendsto_abs_tan_of_cos_eq_zero, ContinuousAt.tendsto, ContinuousAt.norm, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_abs_tan_of_cos_eq_zero h₀) _
    (hc.norm.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atTop, Real.tendsto_abs_tan_of_cos_eq_zero, ContinuousAt.tendsto, ContinuousAt.norm, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ tan x ↔ cos x ≠ 0

Tactic:
⟨fun h => continuousAt_tan.1 h.continuousAt, fun h => (hasDerivAt_tan h).differentiableAt⟩

Premises used: Real.continuousAt_tan, HasDerivAt.differentiableAt, DifferentiableAt.continuousAt, Real.hasDerivAt_tan, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
h : cos x = 0
⊢ ¬DifferentiableAt ℝ tan x

Tactic:
have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = 1 / HPow.hPow (β := ℕ) (cos x) 2

Tactic:
simp [deriv_zero_of_not_differentiableAt this, h, sq]

Premises used: deriv_zero_of_not_differentiableAt, sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
n : WithTop ℕ∞
x : ℝ
⊢ ContDiffAt ℝ n tan x ↔ cos x ≠ 0

Tactic:
⟨fun h => continuousAt_tan.1 h.continuousAt, fun h =>
    (Complex.contDiffAt_tan.2 <| mod_cast h).real_of_complex⟩

Premises used: Iff.mpr, Real.continuousAt_tan, ContDiffAt.real_of_complex, Complex.contDiffAt_tan, Iff.intro, Iff.mp, ContDiffAt.continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
h : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ HasDerivAt tan (1 / HPow.hPow (β := ℕ) (cos x) 2) x

Tactic:
hasDerivAt_tan (cos_pos_of_mem_Ioo h).ne'

Premises used: Real.hasDerivAt_tan, LT.lt.ne', Real.cos_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
h : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ DifferentiableAt ℝ tan x

Tactic:
(hasDerivAt_tan_of_mem_Ioo h).differentiableAt

Premises used: HasDerivAt.differentiableAt, Real.hasDerivAt_tan_of_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
⊢ cos (arctan x) ≠ 0

Tactic:
have A : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
A : cos (arctan x) ≠ 0
⊢ 1 / HPow.hPow (β := ℕ) (cos ((↑tanPartialHomeomorph.symm : ℝ → ℝ) x)) 2 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
A : cos (arctan x) ≠ 0
⊢ HasStrictDerivAt arctan (1 / (1 + HPow.hPow (β := ℕ) x 2)) x

Tactic:
simpa [cos_sq_arctan] using
    tanPartialHomeomorph.hasStrictDerivAt_symm trivial (by simpa) (hasStrictDerivAt_tan A)

Premises used: trivial, Real.tanPartialHomeomorph, Real.hasStrictDerivAt_tan, OpenPartialHomeomorph.hasStrictDerivAt_symm, Real.cos_sq_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
⊢ HasDerivAt arctan (1 / (1 + HPow.hPow (β := ℕ) x 2)) x

Tactic:
(hasStrictDerivAt_arctan x).hasDerivAt

Premises used: Real.hasStrictDerivAt_arctan, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
⊢ HasDerivAt arctan (1 + HPow.hPow (β := ℕ) x 2)⁻¹ x

Tactic:
one_div (1 + x ^ 2) ▸ hasDerivAt_arctan x

Premises used: Eq.rec, HPow.hPow, HAdd.hAdd, one_div, Real.hasDerivAt_arctan, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ arctan x

Tactic:
(hasDerivAt_arctan x).differentiableAt

Premises used: HasDerivAt.differentiableAt, Real.hasDerivAt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
⊢ Differentiable ℝ arctan

Tactic:
differentiableAt_arctan

Premises used: Differentiable, Real.differentiableAt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
⊢ deriv arctan = fun (x : ℝ) ↦ 1 / (1 + HPow.hPow (β := ℕ) x 2)

Tactic:
funext fun x => (hasDerivAt_arctan x).deriv

Premises used: HasDerivAt.deriv, funext, Real.hasDerivAt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
n : WithTop ℕ∞
x : ℝ
this : cos (arctan x) ≠ 0
⊢ 1 / HPow.hPow (β := ℕ) (cos ((↑tanPartialHomeomorph.symm : ℝ → ℝ) x)) 2 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ Real.arctan (f x)) (1 / (1 + HPow.hPow (β := ℕ) (f x) 2) * f') x

Tactic:
(Real.hasStrictDerivAt_arctan (f x)).comp x hf

Premises used: Real.arctan, HasStrictDerivAt.comp, Real.hasStrictDerivAt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℝ) ↦ Real.arctan (f x)) (1 / (1 + HPow.hPow (β := ℕ) (f x) 2) * f') x

Tactic:
(Real.hasDerivAt_arctan (f x)).comp x hf

Premises used: Real.arctan, HasDerivAt.comp, Real.hasDerivAt_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ Real.arctan (f x)) (1 / (1 + HPow.hPow (β := ℕ) (f x) 2) * f') s x

Tactic:
(Real.hasDerivAt_arctan (f x)).comp_hasDerivWithinAt x hf

Premises used: Real.arctan, HasDerivAt.comp_hasDerivWithinAt, Real.hasDerivAt_arctan