Theorem: Weight.dom_of_mem_interior_left (Weights/Dimension2.lean)

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b
Tactic:
obtain ⟨k₁, k₂, hk₁, hk₂, h₁, h₂⟩ := exists_of_mem_interior hm
State after:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b

State before:
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b
Tactic:
apply dom_of_pair_le
State after:
case intro.intro.intro.intro.intro.h
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∀ (a_1 : ↑(testvecs 2 d)),
    0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v a_1) →
      pair' (of_fraction d I.a₁ I.b₁) (v a_1) ≤ pair' (of_fraction d a b) (v a_1)

State before:
case intro.intro.intro.intro.intro.h
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
⊢ ∀ (a_1 : ↑(testvecs 2 d)),
    0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v a_1) →
      pair' (of_fraction d I.a₁ I.b₁) (v a_1) ≤ pair' (of_fraction d a b) (v a_1)
Tactic:
intro i hi
State after:
case intro.intro.intro.intro.intro.h
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ pair' (of_fraction d I.a₁ I.b₁) (v i) ≤ pair' (of_fraction d a b) (v i)

State before:
case intro.intro.intro.intro.intro.h
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ pair' (of_fraction d I.a₁ I.b₁) (v i) ≤ pair' (of_fraction d a b) (v i)
Tactic:
have hi' : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
State after:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)

case intro.intro.intro.intro.intro.h
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
⊢ pair' (of_fraction d I.a₁ I.b₁) (v i) ≤ pair' (of_fraction d a b) (v i)

State before:
case intro.intro.intro.intro.intro.h
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
⊢ pair' (of_fraction d I.a₁ I.b₁) (v i) ≤ pair' (of_fraction d a b) (v i)
Tactic:
calc
  _ = 1 * pair' (of_fraction d I.a₁ I.b₁) (v i) + 0 * pair' (of_fraction d I.a₂ I.b₂) (v i) := by
      rw [one_mul, zero_mul, add_zero]
  _ ≤ k₁ * pair' (of_fraction d I.a₁ I.b₁) (v i) + k₂ * pair' (of_fraction d I.a₂ I.b₂) (v i) :=
      add_le_add (Int.mul_le_mul_of_nonneg_right (by exact_mod_cast hk₁) hi)
                 (Int.mul_le_mul_of_nonneg_right (by exact_mod_cast hk₂.le) hi')
  _ = _ := by
      rw [h₁, h₂, pair'_of_fraction_add, Pi.add_apply, pair'_of_fraction_mul,
          pair'_of_fraction_mul]
State after:
no goals

State before:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
⊢ 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
Tactic:
simp only [v, Nat.cast_ofNat, pair'_of_fraction] at hi ⊢
State after:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑I.a₁ * (↑d - (2 + 1) * ↑(↑i 2)) + ↑I.b₁ * (↑d - (2 + 1) * ↑(↑i 1) + (↑d - (2 + 1) * ↑(↑i 2)))
⊢ 0 ≤ ↑I.a₂ * (↑d - (2 + 1) * ↑(↑i 2)) + ↑I.b₂ * (↑d - (2 + 1) * ↑(↑i 1) + (↑d - (2 + 1) * ↑(↑i 2)))

State before:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑I.a₁ * (↑d - (2 + 1) * ↑(↑i 2)) + ↑I.b₁ * (↑d - (2 + 1) * ↑(↑i 1) + (↑d - (2 + 1) * ↑(↑i 2)))
⊢ 0 ≤ ↑I.a₂ * (↑d - (2 + 1) * ↑(↑i 2)) + ↑I.b₂ * (↑d - (2 + 1) * ↑(↑i 1) + (↑d - (2 + 1) * ↑(↑i 2)))
Tactic:
norm_num at hi ⊢
State after:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑I.a₁ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₁ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2)))
⊢ 0 ≤ ↑I.a₂ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2)))

State before:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ ↑I.a₁ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₁ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2)))
⊢ 0 ≤ ↑I.a₂ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2)))
Tactic:
set bi : ℤ := d - 3 * (i.val 2) with hbi_def
State after:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * (↑d - 3 * ↑(↑i 1) + bi)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + bi)

State before:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * (↑d - 3 * ↑(↑i 1) + bi)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + bi)
Tactic:
set ai : ℤ := d - 3 * (i.val 1) + (d - 3 * (i.val 2)) with hai_def
State after:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai

State before:
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
Tactic:
cases' le_or_lt 0 bi with hbi hbi
State after:
case hi'.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai

case hi'.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai

