internlm/Lean-Github huggingface dataset:
Theorem: Weight.testvecs1
Proof state before:
case h.a.h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
⊢ ↑{ val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } k = ↑a k
Tactic:
simp [Function.update_apply]
Proof state after:
case h.a.h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
⊢ (if k = j then 1 else 0) = ↑a k
Theorem: Weight.testvecs1
Proof state before:
case h.a.h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
⊢ (if k = j then 1 else 0) = ↑a k
Tactic:
split_ifs with hjk
Proof state after:
case pos
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
hjk : k = j
⊢ 1 = ↑a k

case neg
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
hjk : ¬k = j
⊢ 0 = ↑a k
Theorem: Weight.testvecs1
Proof state before:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ j, ↑a j = 1
Tactic:
have h₁ : ∃ j, 0 < a.val j
Proof state after:
case h₁
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ j, 0 < ↑a j

case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
h₁ : ∃ j, 0 < ↑a j
⊢ ∃ j, ↑a j = 1
Theorem: Weight.testvecs1
Proof state before:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
h₁ : ∃ j, 0 < ↑a j
⊢ ∃ j, ↑a j = 1
Tactic:
obtain ⟨j, hj⟩ := h₁
Proof state after:
case h.intro
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ∃ j, ↑a j = 1
Theorem: Weight.testvecs1
Proof state before:
case h.intro
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ∃ j, ↑a j = 1
Tactic:
use j
Proof state after:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ↑a j = 1
Theorem: Weight.testvecs1
Proof state before:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ↑a j = 1
Tactic:
suffices h₃ : a.val j ≤ 1
Proof state after:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
h₃ : ↑a j ≤ 1
⊢ ↑a j = 1

case h₃
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ↑a j ≤ 1
Theorem: Weight.testvecs1
Proof state before:
case h₃
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ↑a j ≤ 1
Tactic:
conv_rhs => rw [← h₂]
Proof state after:
case h₃
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ↑a j ≤ ∑ k : Fin (Nat.succ n), ↑a k
Theorem: Weight.testvecs1
Proof state before:
case h₃
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
⊢ ↑a j ≤ ∑ k : Fin (Nat.succ n), ↑a k
Tactic:
exact Finset.single_le_sum (fun k _ ↦ Nat.zero_le (a.val k)) (Finset.mem_univ j)
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
case h₁
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ j, 0 < ↑a j
Tactic:
by_contra! hf
Proof state after:
case h₁
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
hf : ∀ (j : Fin (Nat.succ n)), ↑a j ≤ 0
⊢ False
Theorem: Weight.testvecs1
Proof state before:
case h₁
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
hf : ∀ (j : Fin (Nat.succ n)), ↑a j ≤ 0
⊢ False
Tactic:
simp only [(fun k ↦ Nat.eq_zero_of_le_zero (hf k)), Finset.sum_const_zero,
             Nat.zero_ne_one] at h₂
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : 0 < ↑a j
h₃ : ↑a j ≤ 1
⊢ ↑a j = 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
Tactic:
intro k hk
Proof state after:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
⊢ ↑a k = 0
Theorem: Weight.testvecs1
Proof state before:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
⊢ ↑a k = 0
Tactic:
let s : Finset (Fin n.succ) := (Finset.univ \ {j})
Proof state after:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
⊢ ↑a k = 0
Theorem: Weight.testvecs1
Proof state before:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
⊢ ↑a k = 0
Tactic:
have hs : insert j s = Finset.univ
Proof state after:
case hs
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
⊢ insert j s = Finset.univ

case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
hs : insert j s = Finset.univ
⊢ ↑a k = 0
Theorem: Weight.testvecs1
Proof state before:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
hs : insert j s = Finset.univ
⊢ ↑a k = 0
Tactic:
have hjs : ¬j ∈ s := by simp
Proof state after:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
hs : insert j s = Finset.univ
hjs : j ∉ s
⊢ ↑a k = 0
Theorem: Weight.testvecs1
Proof state before:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
hs : insert j s = Finset.univ
hjs : j ∉ s
⊢ ↑a k = 0
Tactic:
rw [← hs, Finset.sum_insert hjs, hj] at h₂
Proof state after:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
h₂ : 1 + ∑ x in s, ↑a x = 1
hs : insert j s = Finset.univ
hjs : j ∉ s
⊢ ↑a k = 0
Theorem: Weight.testvecs1
Proof state before:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
h₂ : 1 + ∑ x in s, ↑a x = 1
hs : insert j s = Finset.univ
hjs : j ∉ s
⊢ ↑a k = 0
Tactic:
simp only [Finset.mem_univ, not_true, add_right_eq_self, Finset.sum_eq_zero_iff,
  Finset.mem_sdiff, Finset.mem_singleton, true_and] at h₂
