Lean4
/-- Constructor for isomorphisms in `Square c` -/
def isoMk {sq₁ sq₂ : Square C} (e₁ : sq₁.X₁ ≅ sq₂.X₁) (e₂ : sq₁.X₂ ≅ sq₂.X₂) (e₃ : sq₁.X₃ ≅ sq₂.X₃)
(e₄ : sq₁.X₄ ≅ sq₂.X₄) (comm₁₂ : sq₁.f₁₂ ≫ e₂.hom = e₁.hom ≫ sq₂.f₁₂) (comm₁₃ : sq₁.f₁₃ ≫ e₃.hom = e₁.hom ≫ sq₂.f₁₃)
(comm₂₄ : sq₁.f₂₄ ≫ e₄.hom = e₂.hom ≫ sq₂.f₂₄) (comm₃₄ : sq₁.f₃₄ ≫ e₄.hom = e₃.hom ≫ sq₂.f₃₄) : sq₁ ≅ sq₂
where
hom :=
{ τ₁ := e₁.hom
τ₂ := e₂.hom
τ₃ := e₃.hom
τ₄ := e₄.hom }
inv :=
{ τ₁ := e₁.inv
τ₂ := e₂.inv
τ₃ := e₃.inv
τ₄ := e₄.inv
comm₁₂ := by simp only [← cancel_mono e₂.hom, assoc, Iso.inv_hom_id, comp_id, comm₁₂, Iso.inv_hom_id_assoc]
comm₁₃ := by simp only [← cancel_mono e₃.hom, assoc, Iso.inv_hom_id, comp_id, comm₁₃, Iso.inv_hom_id_assoc]
comm₂₄ := by simp only [← cancel_mono e₄.hom, assoc, Iso.inv_hom_id, comp_id, comm₂₄, Iso.inv_hom_id_assoc]
comm₃₄ := by simp only [← cancel_mono e₄.hom, assoc, Iso.inv_hom_id, comp_id, comm₃₄, Iso.inv_hom_id_assoc] }
