internlm/Lean-Github huggingface dataset:
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  k₁' * I.a₁ * I.b₁ + k₂ * I.a₂ * I.b₁ + (k₁' * I.a₁ * I.b₂ + k₂ * I.a₂ * I.b₂) ≤
    k₁' * I.b₁ * I.a₁ + k₂ * I.b₂ * I.a₁ + (k₁' * I.b₁ * I.a₂ + k₂ * I.b₂ * I.a₂)
⊢ k₂ ≤ k₁'
Tactic:
have rel := I.rel
Proof state after:
case 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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  k₁' * I.a₁ * I.b₁ + k₂ * I.a₂ * I.b₁ + (k₁' * I.a₁ * I.b₂ + k₂ * I.a₂ * I.b₂) ≤
    k₁' * I.b₁ * I.a₁ + k₂ * I.b₂ * I.a₁ + (k₁' * I.b₁ * I.a₂ + k₂ * I.b₂ * I.a₂)
rel : I.a₂ * I.b₁ = I.a₁ * I.b₂ + 1
⊢ k₂ ≤ k₁'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  k₁' * I.a₁ * I.b₁ + k₂ * I.a₂ * I.b₁ + (k₁' * I.a₁ * I.b₂ + k₂ * I.a₂ * I.b₂) ≤
    k₁' * I.b₁ * I.a₁ + k₂ * I.b₂ * I.a₁ + (k₁' * I.b₁ * I.a₂ + k₂ * I.b₂ * I.a₂)
rel : I.a₂ * I.b₁ = I.a₁ * I.b₂ + 1
⊢ k₂ ≤ k₁'
Tactic:
zify at h₂ rel ⊢
Proof state after:
case 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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  ↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂) ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂)
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₂ ≤ ↑k₁'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  ↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂) ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂)
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₂ ≤ ↑k₁'
Tactic:
rw [← sub_nonneg] at h₂ ⊢
Proof state after:
case 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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  0 ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂) -
      (↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ 0 ≤ ↑k₁' - ↑k₂
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  0 ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂) -
      (↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ 0 ≤ ↑k₁' - ↑k₂
Tactic:
convert h₂ using 1
Proof state after:
case h.e'_4
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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  0 ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂) -
      (↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₁' - ↑k₂ =
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂) -
      (↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂))
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case h.e'_4
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₂
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
left✝ : b * (left I).a₁ ≤ a * (left I).b₁
h₂ :
  0 ≤
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂) -
      (↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₁' - ↑k₂ =
    ↑k₁' * ↑I.b₁ * ↑I.a₁ + ↑k₂ * ↑I.b₂ * ↑I.a₁ + (↑k₁' * ↑I.b₁ * ↑I.a₂ + ↑k₂ * ↑I.b₂ * ↑I.a₂) -
      (↑k₁' * ↑I.a₁ * ↑I.b₁ + ↑k₂ * ↑I.a₂ * ↑I.b₁ + (↑k₁' * ↑I.a₁ * ↑I.b₂ + ↑k₂ * ↑I.a₂ * ↑I.b₂))
