internlm/Lean-Github huggingface dataset:
Theorem: Weight.dom_of_mem_interior_right
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
⊢ 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
Tactic:
obtain ⟨aa, haa⟩ : ∃ x : ℕ, (x : ℤ) = -ai :=
  ⟨(-ai).toNat, Int.toNat_of_nonneg (Int.neg_nonneg_of_nonpos hai.le)⟩
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
⊢ 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
Theorem: Weight.dom_of_mem_interior_right
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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 hbi⟩
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
⊢ 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
Theorem: Weight.dom_of_mem_interior_right
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
⊢ 0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
Tactic:
by_contra H
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
H : ¬0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
⊢ False
Theorem: Weight.dom_of_mem_interior_right
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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 }
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Theorem: Weight.dom_of_mem_interior_right
Proof 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_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Proof 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Theorem: Weight.dom_of_mem_interior_right
Proof 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Proof 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Theorem: Weight.dom_of_mem_interior_right
Proof 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Proof 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Theorem: Weight.dom_of_mem_interior_right
Proof 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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 (eq_neg_iff_add_eq_zero.mp h.symm).symm.le
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case hbi
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
⊢ 0 ≤ bi
Tactic:
by_contra hbi
Proof state after:
case hbi
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : ¬0 ≤ bi
⊢ False
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case hbi
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : ¬0 ≤ bi
⊢ False
Tactic:
have H₁ : I.b₂ * ai ≤ 0 :=
  Int.mul_nonpos_of_nonneg_of_nonpos (Int.ofNat_nonneg I.b₂) hai.le
Proof state after:
case hbi
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : ¬0 ≤ bi
H₁ : ↑I.b₂ * ai ≤ 0
⊢ False
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case hbi
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : ¬0 ≤ bi
H₁ : ↑I.b₂ * ai ≤ 0
⊢ False
Tactic:
have H₂ : I.a₂ * bi < 0 :=
  Int.mul_neg_of_pos_of_neg (Int.ofNat_pos.mpr I.a₂_pos) (Int.not_le.mp hbi)
Proof state after:
case hbi
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : ¬0 ≤ bi
H₁ : ↑I.b₂ * ai ≤ 0
H₂ : ↑I.a₂ * bi < 0
⊢ False
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case hbi
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : ¬0 ≤ bi
H₁ : ↑I.b₂ * ai ≤ 0
H₂ : ↑I.a₂ * bi < 0
⊢ False
Tactic:
linarith only [hi, H₁, H₂]
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case memS
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ mem_S_ge d (-ai) bi
Tactic:
refine ⟨Int.neg_pos_of_neg hai, i.val 1, i.val 2, ?_, by linarith, by linarith, by ring⟩
Proof state after:
case memS
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ ↑i 1 + ↑i 2 ≤ d
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case memS
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ ↑i 1 + ↑i 2 ≤ d
Tactic:
have HH : i.val.sum = i.val 0 + (i.val 1 + i.val 2)
Proof state after:
case HH
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ Weight.sum ↑i = ↑i 0 + (↑i 1 + ↑i 2)

case memS
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
HH : Weight.sum ↑i = ↑i 0 + (↑i 1 + ↑i 2)
⊢ ↑i 1 + ↑i 2 ≤ d
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case memS
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
HH : Weight.sum ↑i = ↑i 0 + (↑i 1 + ↑i 2)
⊢ ↑i 1 + ↑i 2 ≤ d
Tactic:
linarith only [i.prop ▸ HH]
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ 2 * d < 3 * ↑i 1 + 3 * ↑i 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ 3 * ↑i 2 ≤ d
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ -ai * (3 * ↑(↑i 2) - ↑d) = bi * (2 * ↑d - 3 * ↑(↑i 1) - 3 * ↑(↑i 2))
Tactic:
ring
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case HH
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
⊢ Weight.sum ↑i = ↑i 0 + (↑i 1 + ↑i 2)
Tactic:
rw [Weight.sum, Fin.sum_univ_three, add_assoc]
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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 }
Proof state after:
no goals
Theorem: Weight.dom_of_mem_interior_right
Proof state before:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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
Proof state after:
case right
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge 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))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge 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₂