awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : -1 < x ∧ x < 1
nlinarith : 1 - HPow.hPow (β := ℕ) x 2 = 0 → 1 - HPow.hPow (β := ℕ) x 2 - 0 + (0 - (-1 - x) * (x - 1)) = 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≠ 0

Tactic:
nlinarith [h.1, h.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : -1 < x ∧ x < 1
nlinarith : 1 - HPow.hPow (β := ℕ) x 2 < 0 → 1 - HPow.hPow (β := ℕ) x 2 - 0 + (0 - (-1 - x) * (x - 1)) = 0
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) x 2

Tactic:
nlinarith [h.1, h.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ arctan 0 = 0

Tactic:
simp [arctan_eq_arcsin]

Premises used: Real.arctan_eq_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ StrictMono arctan

Tactic:
tanOrderIso.symm.strictMono

Premises used: StrictMono, Real.arctan, OrderIso.strictMono, Function.surjInv, OrderIso.symm, Real.tanOrderIso, Classical.choose
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ Monotone arctan

Tactic:
arctan_strictMono.monotone

Premises used: StrictMono.monotone, Real.arctan_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
⊢ arctan x < arctan y ↔ x < y

Tactic:
arctan_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Real.arctan_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
⊢ arctan x ≤ arctan y ↔ x ≤ y

Tactic:
arctan_strictMono.le_iff_le

Premises used: Real.arctan_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ Function.Injective arctan

Tactic:
arctan_strictMono.injective

Premises used: Real.arctan_strictMono, StrictMono.injective
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
⊢ arctan x = arctan y ↔ x = y

Tactic:
arctan_injective.eq_iff

Premises used: Function.Injective.eq_iff, Real.arctan_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
rw rw₁ : arctan x = 0 ↔ arctan x = 0
⊢ arctan x = 0 ↔ arctan x = arctan 0

Tactic:
rw [arctan_zero]

Premises used: Real.arctan_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ Order.IsSuccPrelimit (π / 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ Order.IsPredPrelimit (-(π / 2))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : tan x = y
hx : x ∈ Ioo (-(π / 2)) (π / 2)
rw : y = tan x
rw₁ rw₂ : y = y
⊢ tan (arctan y) = tan x

Tactic:
rw [tan_arctan, h]

Premises used: Real.tan_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
left : -(π / 2) < π / 4
right : π / 4 < π / 2
⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
linarith₆ : π / 4 ≤ -(π / 2) → GT.gt (α := ℝ) 3 0
⊢ -(π / 2) < π / 4

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
linarith₅ : π / 2 ≤ π / 4 → 2 * π - 1 * π + (0 - π) = 0
⊢ π / 4 < π / 2

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
hx₁ : -(π / 2) < π / 3
hx₂ : π / 3 < π / 2
⊢ arctan √3 = π / 3

Tactic:
rw [← tan_pi_div_three, arctan_tan]

Premises used: Real.tan_pi_div_three, Real.arctan_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
hx₁ : LT.lt (α := ℝ) (-3) 2
⊢ -(π / 2) < π / 3

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) (-3) 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
hx₂ : LT.lt (α := ℝ) 2 3
⊢ π / 3 < π / 2

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) 2 3

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
hx₁ : -(π / 2) < π / 6
hx₂ : π / 6 < π / 2
⊢ arctan (√3)⁻¹ = π / 6

Tactic:
rw [inv_eq_one_div, ← tan_pi_div_six, arctan_tan]

Premises used: inv_eq_one_div, Real.tan_pi_div_six, Real.arctan_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
hx₁ : LT.lt (α := ℝ) (-6) 2
⊢ -(π / 2) < π / 6

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) (-6) 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
hx₂ : LT.lt (α := ℝ) 2 6
⊢ π / 6 < π / 2

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
⊢ LT.lt (α := ℝ) 2 6

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ arctan x = π / 4 ↔ x = 1

Tactic:
arctan_injective.eq_iff' arctan_one

