awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → Angle
s : Set α
x y : α
hc : IsConnected s
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ (↑π : Angle)
hx : x ∈ s
hy : y ∈ s
⊢ (f y).sign = (f x).sign

Tactic:
(hc.image _ (hf.angle_sign_comp hs)).isPreconnected.subsingleton (Set.mem_image_of_mem _ hy)
    (Set.mem_image_of_mem _ hx)

Premises used: IsConnected.image, IsPreconnected.subsingleton, IsConnected.isPreconnected, Real.Angle.sign, ContinuousOn.angle_sign_comp, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
⊢ ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2

Tactic:
h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
h₁ :
  ∀ (a : ℤ),
    (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
h₂ :
  ∀ (a : ℤ),
    (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2
h₃ :
  ∀ (x_1 : ℤ),
    (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x_1 : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x = (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1) * π / 2
h₄ :
  ∀ (x : ℤ),
    (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y = (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) * π / 2
⊢ ((∀ (k : ℤ), (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∀ (l : ℤ), (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2) ∨
    (∃ (k : ℤ), (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2) ∧
      ∃ (l : ℤ), (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑l : ℂ) + 1) * (↑π : ℂ) / 2

Tactic:
convert! h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
a : ℤ
h₁ h₂ h₃ h₄ : ¬x = (↑(2 * a + 1) : ℝ) * π / 2 ↔ ¬x = (↑(2 * a + 1) : ℝ) * π / 2
⊢ (↑x : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
a : ℤ
h₁ h₂ h₃ h₄ : ¬y = (↑(2 * a + 1) : ℝ) * π / 2 ↔ ¬y = (↑(2 * a + 1) : ℝ) * π / 2
⊢ (↑y : ℂ) ≠ (HMul.hMul (α := ℂ) 2 (↑a : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y ≠ (HMul.hMul (α := ℝ) 2 (↑a : ℝ) + 1) * π / 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
x_1 : ℤ
h₁ h₂ h₃ h₄ : x = (↑(2 * x_1 + 1) : ℝ) * π / 2 ↔ x = (↑(2 * x_1 + 1) : ℝ) * π / 2
⊢ (↑x : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x_1 : ℂ) + 1) * (↑π : ℂ) / 2 ↔ x = (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1) * π / 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
x_1 : ℤ
h₁ h₂ h₃ h₄ : y = (↑(2 * x_1 + 1) : ℝ) * π / 2 ↔ y = (↑(2 * x_1 + 1) : ℝ) * π / 2
⊢ (↑y : ℂ) = (HMul.hMul (α := ℂ) 2 (↑x_1 : ℂ) + 1) * (↑π : ℂ) / 2 ↔ y = (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1) * π / 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div,
    Complex.ofReal_mul, Complex.ofReal_tan] using
    @Complex.tan_add (x : ℂ) (y : ℂ) (by convert! h <;> norm_cast)

Premises used: Complex.ofReal_add, Complex.tan_add, Complex.ofReal_div, Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  (∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
    ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
tan_add (Or.inl h)

Premises used: Real.tan_add, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2) ∨
    (∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
      ∃ (l : ℤ), y = (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div,
    Complex.ofReal_mul, Complex.ofReal_tan] using
    @Complex.tan_sub (x : ℂ) (y : ℂ) (by convert! h <;> norm_cast)

Premises used: Complex.ofReal_add, Complex.tan_sub, Complex.ofReal_div, Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h :
  (∀ (k : ℤ), x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2) ∧
    ∀ (l : ℤ), y ≠ (HMul.hMul (α := ℝ) 2 (↑l : ℝ) + 1) * π / 2
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
tan_sub (Or.inl h)

Premises used: Or.inl, Real.tan_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ Complex.tan (2 * (↑x : ℂ)) = 2 * Complex.tan (↑x : ℂ) / (1 - HPow.hPow (β := ℕ) (Complex.tan (↑x : ℂ)) 2)

Tactic:
have := @Complex.tan_two_mul x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
this : Complex.tan (2 * (↑x : ℂ)) = 2 * Complex.tan (↑x : ℂ) / (1 - HPow.hPow (β := ℕ) (Complex.tan (↑x : ℂ)) 2)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  ∀ (this : tan (2 * x) = 2 * tan x / (1 - HPow.hPow (β := ℕ) (tan x) 2)),
    tan (2 * x) = 2 * tan x / (1 - HPow.hPow (β := ℕ) (tan x) 2)
⊢ tan (2 * x) = 2 * tan x / (1 - HPow.hPow (β := ℕ) (tan x) 2)

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
n w : ℤ
h : (↑n : ℝ) * π / 2 = (↑n : ℝ) * π / 2
⊢ ∃ (k : ℤ), (↑k : ℝ) * π / 2 = (↑n : ℝ) * π / 2

Tactic:
use n
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
h : ∀ (x : ℝ), sin x / cos x = tan x
⊢ (fun (x : ℝ) ↦ sin x / cos x) = tan

Tactic:
ext1 x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
x : ℝ
h h₁ : sin x / cos x = sin x / cos x
⊢ sin x / cos x = tan x

Tactic:
rw [tan_eq_sin_div_cos]

Premises used: Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
⊢ (fun (x : ℝ) ↦ sin x / cos x) = tan

Tactic:
have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
h_eq : (fun (x : ℝ) ↦ sin x / cos x) = tan
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : ContinuousOn tan {x : ℝ | cos x ≠ 0}) (h_eq : (fun (x : ℝ) ↦ sin x / cos x) = tan),
    ContinuousOn tan {x : ℝ | cos x ≠ 0}
⊢ ContinuousOn tan {x : ℝ | cos x ≠ 0}

Tactic:
rwa [h_eq] at this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
suffices : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}
⊢ ContinuousOn tan {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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}

Tactic:
continuousOn_sin.div continuousOn_cos fun x => id

Premises used: id, Real.continuousOn_cos, ContinuousOn.div, Real.continuousOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sin x / cos x) {x : ℝ | cos x ≠ 0}

Tactic:
exact continuousOn_sin.div continuousOn_cos fun x => id

Premises used: id, Real.continuousOn_cos, ContinuousOn.div, Real.continuousOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ Continuous (Y := ℝ) fun (x : (↑{x : ℝ | cos x ≠ 0} : Type)) ↦ tan (↑x : ℝ)

Tactic:
continuousOn_iff_continuous_restrict.1 continuousOn_tan

Premises used: continuousOn_iff_continuous_restrict, Iff.mp, Real.continuousOn_tan, Set.restrict, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
ContinuousOn.mono continuousOn_tan fun x => ?_

Premises used: Real.continuousOn_tan, ContinuousOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
refine : ∀ x ∈ Ioo (-(π / 2)) (π / 2), Membership.mem (γ := Set ℝ) {x : ℝ | cos x ≠ 0} x
⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
refine ContinuousOn.mono continuousOn_tan fun x => ?_

Premises used: Real.continuousOn_tan, ContinuousOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
simp : -(π / 2) < x → x < π / 2 → ¬cos x = 0
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → Membership.mem (γ := Set ℝ) {x : ℝ | cos x ≠ 0} x

Tactic:
simp only [and_imp, mem_Ioo, mem_setOf_eq, Ne]

Premises used: Set.mem_Ioo, and_imp, Ne, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
rw : -(π / 2) < x → x < π / 2 → ¬∃ (k : ℤ), x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0

Tactic:
rw [cos_eq_zero_iff]

Premises used: Real.cos_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
inr : ∀ (h : r < 0), False
⊢ False

Tactic:
rcases le_or_gt 0 r with h | h

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
inl : ∀ (hx_lt : ¬π / 2 ≤ x) (r : ℤ) (hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2) (h : 0 ≤ r), False
⊢ False

Tactic:
rw [lt_iff_not_ge] at hx_lt

Premises used: lt_iff_not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
⊢ False

Tactic:
hx_lt ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
inl : π / 2 ≤ x
⊢ False

Tactic:
refine hx_lt ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
inl : 1 ≤ HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1
⊢ π / 2 ≤ x

Tactic:
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_left₀ (half_pos pi_pos)]

Premises used: Real.pi, half_pos, mul_div_assoc, Real.pi_pos, HDiv.hDiv, mul_le_mul_iff_left₀, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬π / 2 ≤ x
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : 0 ≤ r
⊢ 1 ≤ HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
inr :
  ∀ (hx_gt : ¬x ≤ -(π / 2)) (hx_lt : x < π / 2) (r : ℤ) (hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2)
    (h : r < 0), False
⊢ False

Tactic:
rw [lt_iff_not_ge] at hx_gt

Premises used: lt_iff_not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
⊢ False

Tactic:
hx_gt ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
inr : x ≤ -(π / 2)
⊢ False

Tactic:
refine hx_gt ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1) * π / 2
h : r < 0
inr : HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1 ≤ -1
⊢ x ≤ -(π / 2)

Tactic:
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, neg_mul_eq_neg_mul,
      mul_le_mul_iff_left₀ (half_pos pi_pos)]

Premises used: Real.pi, half_pos, mul_div_assoc, Real.pi_pos, HDiv.hDiv, neg_mul_eq_neg_mul, mul_le_mul_iff_left₀, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : r ≤ -1), r ≤ -1
⊢ r ≤ -1

Tactic:
rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h

Premises used: Int.lt_iff_add_one_le, le_neg_iff_add_nonpos_right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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

Tactic:
have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
inr₁ : LT.lt (α := ℝ) 0 2
⊢ HMul.hMul (α := ℝ) 2 (↑r : ℝ) + 1 ≤ -1

Tactic:
rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff₀]

Premises used: mul_comm, le_sub_iff_add_le, le_div_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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 : LE.le (α := ℝ) (↑r : ℝ) (-1)
⊢ (↑r : ℝ) ≤ HSub.hSub (α := ℝ) (-1) 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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 inr₁ inr₂ inr₃ :
  ∀ (hxr_eq : x = (↑(2 * r + 1) : ℝ) * π / 2) (h : r < 0) (hr_le : r ≤ Int.negSucc 0), r ≤ Int.negSucc 0
⊢ LE.le (α := ℝ) (↑r : ℝ) (-1)

Tactic:
assumption_mod_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
⊢ LT.lt (α := ℝ) 0 2

Tactic:
zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
⊢ LT.lt (α := ℝ) 0 2

Tactic:
exact zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : -(π / 2) < π / 2
rw : Tendsto tan (𝓝[>] (-(π / 2))) atBot
⊢ Tendsto (β := ℝ) (fun (x : (↑(Ioo (-(π / 2)) (π / 2)) : Type)) ↦ tan (↑x : ℝ)) atBot atBot

Tactic:
rw [tendsto_comp_coe_Ioo_atBot this]

Premises used: tendsto_comp_coe_Ioo_atBot
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot

Tactic:
tendsto_tan_neg_pi_div_two

Premises used: Real.tendsto_tan_neg_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot

Tactic:
exact tendsto_tan_neg_pi_div_two

Premises used: Real.tendsto_tan_neg_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : -(π / 2) < π / 2
rw : Tendsto tan (𝓝[<] (π / 2)) atTop
⊢ Tendsto (β := ℝ) (fun (x : (↑(Ioo (-(π / 2)) (π / 2)) : Type)) ↦ tan (↑x : ℝ)) atTop atTop

Tactic:
rw [tendsto_comp_coe_Ioo_atTop this]

Premises used: tendsto_comp_coe_Ioo_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop

Tactic:
tendsto_tan_pi_div_two

Premises used: Real.tendsto_tan_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop

Tactic:
exact tendsto_tan_pi_div_two

Premises used: Real.tendsto_tan_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ Function.Surjective tan

Tactic:
fun _ => surjOn_tan.subset_range trivial

Premises used: trivial, Set.Mem, setOf, Set.range, Real.surjOn_tan, Function.Surjective, Set.SurjOn.subset_range
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ tan '' Ioo (-(π / 2)) (π / 2) = univ

Tactic:
univ_subset_iff.1 surjOn_tan

Premises used: Set.univ_subset_iff, Iff.mp, Real.surjOn_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ tan (arctan x) = x

Tactic:
tanOrderIso.apply_symm_apply x

Premises used: Real.arctan, OrderIso.apply_symm_apply, Real.tanOrderIso, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ arctan x ∈ Ioo (-(π / 2)) (π / 2)

Tactic:
Subtype.coe_prop _

Premises used: Subtype.coe_prop, Real.arctan, Set.Mem
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ range arctan = Ioo (-(π / 2)) (π / 2)

Tactic:
((EquivLike.surjective _).range_comp _).trans Subtype.range_coe

Premises used: Real.arctan, Function.Surjective.range_comp, Subtype.range_coe, EquivLike.surjective, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
hx₁ : -(π / 2) < x
hx₂ : x < π / 2
⊢ arctan (tan x) = x

Tactic:
Subtype.ext_iff.1 <| tanOrderIso.symm_apply_apply ⟨x, hx₁, hx₂⟩

Premises used: Real.arctan, Subtype.ext_iff, Subtype.mk, And.intro, Iff.mp, Real.tanOrderIso, OrderIso.symm_apply_apply, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ 0 < cos (arctan x)

Tactic:
cos_pos_of_mem_Ioo <| arctan_mem_Ioo x

Premises used: Real.arctan_mem_Ioo, Real.cos_pos_of_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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)
rw₁ rw₂ : HPow.hPow (β := ℕ) x 2 / (1 + HPow.hPow (β := ℕ) 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)

