induction I with
| base       => simp
| left I ih  =>
  obtain ⟨k₁', k₂, H₁, H₂⟩ := ih (mem_of_mem_left I h)
  simp only [left_a₁, left_a₂, left_b₁, left_b₂]
  have ⟨k₁, hk⟩ : ∃ k, k₁' = k + k₂ := by
    rw [← le_iff_exists_add']
    obtain ⟨_, h₂⟩ := h
    simp only [H₁, left_b₂, mul_add, add_mul, H₂, left_a₂] at h₂
    have rel := I.rel
    zify at h₂ rel ⊢
    rw [← sub_nonneg] at h₂ ⊢
    convert h₂ using 1
    linear_combination (k₂ - k₁') * rel
    done
  rw [hk] at H₁ H₂
  refine ⟨k₁, k₂, ?_, ?_⟩ <;> linarith
  done
| right I ih =>
  obtain ⟨k₁, k₂', H₁, H₂⟩ := ih (mem_of_mem_right I h)
  simp only [right_a₁, right_a₂, right_b₁, right_b₂]
  have ⟨k₂, hk⟩ : ∃ k, k₂' = k + k₁ := by
    rw [← le_iff_exists_add']
    obtain ⟨h₁, _⟩ := h
    simp only [H₂, right_a₁, mul_add, add_mul, H₁, right_b₁] at h₁
    have rel := I.rel
    zify at h₁ rel ⊢
    rw [← sub_nonneg] at h₁ ⊢
    convert h₁ using 1
    linear_combination (k₁ - k₂') * rel
    done
  rw [hk] at H₁ H₂
  refine ⟨k₁, k₂, ?_, ?_⟩ <;> linarith
  done
a b : ℕ
I : BasicInterval
h : mem a b I
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
no goals