86lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) : 87 sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
proof body
Tactic-mode proof.
88 classical 89 unfold sumFirst Z_of_window extendPeriodic8 90 have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by 91 intro i; exact Nat.mod_eq_of_lt i.isLt 92 have h8 : 0 < 8 := by decide 93 have hfun : 94 (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ h8⟩ then 1 else 0)) 95 = (fun i : Fin 8 => (if w i then 1 else 0)) := by 96 funext i; simp [hmod i] 97 -- Now the two sums are definitionally equal by hfun. 98 have := congrArg (fun f => ∑ i : Fin 8, f i) hfun 99 simpa using this 100
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.