English
Compatibility for the inverse component: the inverse of XXIsoOfEq composed with ιTotal equals the corresponding total inclusion with adjusted indices.
Русский
Совместимость для обратного компонента: обратный XXIsoOfEq композиции с ιTotal равен соответствующему включению total с изменёнными индексами.
LaTeX
$$$\\big(\\text{XXIsoOfEq} \\; K \\; c_{12} \\; h_1 \\; h_2\\big).inv \\; \\circ \\; ιTotal c_{12} x_1 x_2 i_{12} h = ιTotal c_{12} y_1 y_2 i_{12} (by rw [\\Leftarrow h, h_1, h_2])$$$
Lean4
@[reassoc (attr := simp)]
theorem XXIsoOfEq_inv_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂)
(h : ComplexShape.π c₁ c₂ c₁₂ (x₁, x₂) = i₁₂) :
(K.XXIsoOfEq _ _ _ h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ y₁ y₂ i₁₂ (by rw [← h, h₁, h₂]) :=
by
subst h₁ h₂
simp
