rw [Hx₂]
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : -(↑a * (3 * ↑i₂ - ↑d)) = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑a * (3 * ↑i₂ - ↑d)) = ↑a * ↑x₂
d a b : ℕ
hd : ↑d ≠ 0
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ d
hi₁ : 2 * d < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ d
hab : ↑a = ↑b
x₁ : ℕ
Hx₁ : ↑x₁ = 3 * ↑i₁ + 3 * ↑i₂ - 2 * ↑d
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑d - 3 * ↑i₂
hx₁ : x₁ ≤ d
hx₂ : x₂ ≤ d
hSge : -(↑a * (3 * ↑i₂ - ↑d)) = -(↑b * (2 * ↑d - 3 * ↑i₁ - 3 * ↑i₂))
⊢ -(↑a * (3 * ↑i₂ - ↑d)) = ↑a * (↑d - 3 * ↑i₂)