English
The mates equivalence respects another square composition rule.
Русский
Эквивалентность mейт сохраняет правило композиции квадрата.
LaTeX
$$$$ (\\mathrm{mateEquiv}) \\; \\text{square}$$$$
Lean4
/-- The mates equivalence commutes with composition of squares of squares. These results form the
basis for an isomorphism of double categories to be proven later.
-/
theorem mateEquiv_square (α : TwoSquare G₁ L₁ L₃ H₁) (β : TwoSquare H₁ L₂ L₄ K₁) (γ : TwoSquare G₂ L₃ L₅ H₂)
(δ : TwoSquare H₂ L₄ L₆ K₂) :
(mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ (γ ≫ᵥ δ)) =
((mateEquiv adj₂ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₃ α)) ≫ᵥ ((mateEquiv adj₄ adj₆ δ) ≫ₕ (mateEquiv adj₃ adj₅ γ)) :=
by
have vcomp := mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) (α ≫ᵥ β) (γ ≫ᵥ δ)
simp only [mateEquiv_hcomp] at vcomp
assumption
