obtain ⟨x₁, Hx₁⟩ : ∃ x : ℕ, (x : ℤ) = 2 * δ - i₁ - i₂ :=
  ⟨2 * δ - i₁ -i₂, by rw [Nat.sub_sub, Int.sub_sub]; norm_cast⟩
case intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
⊢ a + b ≤ δ
case intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
⊢ a + b ≤ δ