Tactic:
rw [← tan_sq_div_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]

Premises used: Real.tan_sq_div_one_add_tan_sq, LT.lt.ne', Real.tan_arctan, Real.cos_arctan_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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)⁻¹
rw₂ rw₃ : (1 + HPow.hPow (β := ℕ) x 2)⁻¹ = (1 + HPow.hPow (β := ℕ) x 2)⁻¹
⊢ HPow.hPow (β := ℕ) (cos (arctan x)) 2 = 1 / (1 + HPow.hPow (β := ℕ) x 2)

Tactic:
rw [one_div, ← inv_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]

Premises used: Real.inv_one_add_tan_sq, LT.lt.ne', one_div, Real.tan_arctan, Real.cos_arctan_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
rw : tan (arctan x) / √(1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2) = x / √(1 + HPow.hPow (β := ℕ) x 2)
rw₁ rw₂ : x / √(1 + HPow.hPow (β := ℕ) x 2) = x / √(1 + HPow.hPow (β := ℕ) x 2)
⊢ sin (arctan x) = x / √(1 + HPow.hPow (β := ℕ) x 2)

Tactic:
rw [← tan_div_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]

Premises used: Real.tan_div_sqrt_one_add_tan_sq, Real.tan_arctan, Real.cos_arctan_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
rw : cos (arctan x) = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
rw₁ : (√(1 + HPow.hPow (β := ℕ) (tan (arctan x)) 2))⁻¹ = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
rw₂ rw₃ : (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ = (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
⊢ cos (arctan x) = 1 / √(1 + HPow.hPow (β := ℕ) x 2)

Tactic:
rw [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]

Premises used: Real.inv_sqrt_one_add_tan_sq, one_div, Real.tan_arctan, Real.cos_arctan_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ arctan x < π / 2

Tactic:
(arctan_mem_Ioo x).2

Premises used: Real.arctan_mem_Ioo, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ -(π / 2) < arctan x

Tactic:
(arctan_mem_Ioo x).1

Premises used: Real.arctan_mem_Ioo, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ arctan x = arcsin (x / √(1 + HPow.hPow (β := ℕ) x 2))

Tactic:
Eq.symm <| arcsin_eq_of_sin_eq (sin_arctan x) (mem_Icc_of_Ioo <| arctan_mem_Ioo x)

Premises used: Real.sin_arctan, Real.arctan_mem_Ioo, Real.arcsin_eq_of_sin_eq, Set.mem_Icc_of_Ioo, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
hx : ∀ (h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x), 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
rw_mod_cast : ∀ (h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x), 1 - HPow.hPow (β := ℕ) x 2 ≠ 0
rw_mod_cast₁ : ∀ (h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x), 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
⊢ arcsin x = arctan (x / √(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]

Premises used: Real.arctan_eq_arcsin, Real.sqrt_mul, Real.sq_sqrt, mul_div_cancel₀, div_pow, one_add_div, div_div, Real.sqrt_one, sub_add_cancel, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioo (↑(Int.negSucc 0) : ℝ) 1) x
⊢ -1 < x ∧ x < 1

Tactic:
simp at h