Premises used: Function.Injective.eq_iff', Real.arctan_injective, Real.arctan_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ arctan (-x) = -arctan x

Tactic:
simp [arctan_eq_arcsin, neg_div]

Premises used: Real.arctan_eq_arcsin, neg_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
rw : -arctan 1 = -(π / 4)
rw₁ rw₂ : -(π / 4) = -(π / 4)
⊢ arctan (-1) = -(π / 4)

Tactic:
rw [arctan_neg, arctan_one]

Premises used: Real.arctan_neg, Real.arctan_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ 0 < arctan x ↔ 0 < x

Tactic:
simpa only [arctan_zero] using arctan_lt_arctan_iff (x := 0)

Premises used: Real.arctan_zero, Real.arctan_lt_arctan_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ arctan x < 0 ↔ x < 0

Tactic:
simpa only [arctan_zero] using arctan_lt_arctan_iff (y := 0)

Premises used: Real.arctan_zero, Real.arctan_lt_arctan_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ 0 ≤ arctan x ↔ 0 ≤ x

Tactic:
simpa only [arctan_zero] using arctan_le_arctan_iff (x := 0)

Premises used: Real.arctan_zero, Real.arctan_le_arctan_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
⊢ arctan x ≤ 0 ↔ x ≤ 0

Tactic:
simpa only [arctan_zero] using arctan_le_arctan_iff (y := 0)

Premises used: Real.arctan_zero, Real.arctan_le_arctan_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 ≤ x
rw : arcsin (x / √(1 + HPow.hPow (β := ℕ) x 2)) = arcsin √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
rw₁ : 0 ≤ (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹
⊢ arctan x = arccos (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹

Tactic:
rw [arctan_eq_arcsin, arccos_eq_arcsin]

Premises used: Real.arctan_eq_arcsin, Real.arccos_eq_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹

Tactic:
inv_nonneg.2 (sqrt_nonneg _)

Premises used: Iff.mpr, inv_nonneg, Real.sqrt_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹

Tactic:
exact inv_nonneg.2 (sqrt_nonneg _)

Premises used: Iff.mpr, inv_nonneg, Real.sqrt_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 ≤ x
e_a : x / √(1 + HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)
⊢ arcsin (x / √(1 + HPow.hPow (β := ℕ) x 2)) = arcsin √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
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
e_a₂ : ∀ (h : 0 ≤ x), 0 ≤ (1 + HPow.hPow (β := ℕ) x 2)⁻¹
⊢ x / √(1 + HPow.hPow (β := ℕ) x 2) = √(1 - HPow.hPow (β := ℕ) (√(1 + HPow.hPow (β := ℕ) x 2))⁻¹ 2)

Tactic:
rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div,
    sqrt_sq h]

Premises used: add_sub_cancel_left, Real.sqrt_inv, Real.sq_sqrt, one_div, Real.sqrt_sq, Real.sqrt_div, one_sub_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ HPow.hPow (β := ℕ) x 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 ≤ x
⊢ 1 + HPow.hPow (β := ℕ) x 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
rw : arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x) = π / 2 - arcsin x
⊢ arccos x = arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x)

Tactic:
rw [arccos, eq_comm]

Premises used: eq_comm, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
⊢ arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x) = π / 2 - arcsin x

Tactic:
arctan_eq_of_tan_eq ?_ ⟨?_, ?_⟩

Premises used: Real.arctan_eq_of_tan_eq, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
refine_1 : tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
refine_2 : -(π / 2) < π / 2 - arcsin x
refine_3 : π / 2 - arcsin x < π / 2
⊢ arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x) = π / 2 - arcsin x

Tactic:
refine arctan_eq_of_tan_eq ?_ ⟨?_, ?_⟩

Premises used: Real.arctan_eq_of_tan_eq, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
refine_1 refine_1₁ refine_1₂ refine_1₃ refine_1₄ refine_1₅ :
  ∀ (h : 0 < x), tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
