theorem
proved
tactic proof
ofMicroMoves_zero_outside
show as:
view Lean formalization →
formal statement (Lean)
87theorem ofMicroMoves_zero_outside (moves : List MicroMove) :
88 ∀ {pair prim}, pair ∉ (moves.map (·.pair)).toFinset.filter (fun k =>
89 ∃ prim, aggCoeff moves k prim ≠ 0) → aggCoeff moves pair prim = 0 := by
proof body
Tactic-mode proof.
90 intro pair prim h_not_mem
91 by_contra h_ne
92 apply h_not_mem
93 rw [Finset.mem_filter, List.mem_toFinset]
94 constructor
95 · -- Show pair ∈ moves.map (·.pair)
96 -- If aggCoeff ≠ 0, there's a move with matching pair and prim
97 have h_filter_ne : (moves.filter fun m => m.pair = pair ∧ m.primitive = prim) ≠ [] := by
98 intro h_empty
99 unfold aggCoeff at h_ne
100 rw [h_empty] at h_ne
101 simp at h_ne
102 obtain ⟨m, hm⟩ := List.exists_mem_of_ne_nil _ h_filter_ne
103 rw [List.mem_filter] at hm
104 simp only [decide_eq_true_eq] at hm
105 rw [List.mem_map]
106 exact ⟨m, hm.1, hm.2.1⟩
107 · -- Show ∃ prim', aggCoeff moves pair prim' ≠ 0
108 exact ⟨prim, h_ne⟩
109