State before:
case hi'.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
Tactic:
refine (mul_nonneg_iff_of_pos_right (Int.ofNat_pos.mpr I.b₁_pos)).mp ?_
State after:
case hi'.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ 0 ≤ (↑I.a₂ * bi + ↑I.b₂ * ai) * ↑I.b₁

State before:
case hi'.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ 0 ≤ (↑I.a₂ * bi + ↑I.b₂ * ai) * ↑I.b₁
Tactic:
calc
  (0 : ℤ)
    ≤ (I.a₁ * bi + I.b₁ * ai) * I.b₂           := Int.mul_nonneg hi (Int.ofNat_nonneg I.b₂)
  _ = I.a₁ * I.b₂ * bi + I.b₁ * I.b₂ * ai      := by ring
  _ = I.a₂ * I.b₁ * bi + I.b₁ * I.b₂ * ai - bi := by norm_cast; rw [I.rel]; push_cast; ring
  _ = (I.a₂ * bi + I.b₂ * ai) * I.b₁ - bi      := by ring
  _ ≤ _                                        := Int.sub_le_self _ hbi
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ (↑I.a₁ * bi + ↑I.b₁ * ai) * ↑I.b₂ = ↑I.a₁ * ↑I.b₂ * bi + ↑I.b₁ * ↑I.b₂ * ai
Tactic:
ring
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑I.a₁ * ↑I.b₂ * bi + ↑I.b₁ * ↑I.b₂ * ai = ↑I.a₂ * ↑I.b₁ * bi + ↑I.b₁ * ↑I.b₂ * ai - bi
Tactic:
norm_cast
State after:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑(I.a₁ * I.b₂) * bi + ↑(I.b₁ * I.b₂) * ai = ↑(I.a₂ * I.b₁) * bi + ↑(I.b₁ * I.b₂) * ai - bi

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑(I.a₁ * I.b₂) * bi + ↑(I.b₁ * I.b₂) * ai = ↑(I.a₂ * I.b₁) * bi + ↑(I.b₁ * I.b₂) * ai - bi
Tactic:
rw [I.rel]
State after:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑(I.a₁ * I.b₂) * bi + ↑(I.b₁ * I.b₂) * ai = ↑(I.a₁ * I.b₂ + 1) * bi + ↑(I.b₁ * I.b₂) * ai - bi

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑(I.a₁ * I.b₂) * bi + ↑(I.b₁ * I.b₂) * ai = ↑(I.a₁ * I.b₂ + 1) * bi + ↑(I.b₁ * I.b₂) * ai - bi
Tactic:
push_cast
State after:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑I.a₁ * ↑I.b₂ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₁ * ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))) =
    (↑I.a₁ * ↑I.b₂ + 1) * (↑d - 3 * ↑(↑i 2)) + ↑I.b₁ * ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))) -
      (↑d - 3 * ↑(↑i 2))

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑I.a₁ * ↑I.b₂ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₁ * ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))) =
    (↑I.a₁ * ↑I.b₂ + 1) * (↑d - 3 * ↑(↑i 2)) + ↑I.b₁ * ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))) -
      (↑d - 3 * ↑(↑i 2))
Tactic:
ring
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : 0 ≤ bi
⊢ ↑I.a₂ * ↑I.b₁ * bi + ↑I.b₁ * ↑I.b₂ * ai - bi = (↑I.a₂ * bi + ↑I.b₂ * ai) * ↑I.b₁ - bi
Tactic:
ring
State after:
no goals

State before:
case hi'.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
Tactic:
have hai : 0 ≤ ai
State after:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
⊢ 0 ≤ ai

case hi'.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai

State before:
case hi'.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
Tactic:
have memS : mem_S_le d ai (-bi) :=
  ⟨Int.neg_pos_of_neg hbi, i.val 1, i.val 2, by linarith, by linarith, by ring⟩
State after:
case hi'.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai

State before:
case hi'.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
Tactic:
obtain ⟨aa, haa⟩ : ∃ x : ℕ, (x : ℤ) = ai := ⟨ai.toNat, Int.toNat_of_nonneg hai⟩
State after:
case hi'.inr.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai

State before:
case hi'.inr.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
Tactic:
obtain ⟨bb, hbb⟩ : ∃ x : ℕ, (x : ℤ) = -bi :=
  ⟨(-bi).toNat, Int.toNat_of_nonneg (Int.neg_nonneg_of_nonpos hbi.le)⟩
State after:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai

State before:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
⊢ 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
Tactic:
by_contra H
State after:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ False

State before:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ False
Tactic:
have hmem : mem aa bb I := by constructor <;> { zify; rw [haa, hbb]; linarith }
State after:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
⊢ False

