awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_2 : -(π / 2) < π / 2 - arcsin x
⊢ arctan (√(1 - HPow.hPow (β := ℕ) x 2) / x) = π / 2 - arcsin x
have refine_3 : π / 2 - arcsin x < π / 2
Tactic: refine arctan_eq_of_tan_eq ?_ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
have refine_1 : ∀ (h : 0 < x), tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
have refine_1₆ : ∀ (h : 0 < x), (tan (arcsin x))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ tan (π / 2 - arcsin x) = √(1 - HPow.hPow (β := ℕ) x 2) / x
have refine_1₇ : ∀ (h : 0 < x), (x / √(1 - HPow.hPow (β := ℕ) x 2))⁻¹ = √(1 - HPow.hPow (β := ℕ) x 2) / x
Tactic: rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x
have linarith : π / 2 - arcsin x ≤ -(π / 2) → 2 / 2 = 1
Tactic: linarith only [arcsin_le_pi_div_two x, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
linarith : π / 2 - arcsin x ≤ -(π / 2) → 2 / 2 = 1
⊢ -(π / 2) < π / 2 - arcsin x
have linarith₁ : π / 2 - arcsin x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith only [arcsin_le_pi_div_two x, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
linarith : π / 2 - arcsin x ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : π / 2 - arcsin x ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ -(π / 2) < π / 2 - arcsin x
have linarith₂ : π / 2 - arcsin x ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
Tactic: linarith only [arcsin_le_pi_div_two x, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ -(π / 2) < π / 2 - arcsin x
have linarith₈ : π / 2 - arcsin x ≤ -(π / 2) → 1 * π - 2 * arcsin x - -(1 * π) + (2 * arcsin x - 1 * π) + (0 - π) = 0
Tactic: linarith only [arcsin_le_pi_div_two x, pi_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2
have linarith : π / 2 ≤ π / 2 - arcsin x → 2 / 2 = 1
Tactic: linarith only [arcsin_pos.2 h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
linarith : π / 2 ≤ π / 2 - arcsin x → 2 / 2 = 1
⊢ π / 2 - arcsin x < π / 2
have linarith₁ : π / 2 ≤ π / 2 - arcsin x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith only [arcsin_pos.2 h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ π / 2 - arcsin x < π / 2
have linarith₄ : π / 2 ≤ π / 2 - arcsin x → GT.gt (α := ℝ) 2 0
Tactic: linarith only [arcsin_pos.2 h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ π / 2 - arcsin x < π / 2
have linarith₅ : π / 2 ≤ π / 2 - arcsin x → 1 * π - (1 * π - 2 * arcsin x) + 2 * (0 - arcsin x) = 0
Tactic: linarith only [arcsin_pos.2 h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = π / 2 - arctan x
have hx₁ : -(π / 2) < π / 2 - arctan x
Tactic: rw [← arctan_tan (x := _ - _), tan_pi_div_two_sub, tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
hx₁ : -(π / 2) < π / 2 - arctan x
⊢ arctan x⁻¹ = π / 2 - arctan x
have hx₂ : π / 2 - arctan x < π / 2
Tactic: rw [← arctan_tan (x := _ - _), tan_pi_div_two_sub, tan_arctan]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2
have hx₂ : arctan 0 < arctan x
Tactic: rw [sub_lt_self_iff, ← arctan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
h : x < 0
⊢ arctan x⁻¹ = -(π / 2) - arctan x
have this : arctan (-x)⁻¹ = π / 2 - arctan (-x)
Tactic: have := arctan_inv_of_pos (neg_pos.mpr h)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : x < 0
this : arctan (-x)⁻¹ = π / 2 - arctan (-x)
⊢ arctan x⁻¹ = -(π / 2) - arctan x
have rwa : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : x < 0
this : arctan (-x)⁻¹ = π / 2 - arctan (-x)
rwa : ∀ (this : arctan (-x⁻¹) = π / 2 - arctan (-x)), arctan x⁻¹ = -(π / 2) - arctan x
⊢ arctan x⁻¹ = -(π / 2) - arctan x
have rwa₁ : ∀ (this : -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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ arctan x⁻¹ = -(π / 2) - arctan x
have rwa₂ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ arctan x⁻¹ = -(π / 2) - arctan x
have rwa₃ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ arctan x⁻¹ = -(π / 2) - arctan x
have rwa₄ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ arctan x⁻¹ = -(π / 2) - arctan x
have rwa₅ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
⊢ False
have lb : -(π / 2) < arctan x
Tactic: obtain ⟨lb, ub⟩ := arctan_mem_Ioo x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -(π / 2) < arctan x
⊢ False
have ub : arctan x < π / 2
Tactic: obtain ⟨lb, ub⟩ := arctan_mem_Ioo x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -(π / 2) < arctan x
ub : arctan x < π / 2
⊢ False
have lb₁ : -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
Cleared hypotheses: lb, ub
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : -1 < HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1
ub : arctan x < π / 2
⊢ False
have ub₁ : HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 < 1
Tactic: rw [h, ← one_mul (π / 2), mul_div_assoc, mul_lt_mul_iff_left₀ (by positivity)] at ub
Cleared hypotheses: ub
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
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
⊢ False
have lb₁ : Int.negSucc 0 < 2 * k + 1
Tactic: norm_cast at lb ub
Cleared hypotheses: lb, ub
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
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
⊢ False
have ub₁ : 2 * k + 1 < 1
Tactic: norm_cast at lb ub
Cleared hypotheses: lb, ub
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x : ℝ
k : ℤ
h : arctan x = (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / 2
lb : Int.negSucc 0 < 2 * k + 1
ub : 2 * k + 1 < 1
⊢ False
have lb₁ : -1 < 2 * k + 1
Tactic: change -1 < _ at lb
Cleared hypotheses: lb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2
have inl : ∀ (hy : y ≤ 0), arctan x + arctan y < π / 2
Tactic: rcases le_or_gt y 0 with hy | hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
inl : ∀ (hy : y ≤ 0), arctan x + arctan y < π / 2
⊢ arctan x + arctan y < π / 2
have inr : ∀ (hy : 0 < y), arctan x + arctan y < π / 2
Tactic: rcases le_or_gt y 0 with hy | hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2
have inl : arctan x + arctan y < π / 2 + arctan 0
Tactic: rw [← add_zero (π / 2), ← arctan_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ arctan x + arctan y < π / 2
have h₁ : x < y⁻¹
Tactic: rw [← lt_div_iff₀ hy, ← inv_eq_one_div] at h
Cleared hypotheses: h, hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : x < y⁻¹
hy : 0 < y
⊢ arctan x + arctan y < π / 2
have h₁ : arctan x < arctan y⁻¹
Tactic: replace h : arctan x < arctan y⁻¹ := tanOrderIso.symm.strictMono h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
hy : 0 < y
h : arctan x < arctan y⁻¹
⊢ arctan x + arctan y < π / 2
have inr : ∀ (h : arctan x < π / 2 - arctan y), arctan x + arctan y < π / 2
Tactic: rwa [arctan_inv_of_pos hy, lt_tsub_iff_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
hy : 0 < y
h : arctan x < arctan y⁻¹
inr : ∀ (h : arctan x < π / 2 - arctan y), arctan x + arctan y < π / 2
⊢ arctan x + arctan y < π / 2
have inr₁ : ∀ (h : arctan x + arctan y < π / 2), arctan x + arctan y < π / 2
Tactic: rwa [arctan_inv_of_pos hy, lt_tsub_iff_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))
have rw : arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))
Tactic: rw [← arctan_tan (x := _ + _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
rw : arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))
have hx₁ : -(π / 2) < arctan x + arctan y
Tactic: rw [← arctan_tan (x := _ + _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))
have hx₂ : arctan x + arctan y < π / 2
Tactic: rw [← arctan_tan (x := _ + _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
⊢ arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))
have e_x : tan (arctan x + arctan y) = (x + y) / (1 - x * y)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
| (x + y) / (1 - x * y)
have rw : (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))
Tactic: rw [← tan_arctan x, ← tan_arctan y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
⊢ tan (arctan x + arctan y) = (x + y) / (1 - x * y)
have e_x : tan (arctan x + arctan y) = (tan (arctan x) + tan (arctan y)) / (1 - tan (arctan x) * tan (arctan y))
Tactic: conv_rhs => rw [← tan_arctan x, ← tan_arctan y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x y : ℝ
h : x * y < 1
⊢ -(π / 2) < arctan x + arctan y
have hx₁ : arctan (-x) + arctan (-y) < π / 2
Tactic: rw [neg_lt, neg_add, ← arctan_neg, ← arctan_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : x * y < 1
⊢ arctan (-x) + arctan (-y) < π / 2
have h₁ : -x * -y < 1
Tactic: rw [← neg_mul_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ 0 < y
have this : 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0
Tactic: have := mul_pos_iff.mp (zero_lt_one.trans h)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π
have hy : 0 < y
Tactic: have hy : 0 < y := by
    have := mul_pos_iff.mp (zero_lt_one.trans h)
    simpa [hx, hx.asymm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π
have k : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
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 + arctan y = arctan ((x + y) / (1 - x * y)) + π
have k₁ : 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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : 1 < x * y
hx : x < 0
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
have h₁ : 1 < -x * -y
Tactic: rw [← neg_mul_neg] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
Goal:
x y : ℝ
h : 1 < -x * -y
hx : x < 0
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π
have k : arctan (-x) + arctan (-y) = arctan ((-x + -y) / (1 - -x * -y)) + π
Tactic: have k := arctan_add_eq_add_pi h (neg_pos.mpr hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (hypothesis)
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)) - π
have k₁ : -(arctan (-x) + arctan (-y)) = -(arctan (-((x + y) / (1 - x * y))) + π)
Tactic: rw [show _ / _ = -((x + y) / (1 - x * y)) by ring, ← neg_inj] at k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ x * x < 1
have nlinarith : 1 ≤ x * x → 1 - x * x + (0 - (-1 - x) * (x - 1)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ 2 * arctan x = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2))
have rw : arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2))
Tactic: rw [two_mul, arctan_add (by nlinarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ arctan ((x + x) / (1 - x * x)) = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2))
have e_x : (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 1 < x
⊢ 1 < x * x
have nlinarith : x * x ≤ 1 → 2 * (1 - x) + (x * x - 1) + (0 - (1 - x) * (1 - x)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 1 < x
nlinarith : x * x ≤ 1 → 2 * (1 - x) + (x * x - 1) + (0 - (1 - x) * (1 - x)) = 0
⊢ 1 < x * x
have nlinarith₁ : x * x ≤ 1 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 1 < x
⊢ 0 < x
have linarith : x ≤ 0 → -1 + (1 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 1 < x
⊢ 2 * arctan x = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) + π
have rw : arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) + π
Tactic: rw [two_mul, arctan_add_eq_add_pi (by nlinarith) (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : 1 < x
⊢ arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) + π
have e_a : (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : x < -1
⊢ 1 < x * x
have nlinarith : x * x ≤ 1 → 2 * (x - -1) + (x * x - 1) + (0 - (x - -1) * (x - -1)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : x < -1
nlinarith : x * x ≤ 1 → 2 * (x - -1) + (x * x - 1) + (0 - (x - -1) * (x - -1)) = 0
⊢ 1 < x * x
have nlinarith₁ : x * x ≤ 1 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : x < -1
⊢ x < 0
have linarith : 0 ≤ x → -1 + (x - -1) + (0 - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : x < -1
⊢ 2 * arctan x = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) - π
have rw : arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) - π
Tactic: rw [two_mul, arctan_add_eq_sub_pi (by nlinarith) (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
x : ℝ
h : x < -1
⊢ arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - HPow.hPow (β := ℕ) x 2)) - π
have e_a : (x + x) / (1 - x * x) = 2 * x / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ arctan 2⁻¹ + arctan 3⁻¹ = π / 4
have rw : arctan (HAdd.hAdd (α := ℝ) 2⁻¹ 3⁻¹ / (1 - HMul.hMul (α := ℝ) 2⁻¹ 3⁻¹)) = π / 4
Tactic: rw [arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw : arctan (HAdd.hAdd (α := ℝ) 2⁻¹ 3⁻¹ / (1 - HMul.hMul (α := ℝ) 2⁻¹ 3⁻¹)) = π / 4
⊢ arctan 2⁻¹ + arctan 3⁻¹ = π / 4
have rw₁ : HMul.hMul (α := ℝ) 2⁻¹ 3⁻¹ < 1
Tactic: rw [arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
⊢ 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4
have rw : arctan (HMul.hMul (α := ℝ) 2 2⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 2⁻¹ 2)) =
  arctan (HAdd.hAdd (α := ℝ) 1 7⁻¹ / (1 - HMul.hMul (α := ℝ) 1 7⁻¹))
Tactic: rw [two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
Goal:
rw :
  arctan (HMul.hMul (α := ℝ) 2 2⁻¹ / (1 - HPow.hPow (α := ℝ) (β := ℕ) 2⁻¹ 2)) =
    arctan (HAdd.hAdd (α := ℝ) 1 7⁻¹ / (1 - HMul.hMul (α := ℝ) 1 7⁻¹))
⊢ 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4
have rw₁ : HMul.hMul (α := ℝ) 1 7⁻¹ < 1
Tactic: rw [two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add, arctan_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan (goal)
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
⊢ 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4
have h₁ : LT.lt (α := ℝ) (-1) 2⁻¹
Tactic: rw [two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add, arctan_add]