Theorem: Weight.tv_finset (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
⊢ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) = testvecs n d
Tactic:
simp only [testvecs]
State after:
n d : ℕ
inst✝ : NeZero d
⊢ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) = {w | Weight.sum w = d}

State before:
n d : ℕ
inst✝ : NeZero d
⊢ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) = {w | Weight.sum w = d}
Tactic:
ext a
State after:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ a ∈ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) ↔ a ∈ {w | Weight.sum w = d}

State before:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ a ∈ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) ↔ a ∈ {w | Weight.sum w = d}
Tactic:
simp only [Finset.Nat.mem_antidiagonalTuple, Finset.mem_coe, Finset.mem_mk, Weight.sum]
State after:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ ∑ i : Fin (Nat.succ n), a i = d ↔ a ∈ {w | ∑ j : Fin (Nat.succ n), w j = d}

State before:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ ∑ i : Fin (Nat.succ n), a i = d ↔ a ∈ {w | ∑ j : Fin (Nat.succ n), w j = d}
Tactic:
rfl
State after:
no goals