Tactic:
linear_combination (k₂ - k₁') * rel
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case right
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 (right I)
⊢ ∃ k₁ k₂, a = k₁ * (right I).a₁ + k₂ * (right I).a₂ ∧ b = k₁ * (right I).b₁ + k₂ * (right I).b₂
Tactic:
obtain ⟨k₁, k₂', H₁, H₂⟩ := ih (mem_of_mem_right I h)
Proof state after:
case right.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 (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * (right I).a₁ + k₂ * (right I).a₂ ∧ b = k₁ * (right I).b₁ + k₂ * (right I).b₂
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case right.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 (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
⊢ ∃ k₁ k₂, a = k₁ * (right I).a₁ + k₂ * (right I).a₂ ∧ b = k₁ * (right I).b₁ + k₂ * (right I).b₂
Tactic:
simp only [right_a₁, right_a₂, right_b₁, right_b₂]
Proof state after:
case right.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 (right 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₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * I.b₂
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case right.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 (right 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₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * I.b₂
Tactic:
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
Proof state after:
case right.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 (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
k₂ : ℕ
hk : k₂' = k₂ + k₁
⊢ ∃ k₁ k₂, a = k₁ * (I.a₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * I.b₂
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case right.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 (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
k₂ : ℕ
hk : k₂' = k₂ + k₁
⊢ ∃ k₁ k₂, a = k₁ * (I.a₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * I.b₂
Tactic:
rw [hk] at H₁ H₂
Proof state after:
case right.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 (right I)
k₁ k₂' k₂ : ℕ
H₂ : b = k₁ * I.b₁ + (k₂ + k₁) * I.b₂
H₁ : a = k₁ * I.a₁ + (k₂ + k₁) * I.a₂
hk : k₂' = k₂ + k₁
⊢ ∃ k₁ k₂, a = k₁ * (I.a₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * I.b₂
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case right.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 (right I)
k₁ k₂' k₂ : ℕ
H₂ : b = k₁ * I.b₁ + (k₂ + k₁) * I.b₂
H₁ : a = k₁ * I.a₁ + (k₂ + k₁) * I.a₂
hk : k₂' = k₂ + k₁
⊢ ∃ k₁ k₂, a = k₁ * (I.a₁ + I.a₂) + k₂ * I.a₂ ∧ b = k₁ * (I.b₁ + I.b₂) + k₂ * I.b₂
Tactic:
refine ⟨k₁, k₂, ?_, ?_⟩ <;> linarith
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
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 (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
⊢ ∃ k, k₂' = k + k₁
Tactic:
rw [← le_iff_exists_add']
Proof state after:
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 (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
⊢ k₁ ≤ k₂'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
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 (right I)
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
⊢ k₁ ≤ k₂'
Tactic:
obtain ⟨h₁, _⟩ := h
Proof state after:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
h₁ : b * (right I).a₁ ≤ a * (right I).b₁
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
⊢ k₁ ≤ k₂'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
h₁ : b * (right I).a₁ ≤ a * (right I).b₁
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
⊢ k₁ ≤ k₂'
Tactic:
simp only [H₂, right_a₁, mul_add, add_mul, H₁, right_b₁] at h₁
Proof state after:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  k₁ * I.b₁ * I.a₁ + k₂' * I.b₂ * I.a₁ + (k₁ * I.b₁ * I.a₂ + k₂' * I.b₂ * I.a₂) ≤
    k₁ * I.a₁ * I.b₁ + k₂' * I.a₂ * I.b₁ + (k₁ * I.a₁ * I.b₂ + k₂' * I.a₂ * I.b₂)
⊢ k₁ ≤ k₂'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  k₁ * I.b₁ * I.a₁ + k₂' * I.b₂ * I.a₁ + (k₁ * I.b₁ * I.a₂ + k₂' * I.b₂ * I.a₂) ≤
    k₁ * I.a₁ * I.b₁ + k₂' * I.a₂ * I.b₁ + (k₁ * I.a₁ * I.b₂ + k₂' * I.a₂ * I.b₂)
⊢ k₁ ≤ k₂'
Tactic:
have rel := I.rel
Proof state after:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  k₁ * I.b₁ * I.a₁ + k₂' * I.b₂ * I.a₁ + (k₁ * I.b₁ * I.a₂ + k₂' * I.b₂ * I.a₂) ≤
    k₁ * I.a₁ * I.b₁ + k₂' * I.a₂ * I.b₁ + (k₁ * I.a₁ * I.b₂ + k₂' * I.a₂ * I.b₂)
rel : I.a₂ * I.b₁ = I.a₁ * I.b₂ + 1
⊢ k₁ ≤ k₂'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  k₁ * I.b₁ * I.a₁ + k₂' * I.b₂ * I.a₁ + (k₁ * I.b₁ * I.a₂ + k₂' * I.b₂ * I.a₂) ≤
    k₁ * I.a₁ * I.b₁ + k₂' * I.a₂ * I.b₁ + (k₁ * I.a₁ * I.b₂ + k₂' * I.a₂ * I.b₂)
rel : I.a₂ * I.b₁ = I.a₁ * I.b₂ + 1
⊢ k₁ ≤ k₂'
Tactic:
zify at h₁ rel ⊢
Proof state after:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  ↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂) ≤
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂)
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₁ ≤ ↑k₂'
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  ↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂) ≤
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂)
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₁ ≤ ↑k₂'
Tactic:
rw [← sub_nonneg] at h₁ ⊢
Proof state after:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  0 ≤
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂) -
      (↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ 0 ≤ ↑k₂' - ↑k₁
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case 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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  0 ≤
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂) -
      (↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ 0 ≤ ↑k₂' - ↑k₁
Tactic:
convert h₁ using 1
Proof state after:
case h.e'_4
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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  0 ≤
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂) -
      (↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₂' - ↑k₁ =
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂) -
      (↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂))
Theorem: Weight.BasicInterval.exists_of_mem
Proof state before:
case h.e'_4
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₂
k₁ k₂' : ℕ
H₁ : a = k₁ * I.a₁ + k₂' * I.a₂
H₂ : b = k₁ * I.b₁ + k₂' * I.b₂
right✝ : a * (right I).b₂ ≤ b * (right I).a₂
h₁ :
  0 ≤
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂) -
      (↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂))
rel : ↑I.a₂ * ↑I.b₁ = ↑I.a₁ * ↑I.b₂ + 1
⊢ ↑k₂' - ↑k₁ =
    ↑k₁ * ↑I.a₁ * ↑I.b₁ + ↑k₂' * ↑I.a₂ * ↑I.b₁ + (↑k₁ * ↑I.a₁ * ↑I.b₂ + ↑k₂' * ↑I.a₂ * ↑I.b₂) -
      (↑k₁ * ↑I.b₁ * ↑I.a₁ + ↑k₂' * ↑I.b₂ * ↑I.a₁ + (↑k₁ * ↑I.b₁ * ↑I.a₂ + ↑k₂' * ↑I.b₂ * ↑I.a₂))
