-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_add_eq_add_pi {x y : ℝ} (h : 1 < x * y) (hx : 0 < x) :
    arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π

Proof state:
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

Result:
no goals

Proof state:
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)) + π

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

Result:
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)) + π

Proof state:
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)

Result:
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)) + π

Proof state:
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]

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_1
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y
⊢ (x + y) / (1 - x * y) = (-x + -y) / (x * y - 1)

Tactic:
rw [show -x + -y = -(x + y) by ring, show x * y - 1 = -(1 - x * y) by ring, neg_div_neg_eq]

Result:
no goals

Proof state:
x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π

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

Result:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π

Proof state:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y
⊢ x * y - 1 = -(1 - x * y)

Tactic:
ring

Result:
no goals

Proof state:
x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ 0 < y

Tactic:
have := mul_pos_iff.mp (zero_lt_one.trans h)

Result:
x y : ℝ
h : 1 < x * y
hx : 0 < x
this : 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0
⊢ 0 < y

Proof state:
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:
convert k.symm using 3

Result:
case h.e'_3.h.e'_5.h.e'_1
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y
⊢ (x + y) / (1 - x * y) = -((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))

Proof state:
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y
⊢ -x + -y = -(x + y)

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_1
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y
⊢ (x + y) / (1 - x * y) = -((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))

Tactic:
field_simp

Result:
case h.e'_3.h.e'_5.h.e'_1
x y : ℝ
h : 1 < x * y
hx : 0 < x
hy : 0 < y
k : arctan (-((x⁻¹ + y⁻¹) / (1 - x⁻¹ * y⁻¹))) + π = arctan x + arctan y
⊢ (x + y) / (1 - x * y) = (-x + -y) / (x * y - 1)