refine_1₆ : ∀ (h : 0 < x), (tan (arcsin x))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
refine_1₇ : ∀ (h : 0 < x), (x / √(1 - HPow.hPow (β := ℕ) x 2))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
⊢ tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x

Tactic:
rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]

Premises used: Real.tan_pi_div_two_sub, inv_div, Real.tan_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
linarith : π / 2 - arcsin x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : π / 2 - arcsin x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 - arcsin x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : π / 2 - arcsin x ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : π / 2 - arcsin x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π / 2 - arcsin x ≤ -(π / 2) → 2 / 2 = 1
linarith₆ : π / 2 - arcsin x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π / 2 - arcsin x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₈ : π / 2 - arcsin x ≤ -(π / 2) → 1 * π - 2 * arcsin x - -(1 * π) + (2 * arcsin x - 1 * π) + (0 - π) = 0
⊢ -(π / 2) < π / 2 - arcsin x

Tactic:
linarith only [arcsin_le_pi_div_two x, pi_pos]

Premises used: Real.arcsin_le_pi_div_two, Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
linarith : π / 2 ≤ π / 2 - arcsin x → 2 / 2 = 1
linarith₁ : π / 2 ≤ π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π / 2 ≤ π / 2 - arcsin x → 2 / 2 = 1
linarith₃ : π / 2 ≤ π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π / 2 ≤ π / 2 - arcsin x → GT.gt (α := ℝ) 2 0
linarith₅ : π / 2 ≤ π / 2 - arcsin x → 1 * π - (1 * π - 2 * arcsin x) + 2 * (0 - arcsin x) = 0
linarith₆ : π / 2 ≤ π / 2 - arcsin x → GT.gt (α := ℝ) 2 0
⊢ π / 2 - arcsin x < π / 2

Tactic:
linarith only [arcsin_pos.2 h]

Premises used: Iff.mpr, Real.arcsin_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
hx₁ : -(π / 2) < π / 2 - arctan x
hx₂ : π / 2 - arctan x < π / 2
⊢ arctan x⁻¹ = π / 2 - arctan x

Tactic:
rw [← arctan_tan (x := _ - _), tan_pi_div_two_sub, tan_arctan]

Premises used: Real.tan_pi_div_two_sub, Real.tan_arctan, Real.arctan_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

Tactic:
simpa using (arctan_lt_pi_div_two x).trans (half_lt_self_iff.mpr pi_pos)

Premises used: Iff.mpr, Real.pi_pos, half_lt_self_iff, LT.lt.trans, Real.arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
hx₂ : arctan 0 < arctan x
⊢ π / 2 - arctan x < π / 2

Tactic:
rw [sub_lt_self_iff, ← arctan_zero]

Premises used: Real.arctan_zero, sub_lt_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
⊢ arctan 0 < arctan x

Tactic:
tanOrderIso.symm.strictMono h

Premises used: Real.arctan, OrderIso.strictMono, OrderIso.symm, Real.tanOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : 0 < x
⊢ arctan 0 < arctan x

Tactic:
exact tanOrderIso.symm.strictMono h

Premises used: OrderIso.strictMono, OrderIso.symm, Real.tanOrderIso
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : x < 0
⊢ arctan (-x)⁻¹ = π / 2 - arctan (-x)

Tactic:
have := arctan_inv_of_pos (neg_pos.mpr h)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
h : x < 0
this : arctan (-x)⁻¹ = π / 2 - arctan (-x)
rwa : ∀ (this : arctan (-x⁻¹) = π / 2 - arctan (-x)), arctan x⁻¹ = -(π / 2) - arctan x
rwa₁ : ∀ (this : -arctan x⁻¹ = π / 2 - arctan (-x)), arctan x⁻¹ = -(π / 2) - arctan x
rwa₂ : ∀ (this : arctan x⁻¹ = -(π / 2 - arctan (-x))), arctan x⁻¹ = -(π / 2) - arctan x
rwa₃ : ∀ (this : arctan x⁻¹ = -(π / 2) - -arctan (-x)), arctan x⁻¹ = -(π / 2) - arctan x
rwa₄ : ∀ (this : arctan x⁻¹ = -(π / 2) - - -arctan x), arctan x⁻¹ = -(π / 2) - arctan x
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (this : arctan x⁻¹ = -(π / 2) - arctan x), arctan x⁻¹ = -(π / 2) - arctan x
⊢ arctan x⁻¹ = -(π / 2) - arctan x

