English
For fixed i1, if i2 relates to i2' then the next component along π with (i1,i2) equals that with (i1,i2').
Русский
Для фиксированного i1, если i2 связано с i2', то следующий компонент вдоль π по (i1,i2) = компонент по (i1,i2').
LaTeX
$$$\\forall i_1\\in I_1\\; \\forall {i_2,i_2'\\in I_2}\\; (c_2.Rel(i_2,i_2')) \\Rightarrow c_{12}.next(\\pi(c_1,c_2,c_{12})(\\langle i_1,i_2\\rangle))=\\pi(c_1,c_2,c_{12})(\\langle i_1,i_2'\\rangle)$$$
Lean4
theorem ε₁_ε₂ {i₁ i₁' : I₁} {i₂ i₂' : I₂} (h₁ : c₁.Rel i₁ i₁') (h₂ : c₂.Rel i₂ i₂') :
ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ * ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = -ε₂ c₁ c₂ c₁₂ ⟨i₁', i₂⟩ * ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ :=
Eq.trans (mul_one _).symm
(by
rw [← Int.units_mul_self (ComplexShape.ε₁ c₁ c₂ c₁₂ (i₁, i₂')), mul_assoc]
conv_lhs =>
arg 2
rw [← mul_assoc, ε₂_ε₁ c₁₂ h₁ h₂]
rw [neg_mul, neg_mul, neg_mul, mul_neg, neg_inj, ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul])
