have ha : a ≤ x₁
case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : a * x₂ = b * x₁
⊢ a + b ≤ δ
case ha
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : a * x₂ = b * x₁
⊢ a ≤ x₁

case intro.intro.intro.intro.intro.intro.intro.intro
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
x₁ : ℕ
Hx₁ : ↑x₁ = 2 * ↑δ - ↑i₁ - ↑i₂
x₂ : ℕ
Hx₂ : ↑x₂ = ↑i₂ - ↑δ
Hx₂' : 0 < x₂
hx : x₁ + x₂ ≤ δ
hSle : a * x₂ = b * x₁
ha : a ≤ x₁
⊢ a + b ≤ δ