rw [← mul_add, ← mul_assoc, mul_comm 2, mul_assoc] at hi₁
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * (3 * δ) < 3 * i₁ + 3 * i₂
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 3 * (2 * δ) < 3 * (i₁ + i₂)
hi₂ : 3 * i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
⊢ a ≤ δ ∧ b ≤ δ