Tactic:
rwa [inv_neg, arctan_neg, neg_eq_iff_eq_neg, neg_sub', arctan_neg, neg_neg] at this

Premises used: inv_neg, Real.arctan_neg, neg_neg, neg_eq_iff_eq_neg, neg_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
by_contra! : ∀ (k : ℤ) (h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2), False
⊢ ∀ (k : ℤ), arctan x ≠ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2

Tactic:
by_contra! ⟨k, h⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
⊢ -(π / 2) < arctan x

Tactic:
obtain ⟨lb, ub⟩ := arctan_mem_Ioo x

Premises used: Real.arctan_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -(π / 2) < arctan x
⊢ arctan x < π / 2

Tactic:
obtain ⟨lb, ub⟩ := arctan_mem_Ioo x

Premises used: Real.arctan_mem_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -1 * (π / 2) < (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (π / 2)
ub : arctan x < π / 2
⊢ 0 < π / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -(π / 2) < arctan x
ub : arctan x < π / 2
⊢ -1 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1

Tactic:
rw [h, neg_eq_neg_one_mul, mul_div_assoc, mul_lt_mul_iff_left₀ (by positivity)] at lb

Premises used: mul_div_assoc, neg_eq_neg_one_mul, mul_lt_mul_iff_left₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -(π / 2) < arctan x
ub : arctan x < π / 2
lb₁ : -1 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
⊢ arctan x < π / 2

Tactic:
rw [h, neg_eq_neg_one_mul, mul_div_assoc, mul_lt_mul_iff_left₀ (by positivity)] at lb

Premises used: mul_div_assoc, neg_eq_neg_one_mul, mul_lt_mul_iff_left₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -1 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
ub : (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (π / 2) < 1 * (π / 2)
⊢ 0 < π / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -1 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
ub : arctan x < π / 2
⊢ HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 < 1

Tactic:
rw [h, ← one_mul (π / 2), mul_div_assoc, mul_lt_mul_iff_left₀ (by positivity)] at ub

Premises used: Real.pi, mul_div_assoc, HDiv.hDiv, OfNat.ofNat, one_mul, mul_lt_mul_iff_left₀
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -1 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
ub : HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 < 1
⊢ Int.negSucc 0 < 2 * k + 1

Tactic:
norm_cast at lb ub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -1 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
ub : HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 < 1
lb₁ : Int.negSucc 0 < 2 * k + 1
⊢ 2 * k + 1 < 1

Tactic:
norm_cast at lb ub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : Int.negSucc 0 < 2 * k + 1
ub : 2 * k + 1 < 1
⊢ -1 < 2 * k + 1

Tactic:
change -1 < _ at lb
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
ub : 2 * k + 1 < 1
lb : -1 < 2 * k + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
inl : ∀ (hy : y ≤ 0), arctan x + arctan y < π / 2
inr : ∀ (hy : 0 < y), arctan x + arctan y < π / 2
⊢ arctan x + arctan y < π / 2

Tactic:
rcases le_or_gt y 0 with hy | hy

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
hy : y ≤ 0
inl : arctan x + arctan y < π / 2 + arctan 0
⊢ arctan x + arctan y < π / 2

Tactic:
rw [← add_zero (π / 2), ← arctan_zero]

Premises used: Real.pi, HDiv.hDiv, Real.arctan_zero, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2 + arctan 0

Tactic:
add_lt_add_of_lt_of_le (arctan_lt_pi_div_two _) (tanOrderIso.symm.monotone hy)

Premises used: OrderIso.monotone, OrderIso.symm, add_lt_add_of_lt_of_le, Real.tanOrderIso, Real.arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2 + arctan 0

Tactic:
exact add_lt_add_of_lt_of_le (arctan_lt_pi_div_two _) (tanOrderIso.symm.monotone hy)

Premises used: OrderIso.monotone, OrderIso.symm, add_lt_add_of_lt_of_le, Real.tanOrderIso, Real.arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ x < y⁻¹

Tactic:
rw [← lt_div_iff₀ hy, ← inv_eq_one_div] at h

Premises used: lt_div_iff₀, inv_eq_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
hy : 0 < y
h₁ : x < y⁻¹
⊢ 0 < y

Tactic:
rw [← lt_div_iff₀ hy, ← inv_eq_one_div] at h

Premises used: lt_div_iff₀, inv_eq_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x < y⁻¹
hy : 0 < y
⊢ arctan x < arctan y⁻¹

Tactic:
replace h : arctan x < arctan y⁻¹ := tanOrderIso.symm.strictMono h
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
hy : 0 < y
h : arctan x < arctan y⁻¹
inr : ∀ (h : arctan x < π / 2 - arctan y), arctan x + arctan y < π / 2
inr₁ inr₂ inr₃ inr₄ : ∀ (h : arctan x + arctan y < π / 2), arctan x + arctan y < π / 2
⊢ arctan x + arctan y < π / 2

Tactic:
rwa [arctan_inv_of_pos hy, lt_tsub_iff_right] at h

Premises used: lt_tsub_iff_right, Real.arctan_inv_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
rw : arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))
hx₁ : -(π / 2) < arctan x + arctan y
hx₂ : arctan x + arctan y < π / 2
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))

