English
The length of a walk in the box product equals the sum of the lengths of its left and right projections.
Русский
Длина пути в boxProd равна сумме длин его левой и правой проекций.
LaTeX
$$$\\\\forall {G H} {w : (G □ H).Walk { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ },\\\\ w.length = w.ofBoxProdLeft.length + w.ofBoxProdRight.length$$$
Lean4
theorem length_boxProd {a₁ a₂ : α} {b₁ b₂ : β} [DecidableEq α] [DecidableEq β] [DecidableRel G.Adj] [DecidableRel H.Adj]
(w : (G □ H).Walk (a₁, b₁) (a₂, b₂)) : w.length = w.ofBoxProdLeft.length + w.ofBoxProdRight.length := by
match w with
| .nil => simp [ofBoxProdLeft, ofBoxProdRight]
| .cons x w' =>
next c =>
unfold ofBoxProdLeft ofBoxProdRight
rw [length_cons, length_boxProd w']
have disj : (G.Adj a₁ c.1 ∧ b₁ = c.2) ∨ (H.Adj b₁ c.2 ∧ a₁ = c.1) := by simp_all
rcases disj with h₁ | h₂
· simp only [h₁, and_self, ↓reduceDIte, length_cons, Or.by_cases]
rw [add_comm, add_comm w'.ofBoxProdLeft.length 1, add_assoc]
congr <;> simp [h₁.2.symm]
· simp only [h₂, add_assoc, Or.by_cases]
congr <;> simp [h₂.2.symm]
