Theorem: Weight.testvecs1 (Weights/Degree1.lean)

State before:
n✝ n : ℕ
⊢ Function.Bijective (tw n 1)
Tactic:
refine ⟨tw_inj n 1, ?_⟩
State after:
n✝ n : ℕ
⊢ Function.Surjective (tw n 1)

State before:
n✝ n : ℕ
⊢ Function.Surjective (tw n 1)
Tactic:
intro a
State after:
n✝ n : ℕ
a : ↑(testvecs n 1)
⊢ ∃ a_1, tw n 1 a_1 = a

State before:
n✝ n : ℕ
a : ↑(testvecs n 1)
⊢ ∃ a_1, tw n 1 a_1 = a
Tactic:
have h₂ : ∑ k, a.val k = 1 := a.2
State after:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, tw n 1 a_1 = a

State before:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, tw n 1 a_1 = a
Tactic:
simp [tw, tw']
State after:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a

State before:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Tactic:
have h : ∃ j, a.val j = 1
State after:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ j, ↑a j = 1

n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
h : ∃ j, ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a

State before:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
h : ∃ j, ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Tactic:
obtain ⟨j, hj⟩ := h
State after:
case intro
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a

State before:
case intro
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Tactic:
use j
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
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a

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
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a
Tactic:
have h' : ∀ k, k ≠ j → a.val k = 0
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)), k ≠ j → ↑a k = 0

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
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a

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
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a
Tactic:
ext k
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)
⊢ ↑{ val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } k = ↑a k

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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