Tactic:
rw [← arctan_tan (x := _ + _)]

Premises used: Real.arctan_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
e_x : tan (arctan x + arctan y) = (x + y) / (1 - x * y)
⊢ arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
rw : (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))
| (x + y) / (1 - x * y)

Tactic:
rw [← tan_arctan x, ← tan_arctan y]

Premises used: Real.tan_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
e_x : tan (arctan x + arctan y) = (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))
⊢ tan (arctan x + arctan y) = (x + y) / (1 - x * y)

Tactic:
conv_rhs => rw [← tan_arctan x, ← tan_arctan y]

Premises used: Real.tan_arctan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))

Tactic:
tan_add' ⟨arctan_ne_mul_pi_div_two, arctan_ne_mul_pi_div_two⟩

Premises used: Real.tan_add', And.intro, Real.arctan_ne_mul_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))

Tactic:
exact tan_add' ⟨arctan_ne_mul_pi_div_two, arctan_ne_mul_pi_div_two⟩

Premises used: Real.tan_add', And.intro, Real.arctan_ne_mul_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
hx₁ : arctan (-x) + arctan (-y) < π / 2
⊢ -(π / 2) < arctan x + arctan y

Tactic:
rw [neg_lt, neg_add, ← arctan_neg, ← arctan_neg]

Premises used: neg_add, Real.arctan_neg, neg_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
⊢ -x * -y < 1

Tactic:
rw [← neg_mul_neg] at h

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

Tactic:
arctan_add_arctan_lt_pi_div_two h

Premises used: Real.arctan_add_arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : -x * -y < 1
⊢ arctan (-x) + arctan (-y) < π / 2

Tactic:
exact arctan_add_arctan_lt_pi_div_two h

Premises used: Real.arctan_add_arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
arctan_add_arctan_lt_pi_div_two h

Premises used: Real.arctan_add_arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
exact arctan_add_arctan_lt_pi_div_two h

Premises used: Real.arctan_add_arctan_lt_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0

Tactic:
have := mul_pos_iff.mp (zero_lt_one.trans h)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
this : 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0
⊢ 0 < y

Tactic:
simpa [hx, hx.asymm]

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

Tactic:
have hy : 0 < y := by
    have := mul_pos_iff.mp (zero_lt_one.trans h)
    simpa [hx, hx.asymm]