simp only [left_a₁, left_a₂, left_b₁, left_b₂]
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * (left I).a₁ + k₂ * (left I).a₂ ∧ b = k₁ * (left I).b₁ + k₂ * (left I).b₂
case left.intro.intro.intro
a b : ℕ
I : BasicInterval
ih : mem a b I → ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
h : mem a b (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)