Proof state after:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
hs : insert j s = Finset.univ
hjs : j ∉ s
h₂ : ∀ (x : Fin (Nat.succ n)), ¬x = j → ↑a x = 0
⊢ ↑a k = 0
Theorem: Weight.testvecs1
Proof state before:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
hs : insert j s = Finset.univ
hjs : j ∉ s
h₂ : ∀ (x : Fin (Nat.succ n)), ¬x = j → ↑a x = 0
⊢ ↑a k = 0
Tactic:
exact h₂ k hk
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
case hs
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
⊢ insert j s = Finset.univ
Tactic:
simp [Finset.insert_eq]
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
k : Fin (Nat.succ n)
hk : k ≠ j
s : Finset (Fin (Nat.succ n)) := Finset.univ \ {j}
hs : insert j s = Finset.univ
⊢ j ∉ s
Tactic:
simp
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
case pos
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
hjk : k = j
⊢ 1 = ↑a k
Tactic:
rw [hjk]
Proof state after:
case pos
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
hjk : k = j
⊢ 1 = ↑a j
Theorem: Weight.testvecs1
Proof state before:
case pos
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
hjk : k = j
⊢ 1 = ↑a j
Tactic:
exact hj.symm
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
case neg
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
hjk : ¬k = j
⊢ 0 = ↑a k
Tactic:
exact (h' k hjk).symm
Proof state after:
no goals
Theorem: Weight.w1_zero
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ w1 n 0 = 0
Tactic:
simp only [w1, eq_self_iff_true, if_true]
Proof state after:
no goals
Theorem: Weight.sum_w1
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ Weight.sum (w1 n) = n
Tactic:
simp [w1, Weight.sum, Finset.sum_ite, Finset.filter_ne']
Proof state after:
no goals
Theorem: Weight.E_w1
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ E (w1 n) = 1
Tactic:
rw [E, sum_w1]
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
⊢ n * 1 / (n + 1) + 1 = 1
Theorem: Weight.E_w1
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ n * 1 / (n + 1) + 1 = 1
Tactic:
simp [Nat.div_eq_zero_iff]
Proof state after:
no goals
Theorem: Weight.w1_balanced
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ balanced (w1 n)
Tactic:
simp only [balanced]
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
⊢ ∀ (j : Fin (Nat.succ n)), w1 n j ≤ E (w1 n)
Theorem: Weight.w1_balanced
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
⊢ ∀ (j : Fin (Nat.succ n)), w1 n j ≤ E (w1 n)
Tactic:
intro j
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ w1 n j ≤ E (w1 n)
Theorem: Weight.w1_balanced
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ w1 n j ≤ E (w1 n)
Tactic:
rw [E_w1, w1]
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ (if j = 0 then 0 else 1) ≤ 1
Theorem: Weight.w1_balanced
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
⊢ (if j = 0 then 0 else 1) ≤ 1
Tactic:
split_ifs with h
Proof state after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : j = 0
⊢ 0 ≤ 1

case neg
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : ¬j = 0
⊢ 1 ≤ 1
Theorem: Weight.w1_balanced
Proof state before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : j = 0
⊢ 0 ≤ 1
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Weight.w1_balanced
Proof state before:
case neg
n✝ n : ℕ
inst✝ : NeZero n
j : Fin (Nat.succ n)
h : ¬j = 0
⊢ 1 ≤ 1
Tactic:
exact le_rfl
Proof state after:
no goals
Theorem: Weight.pair_w1
Proof state before:
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
⊢ pair (w1 n) ↑a = if a = tw n 1 0 then 0 else 1
Tactic:
obtain ⟨k, ha⟩ := (testvecs1 n).2 a
Proof state after:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ pair (w1 n) ↑a = if a = tw n 1 0 then 0 else 1
Theorem: Weight.pair_w1
Proof state before:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ pair (w1 n) ↑a = if a = tw n 1 0 then 0 else 1
Tactic:
rw [ha.symm, pair_tw, Nat.sub_self, zero_mul, zero_add, w1_apply]
Proof state after:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Theorem: Weight.pair_w1
Proof state before:
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
by_cases hk : k = 0
Proof state after:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1

case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Theorem: Weight.pair_w1
Proof state before:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
simp only [hk, eq_self_iff_true]
Proof state after:
no goals
Theorem: Weight.pair_w1
Proof state before:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
simp only [hk, if_false]
Proof state after:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ 1 = if tw n 1 k = tw n 1 0 then 0 else 1
Theorem: Weight.pair_w1
Proof state before:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
⊢ 1 = if tw n 1 k = tw n 1 0 then 0 else 1
Tactic:
split_ifs with h'
Proof state after:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
⊢ False

case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : ¬tw n 1 k = tw n 1 0
⊢ 1 = 1
Theorem: Weight.pair_w1
Proof state before:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
⊢ False
Tactic:
have t := hk (tw_inj n 1 h')
Proof state after:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
t : False
⊢ False
Theorem: Weight.pair_w1
Proof state before:
case pos
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
t : False
⊢ False
Tactic:
tauto
Proof state after:
no goals
Theorem: Weight.pair_w1
Proof state before:
case neg
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
hk : ¬k = 0
h' : ¬tw n 1 k = tw n 1 0
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Weight.w1_minimal
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ w1 n ≤ w
Tactic:
simp only [dom_iff, f_le_iff, f_apply, Subtype.coe_mk]
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ ∀ (a : ↑(testvecs n 1)), E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a
Theorem: Weight.w1_minimal
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ ∀ (a : ↑(testvecs n 1)), E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a
Tactic:
intro a
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a
Theorem: Weight.w1_minimal
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a
Tactic:
simp only [E_w1, ge_iff_le, tsub_le_iff_right, pair_w1]
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ 1 ≤ E w - pair w ↑a + if a = tw n 1 0 then 0 else 1
Theorem: Weight.w1_minimal
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ 1 ≤ E w - pair w ↑a + if a = tw n 1 0 then 0 else 1
Tactic:
split_ifs with h
Proof state after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 0

case neg
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : ¬a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 1
Theorem: Weight.w1_minimal
Proof state before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 0
Tactic:
rw [← f, h, eval_f_tw, hw]
Proof state after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - (1 - 1) * 0 - 0 + 0
Theorem: Weight.w1_minimal
Proof state before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - (1 - 1) * 0 - 0 + 0
Tactic:
simp only [mul_zero, tsub_zero, add_zero]
Proof state after:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w
Theorem: Weight.w1_minimal
Proof state before:
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w
Tactic:
exact one_le_E w
Proof state after:
no goals
Theorem: Weight.w1_minimal
Proof state before:
case neg
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : ¬a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 1
Tactic:
simp only [le_add_iff_nonneg_left, zero_le']
Proof state after:
no goals
Theorem: Weight.w1_unique
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
⊢ w = w1 n
Tactic:
have h₁ := w1_minimal hw
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
⊢ w = w1 n
Theorem: Weight.w1_unique
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
⊢ w = w1 n
Tactic:
have h₂ := hmin _ h₁
Proof state after:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ w = w1 n
Theorem: Weight.w1_unique
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ w = w1 n
Tactic:
have hE : w.E = 1
Proof state after:
case hE
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
⊢ E w = 1

n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
⊢ w = w1 n
Theorem: Weight.w1_unique
Proof state before:
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
⊢ w = w1 n
Tactic:
ext j
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
⊢ w j = w1 n j
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
⊢ w j = w1 n j
Tactic:
have hc₁ := (lec_iff _ _).mp
              ((dom_iff_gec_of_balanced hw (w1_balanced n) (hE.trans (E_w1 n).symm)).mp h₂)
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
⊢ w j = w1 n j
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
⊢ w j = w1 n j
Tactic:
have hsum : (w1 n).sum ≤ w.sum := Finset.sum_le_sum (fun j _ ↦ hc₁ j)
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : Weight.sum (w1 n) ≤ Weight.sum w
⊢ w j = w1 n j
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : Weight.sum (w1 n) ≤ Weight.sum w
⊢ w j = w1 n j
Tactic:
rw [sum_w1] at hsum
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : E w = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j
Tactic:
rw [E] at hE
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : Weight.sum w * 1 / (n + 1) + 1 = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
hE : Weight.sum w * 1 / (n + 1) + 1 = 1
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
⊢ w j = w1 n j
Tactic:
simp [Nat.div_eq_zero_iff] at hE
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
⊢ w j = w1 n j
Theorem: Weight.w1_unique
Proof state before:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
⊢ w j = w1 n j
Tactic:
have hn : w.sum = n := Nat.eq_of_le_of_lt_succ hsum hE
Proof state after:
case h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
hmin : ∀ w' ≤ w, w ≤ w'
h₁ : w1 n ≤ w
h₂ : w ≤ w1 n
j : Fin (Nat.succ n)
hc₁ : ∀ (j : Fin (Nat.succ n)), w1 n j ≤ w j
hsum : n ≤ Weight.sum w
hE : Weight.sum w < n + 1
hn : Weight.sum w = n
⊢ w j = w1 n j