Tactic:
linear_combination (k₁ - k₂') * rel
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
a b : ℕ
I : BasicInterval
h : mem_interior a b I
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Tactic:
obtain ⟨k₁, k₂, h₁, h₂⟩ := exists_of_mem (mem_of_mem_interior h)
Proof state after:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : mem_interior a b I
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : mem_interior a b I
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Tactic:
simp only [mem_interior] at h
Proof state after:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∃ k₁ k₂, 0 < k₁ ∧ 0 < k₂ ∧ a = k₁ * I.a₁ + k₂ * I.a₂ ∧ b = k₁ * I.b₁ + k₂ * I.b₂
Tactic:
refine ⟨k₁, k₂, Nat.pos_of_ne_zero ?_, Nat.pos_of_ne_zero ?_, h₁, h₂⟩
Proof state after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ ≠ 0

case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₂ ≠ 0
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₁ ≠ 0
Tactic:
rintro rfl
Proof state after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = 0 * I.a₁ + k₂ * I.a₂
h₂ : b = 0 * I.b₁ + k₂ * I.b₂
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = 0 * I.a₁ + k₂ * I.a₂
h₂ : b = 0 * I.b₁ + k₂ * I.b₂
⊢ False
Tactic:
simp only [zero_mul, zero_add] at h₁ h₂
Proof state after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
⊢ False
Tactic:
replace h := h.2
Proof state after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : a * I.b₂ < b * I.a₂
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : a * I.b₂ < b * I.a₂
⊢ False
Tactic:
simp only [h₁, mul_assoc, h₂, mul_comm I.a₂] at h
Proof state after:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : k₂ * (I.b₂ * I.a₂) < k₂ * (I.b₂ * I.a₂)
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_1
a b : ℕ
I : BasicInterval
k₂ : ℕ
h₁ : a = k₂ * I.a₂
h₂ : b = k₂ * I.b₂
h : k₂ * (I.b₂ * I.a₂) < k₂ * (I.b₂ * I.a₂)
⊢ False
Tactic:
exact lt_irrefl _ h
Proof state after:
no goals
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ k₂ : ℕ
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ k₂ ≠ 0
Tactic:
rintro rfl
Proof state after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁ + 0 * I.a₂
h₂ : b = k₁ * I.b₁ + 0 * I.b₂
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁ + 0 * I.a₂
h₂ : b = k₁ * I.b₁ + 0 * I.b₂
⊢ False
Tactic:
simp only [zero_mul, add_zero] at h₁ h₂
Proof state after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
h : b * I.a₁ < a * I.b₁ ∧ a * I.b₂ < b * I.a₂
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
⊢ False
Tactic:
replace h := h.1
Proof state after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : b * I.a₁ < a * I.b₁
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : b * I.a₁ < a * I.b₁
⊢ False
Tactic:
simp only [h₁, mul_assoc, h₂, mul_comm I.a₁] at h
Proof state after:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : k₁ * (I.b₁ * I.a₁) < k₁ * (I.b₁ * I.a₁)
⊢ False
Theorem: Weight.BasicInterval.exists_of_mem_interior
Proof state before:
case intro.intro.intro.refine_2
a b : ℕ
I : BasicInterval
k₁ : ℕ
h₁ : a = k₁ * I.a₁
h₂ : b = k₁ * I.b₁
h : k₁ * (I.b₁ * I.a₁) < k₁ * (I.b₁ * I.a₁)
⊢ False
Tactic:
exact lt_irrefl _ h
Proof state after:
no goals
Theorem: Weight.BasicInterval.feasible_base
Proof state before:
⊢ feasible 1 base
Tactic:
simp [feasible]
Proof state after:
no goals
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
d : ℕ
I : BasicInterval
h : feasible d I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
Tactic:
by_cases h' : I.feasible d.succ
Proof state after:
case pos
d : ℕ
I : BasicInterval
h : feasible d I
h' : feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)

case neg
d : ℕ
I : BasicInterval
h : feasible d I
h' : ¬feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
case pos
d : ℕ
I : BasicInterval
h : feasible d I
h' : feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
Tactic:
exact Or.inl h'
Proof state after:
no goals
Theorem: Weight.BasicInterval.feasible_left_or_right
Proof state before:
case neg
d : ℕ
I : BasicInterval
h : feasible d I
h' : ¬feasible (Nat.succ d) I
⊢ feasible (Nat.succ d) I ∨ feasible (Nat.succ d) (left I) ∧ feasible (Nat.succ d) (right I)
Tactic:
simp only [feasible] at h h' ⊢
Proof state after:
case neg
d : ℕ
I : BasicInterval
h : I.a₁ + I.b₁ ≤ d ∧ I.a₂ + I.b₂ ≤ d ∧ d < I.a₁ + I.a₂ + I.b₁ + I.b₂
h' : ¬(I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂)
⊢ I.a₁ + I.b₁ ≤ Nat.succ d ∧ I.a₂ + I.b₂ ≤ Nat.succ d ∧ Nat.succ d < I.a₁ + I.a₂ + I.b₁ + I.b₂ ∨
    ((left I).a₁ + (left I).b₁ ≤ Nat.succ d ∧
        (left I).a₂ + (left I).b₂ ≤ Nat.succ d ∧ Nat.succ d < (left I).a₁ + (left I).a₂ + (left I).b₁ + (left I).b₂) ∧
      (right I).a₁ + (right I).b₁ ≤ Nat.succ d ∧
        (right I).a₂ + (right I).b₂ ≤ Nat.succ d ∧
          Nat.succ d < (right I).a₁ + (right I).a₂ + (right I).b₁ + (right I).b₂