proposition: Lemma DExtIso_Comm1 {PT : PreTriangData} {D1 D2 : DTri} (D1' D2' : Tri) (I1 : TriIso D1 D1') (I2 : TriIso D2 D2') {f1 : Ob1 D1 --> Ob1 D2} {f2 : Ob2 D1 --> Ob2 D2} (H : f1 · Mor1 D2 = Mor1 D1 · f2) (h : Ob3 D1' --> Ob3 D2') (comm1 : Mor2 D1' · h = MPMor2 (TriIsoInv I1) · f2 · MPMor2 I2 · Mor2 D2') (comm2 : Mor3 D1' · (# (AddEquiv1 (@Trans PT)) (MPMor1 (TriIsoInv I1) · f1 · MPMor1 I2)) = h · Mor3 D2') : Mor2 D1 · (MPMor3 I1 · h · MPMor3 (TriIsoInv I2)) = f2 · Mor2 D2.
proof: Proof. rewrite assoc. rewrite assoc. rewrite <- (MPComm2 I1). rewrite <- (assoc _ (Mor2 D1')). rewrite comm1. rewrite assoc. rewrite assoc. rewrite assoc. cbn. rewrite (is_inverse_in_precat1 (TriMor_is_iso2 I1)). rewrite id_left. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite assoc. rewrite (MPComm2 I2). rewrite <- assoc. rewrite (is_inverse_in_precat1 (TriMor_is_iso3 I2)). apply id_right. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.ShortExactSequences UniMath.CategoryTheory.Categories.Abgr UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.AdditiveFunctors UniMath.CategoryTheory.FiveLemma