Theorem: Weight.BasicInterval.exists_of_mem (Weights/BasicInterval.lean)

State before:
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₂
Tactic:
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
State after:
no goals

State before:
case base
a b : ℕ
h : mem a b base
⊢ ∃ k₁ k₂, a = k₁ * base.a₁ + k₂ * base.a₂ ∧ b = k₁ * base.b₁ + k₂ * base.b₂
Tactic:
simp
State after:
no goals

State before:
case left
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₂, a = k₁ * (left I).a₁ + k₂ * (left I).a₂ ∧ b = k₁ * (left I).b₁ + k₂ * (left I).b₂
Tactic:
obtain ⟨k₁', k₂, H₁, H₂⟩ := ih (mem_of_mem_left I h)
State after:
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₂

State before:
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₂
Tactic:
simp only [left_a₁, left_a₂, left_b₁, left_b₂]
State after:
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₂)

State before:
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₂)
Tactic:
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
State after:
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₁ : ℕ
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)

State before:
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₁ : ℕ
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Tactic:
rw [hk] at H₁ H₂
State after:
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₂ k₁ : ℕ
H₂ : b = (k₁ + k₂) * I.b₁ + k₂ * I.b₂
H₁ : a = (k₁ + k₂) * I.a₁ + k₂ * I.a₂
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)

State before:
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₂ k₁ : ℕ
H₂ : b = (k₁ + k₂) * I.b₁ + k₂ * I.b₂
H₁ : a = (k₁ + k₂) * I.a₁ + k₂ * I.a₂
hk : k₁' = k₁ + k₂
⊢ ∃ k₁ k₂, a = k₁ * I.a₁ + k₂ * (I.a₁ + I.a₂) ∧ b = k₁ * I.b₁ + k₂ * (I.b₁ + I.b₂)
Tactic:
refine ⟨k₁, k₂, ?_, ?_⟩ <;> linarith
State after:
no goals

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 (left 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']
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 (left I)
k₁' k₂ : ℕ
H₁ : a = k₁' * I.a₁ + k₂ * I.a₂
H₂ : b = k₁' * I.b₁ + k₂ * I.b₂
⊢ k₂ ≤ k₁'

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 (left 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
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₂ : a * (left I).b₂ ≤ b * (left I).a₂
⊢ k₂ ≤ k₁'

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₂ : a * (left I).b₂ ≤ b * (left I).a₂
⊢ k₂ ≤ k₁'
Tactic:
simp only [H₁, left_b₂, mul_add, add_mul, H₂, left_a₂] at h₂
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₂)
⊢ k₂ ≤ k₁'

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
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₁'

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 ⊢
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₁'

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₂ ⊢
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₂

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
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₂))

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
State after:
no goals

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)
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₂

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₂]
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₂

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
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₂

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₂
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₂

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
State after:
no goals

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']
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₂'

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
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₂'

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₁
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₂'

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
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₂'

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 ⊢
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₂'

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₁ ⊢
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₁

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
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₂))

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
State after:
no goals