State before:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
⊢ False
Tactic:
specialize h aa bb (haa.symm ▸ hbb.symm ▸ memS) hmem
State after:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
h : aa * I.b₂ = bb * I.a₂
⊢ False

State before:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
h : aa * I.b₂ = bb * I.a₂
⊢ False
Tactic:
zify at h
State after:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
h : ↑aa * ↑I.b₂ = ↑bb * ↑I.a₂
⊢ False

State before:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
h : ↑aa * ↑I.b₂ = ↑bb * ↑I.a₂
⊢ False
Tactic:
rw [haa, hbb, neg_mul, mul_comm ai, mul_comm bi] at h
State after:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
h : ↑I.b₂ * ai = -(↑I.a₂ * bi)
⊢ False

State before:
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hmem : mem aa bb I
h : ↑I.b₂ * ai = -(↑I.a₂ * bi)
⊢ False
Tactic:
exact H (neg_eq_iff_add_eq_zero.mp h.symm).symm.le
State after:
no goals

State before:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
⊢ 0 ≤ ai
Tactic:
by_contra hai
State after:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : ¬0 ≤ ai
⊢ False

State before:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : ¬0 ≤ ai
⊢ False
Tactic:
have H₁ : I.a₁ * bi ≤ 0 :=
  Int.mul_nonpos_of_nonneg_of_nonpos (Int.ofNat_nonneg I.a₁) hbi.le
State after:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : ¬0 ≤ ai
H₁ : ↑I.a₁ * bi ≤ 0
⊢ False

State before:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : ¬0 ≤ ai
H₁ : ↑I.a₁ * bi ≤ 0
⊢ False
Tactic:
have H₂ : I.b₁ * ai < 0 :=
  Int.mul_neg_of_pos_of_neg (Int.ofNat_pos.mpr I.b₁_pos) (Int.not_le.mp hai)
State after:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : ¬0 ≤ ai
H₁ : ↑I.a₁ * bi ≤ 0
H₂ : ↑I.b₁ * ai < 0
⊢ False

State before:
case hai
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : ¬0 ≤ ai
H₁ : ↑I.a₁ * bi ≤ 0
H₂ : ↑I.b₁ * ai < 0
⊢ False
Tactic:
linarith only [hi, H₁, H₂]
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
⊢ 3 * ↑i 1 + 3 * ↑i 2 ≤ 2 * d
Tactic:
linarith
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
⊢ d < 3 * ↑i 2
Tactic:
linarith
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
⊢ ai * (3 * ↑(↑i 2) - ↑d) = -bi * (2 * ↑d - 3 * ↑(↑i 1) - 3 * ↑(↑i 2))
Tactic:
ring
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ mem aa bb I
Tactic:
constructor <;> { zify; rw [haa, hbb]; linarith }
State after:
no goals

State before:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ aa * I.b₂ ≤ bb * I.a₂
Tactic:
zify
State after:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ ↑aa * ↑I.b₂ ≤ ↑bb * ↑I.a₂

State before:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ ↑aa * ↑I.b₂ ≤ ↑bb * ↑I.a₂
Tactic:
rw [haa, hbb]
State after:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ ai * ↑I.b₂ ≤ -bi * ↑I.a₂

State before:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hbi : bi < 0
hai : 0 ≤ ai
memS : mem_S_le d ai (-bi)
aa : ℕ
haa : ↑aa = ai
bb : ℕ
hbb : ↑bb = -bi
H : ¬0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
⊢ ai * ↑I.b₂ ≤ -bi * ↑I.a₂
Tactic:
linarith
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
⊢ pair' (of_fraction d I.a₁ I.b₁) (v i) =
    1 * pair' (of_fraction d I.a₁ I.b₁) (v i) + 0 * pair' (of_fraction d I.a₂ I.b₂) (v i)
Tactic:
rw [one_mul, zero_mul, add_zero]
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
⊢ 1 ≤ ↑k₁
Tactic:
exact_mod_cast hk₁
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
⊢ 0 ≤ ↑k₂
Tactic:
exact_mod_cast hk₂.le
State after:
no goals

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
hi : 0 ≤ pair' (of_fraction d I.a₁ I.b₁) (v i)
hi' : 0 ≤ pair' (of_fraction d I.a₂ I.b₂) (v i)
⊢ ↑k₁ * pair' (of_fraction d I.a₁ I.b₁) (v i) + ↑k₂ * pair' (of_fraction d I.a₂ I.b₂) (v i) =
    pair' (of_fraction d a b) (v i)
Tactic:
rw [h₁, h₂, pair'_of_fraction_add, Pi.add_apply, pair'_of_fraction_mul,
    pair'_of_fraction_mul]
State after:
no goals