awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
rw :
  Eq (α := ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)
    (CategoryStruct.comp (Y :=
        ShortComplex.LeftHomologyData.K (S := (K.extend e).sc j')
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData)))
        (Iso.hom
          (ShortComplex.LeftHomologyData.cyclesIso
            (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))))
        (ShortComplex.LeftHomologyData.π
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
      ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)
    (CategoryStruct.comp (Y := K.cycles j) (Iso.hom (K.extendCyclesIso e hj'))
        (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.π) :
      ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)
⊢ Eq (α := (K.extend e).cycles j' ⟶ K.homology j)
    (CategoryStruct.comp (Y := (K.extend e).homology j') ((K.extend e).sc j').homologyπ
        (CategoryStruct.comp (Y := (K.sc j).homologyData.left.H)
          (Iso.hom
              (ShortComplex.LeftHomologyData.homologyIso
                (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
            (K.extend e).homology j' ⟶ (K.sc j).homologyData.left.H)
          (Iso.inv (K.sc j).homologyData.left.homologyIso)) :
      (K.extend e).cycles j' ⟶ K.homology j)
    (CategoryStruct.comp (Y := K.cycles j) (Iso.hom (K.extendCyclesIso e hj')) (K.sc j).homologyπ :
      (K.extend e).cycles j' ⟶ K.homology j)

Tactic:
rw [ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc,
    ← cancel_mono (K.sc j).homologyData.left.homologyIso.hom,
    assoc, assoc, assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc, HomologicalComplex.sc, CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom, CategoryTheory.Iso.hom, CategoryTheory.ShortComplex.homologyData
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
dsimp :
  Eq (α := ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)
    (Iso.hom
        (ShortComplex.LeftHomologyData.cyclesIso
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) ≫
      (K.sc j).homologyData.left.π)
    (CategoryStruct.comp (Y := K.cycles j)
      (CategoryStruct.comp (Y := (K.sc j).homologyData.left.K)
        (Iso.hom
            (ShortComplex.LeftHomologyData.cyclesIso
              (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
          (K.extend e).cycles j' ⟶ (K.sc j).homologyData.left.K)
        (Iso.inv (K.sc j).homologyData.left.cyclesIso : (K.sc j).homologyData.left.K ⟶ K.cycles j))
      (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.π))
⊢ Eq (α := ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)
    (CategoryStruct.comp (Y :=
        ShortComplex.LeftHomologyData.K (S := (K.extend e).sc j')
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData)))
        (Iso.hom
          (ShortComplex.LeftHomologyData.cyclesIso
            (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))))
        (ShortComplex.LeftHomologyData.π
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
      ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)
    (CategoryStruct.comp (Y := K.cycles j) (Iso.hom (K.extendCyclesIso e hj'))
        (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.π) :
      ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)

Tactic:
dsimp [extendCyclesIso]

Premises used: HomologicalComplex.extendCyclesIso
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := ((K.extend e).sc j').cycles ⟶ (K.sc j).homologyData.left.H)
    (Iso.hom
        (ShortComplex.LeftHomologyData.cyclesIso
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) ≫
      (K.sc j).homologyData.left.π)
    (CategoryStruct.comp (Y := K.cycles j)
      (CategoryStruct.comp (Y := (K.sc j).homologyData.left.K)
        (Iso.hom
            (ShortComplex.LeftHomologyData.cyclesIso
              (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
          (K.extend e).cycles j' ⟶ (K.sc j).homologyData.left.K)
        (Iso.inv (K.sc j).homologyData.left.cyclesIso : (K.sc j).homologyData.left.K ⟶ K.cycles j))
      (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.π))

Tactic:
simp only [assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := K.cycles j ⟶ (K.extend e).homology j') (K.homologyπ j ≫ Iso.inv (K.extendHomologyIso e hj'))
    (Iso.inv (K.extendCyclesIso e hj') ≫ (K.extend e).homologyπ j')

Tactic:
simp only [← cancel_mono (K.extendHomologyIso e hj').hom,
    assoc, Iso.inv_hom_id, comp_id, homologyπ_extendHomologyIso_hom, Iso.inv_hom_id_assoc]

Premises used: HomologicalComplex.homologyπ_extendHomologyIso_hom, CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.extendHomologyIso, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
rw :
  Eq (α := K.X j ⟶ K.opcycles j) (K.pOpcycles j)
    (Iso.inv (K.extendXIso e hj') ≫
      CategoryStruct.comp (Y := (K.extend e).opcycles j') ((K.extend e).pOpcycles j')
        (Iso.hom (K.extendOpcyclesIso e hj')))
⊢ Eq (α := K.X j ⟶ (K.extend e).opcycles j')
    (CategoryStruct.comp (Y := K.opcycles j) (K.pOpcycles j) (Iso.inv (K.extendOpcyclesIso e hj')))
    (Iso.inv (K.extendXIso e hj') ≫ (K.extend e).pOpcycles j')

Tactic:
rw [← cancel_mono (K.extendOpcyclesIso e hj').hom, assoc, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, HomologicalComplex.extendOpcyclesIso, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
dsimp :
  Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles
    (Iso.inv (K.extendXIso e hj') ≫
      CategoryStruct.comp (Y := (K.extend e).opcycles j') ((K.extend e).sc j').pOpcycles
        (CategoryStruct.comp (Y := (K.sc j).homologyData.right.Q)
          (Iso.hom
              (ShortComplex.RightHomologyData.opcyclesIso
                (ShortComplex.HomologyData.right (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
            (K.extend e).opcycles j' ⟶ (K.sc j).homologyData.right.Q)
          (Iso.inv (K.sc j).homologyData.right.opcyclesIso)))
⊢ Eq (α := K.X j ⟶ K.opcycles j) (K.pOpcycles j)
    (Iso.inv (K.extendXIso e hj') ≫
      CategoryStruct.comp (Y := (K.extend e).opcycles j') ((K.extend e).pOpcycles j')
        (Iso.hom (K.extendOpcyclesIso e hj')))

Tactic:
dsimp [extendOpcyclesIso, pOpcycles]

Premises used: HomologicalComplex.extendOpcyclesIso, HomologicalComplex.pOpcycles
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
rw :
  Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles
    (CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
      (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := (K.extend e).sc j')
          (ShortComplex.HomologyData.right (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData)))
        (ShortComplex.RightHomologyData.p
          (ShortComplex.HomologyData.right (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData)))
        (Iso.inv (K.sc j).homologyData.right.opcyclesIso)))
⊢ Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles
    (Iso.inv (K.extendXIso e hj') ≫
      CategoryStruct.comp (Y := (K.extend e).opcycles j') ((K.extend e).sc j').pOpcycles
        (CategoryStruct.comp (Y := (K.sc j).homologyData.right.Q)
          (Iso.hom
              (ShortComplex.RightHomologyData.opcyclesIso
                (ShortComplex.HomologyData.right (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
            (K.extend e).opcycles j' ⟶ (K.sc j).homologyData.right.Q)
          (Iso.inv (K.sc j).homologyData.right.opcyclesIso)))

Tactic:
rw [ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
dsimp :
  Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles
    (CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
      ((Iso.hom (K.extendXIso e hj') ≫ (K.sc j).homologyData.right.p) ≫
        Iso.inv (K.sc j).homologyData.right.opcyclesIso))
⊢ Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles
    (CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
      (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := (K.extend e).sc j')
          (ShortComplex.HomologyData.right (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData)))
        (ShortComplex.RightHomologyData.p
          (ShortComplex.HomologyData.right (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData)))
        (Iso.inv (K.sc j).homologyData.right.opcyclesIso)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
rw : Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles (K.sc' (c.prev j) j (c.next j)).pOpcycles
⊢ Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles
    (CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
      ((Iso.hom (K.extendXIso e hj') ≫ (K.sc j).homologyData.right.p) ≫
        Iso.inv (K.sc j).homologyData.right.opcyclesIso))

Tactic:
rw [assoc, Iso.inv_hom_id_assoc, ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles (K.sc' (c.prev j) j (c.next j)).pOpcycles

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := (K.extend e).X j' ⟶ K.opcycles j)
    (CategoryStruct.comp (Y := (K.extend e).opcycles j') ((K.extend e).pOpcycles j')
      (Iso.hom (K.extendOpcyclesIso e hj')))
    (Iso.hom (K.extendXIso e hj') ≫ K.pOpcycles j)

Tactic:
simp only [← cancel_mono (K.extendOpcyclesIso e hj').inv,
    assoc, Iso.hom_inv_id, comp_id, pOpcycles_extendOpcyclesIso_inv, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, HomologicalComplex.pOpcycles_extendOpcyclesIso_inv, HomologicalComplex.extendOpcyclesIso, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := (K.extend e).homology j' ⟶ K.opcycles j) (Iso.hom (K.extendHomologyIso e hj') ≫ K.homologyι j)
    ((K.extend e).homologyι j' ≫ Iso.hom (K.extendOpcyclesIso e hj'))

Tactic:
simp only [← cancel_epi ((K.extend e).homologyπ j'),
    homologyπ_extendHomologyIso_hom_assoc, homology_π_ι, extendCyclesIso_hom_iCycles_assoc,
    homology_π_ι_assoc, pOpcycles_extendOpcyclesIso_hom]

Premises used: HomologicalComplex.homologyπ, HomologicalComplex.extend, HomologicalComplex.homology_π_ι_assoc, HomologicalComplex.homologyπ_extendHomologyIso_hom_assoc, HomologicalComplex.pOpcycles_extendOpcyclesIso_hom, HomologicalComplex.homology_π_ι, HomologicalComplex.extendCyclesIso_hom_iCycles_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := K.homology j ⟶ (K.extend e).opcycles j') (Iso.inv (K.extendHomologyIso e hj') ≫ (K.extend e).homologyι j')
    (K.homologyι j ≫ Iso.inv (K.extendOpcyclesIso e hj'))

Tactic:
simp only [← cancel_epi (K.extendHomologyIso e hj').hom,
    Iso.hom_inv_id_assoc, extendHomologyIso_hom_homologyι_assoc, Iso.hom_inv_id, comp_id]

Premises used: HomologicalComplex.extendHomologyIso_hom_homologyι_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, HomologicalComplex.extendHomologyIso, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : L.HasHomology j
inst_5 : (K.extend e).HasHomology j'
inst_6 : (L.extend e).HasHomology j'
⊢ Eq (α := (K.extend e).cycles j' ⟶ L.cycles j)
    (CategoryStruct.comp (Y := (L.extend e).cycles j') (cyclesMap (extendMap φ e) j')
      (Iso.hom (L.extendCyclesIso e hj')))
    (CategoryStruct.comp (Y := K.cycles j) (Iso.hom (K.extendCyclesIso e hj')) (cyclesMap φ j))

Tactic:
simp [← cancel_mono (L.iCycles j), extendMap_f φ e hj']

Premises used: HomologicalComplex.extendMap_f, HomologicalComplex.iCycles, CategoryTheory.cancel_mono
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : L.HasHomology j
inst_5 : (K.extend e).HasHomology j'
inst_6 : (L.extend e).HasHomology j'
⊢ Eq (α := (K.extend e).homology j' ⟶ L.homology j)
    (CategoryStruct.comp (Y := (L.extend e).homology j') (homologyMap (extendMap φ e) j')
      (Iso.hom (L.extendHomologyIso e hj')))
    (CategoryStruct.comp (Y := K.homology j) (Iso.hom (K.extendHomologyIso e hj')) (homologyMap φ j))

Tactic:
simp [← cancel_epi ((K.extend e).homologyπ _)]

Premises used: HomologicalComplex.homologyπ, HomologicalComplex.extend, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : L.HasHomology j
inst_5 : (K.extend e).HasHomology j'
inst_6 : (L.extend e).HasHomology j'
simp :
  IsIso (X := (K.extend e).homology j') (Y := (L.extend e).homology j') (homologyMap (extendMap φ e) j') ↔
    IsIso (X := K.homology j) (Y := L.homology j) (homologyMap φ j)
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j' ↔ QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]

Premises used: quasiIsoAt_iff_isIso_homologyMap
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : L.HasHomology j
inst_5 : (K.extend e).HasHomology j'
inst_6 : (L.extend e).HasHomology j'
⊢ IsIso (X := (K.extend e).homology j') (Y := (L.extend e).homology j') (homologyMap (extendMap φ e) j') ↔
    IsIso (X := K.homology j) (Y := L.homology j) (homologyMap φ j)

Tactic:
(MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (K.extendHomologyIso e hj') (L.extendHomologyIso e hj'))

Premises used: CategoryTheory.MorphismProperty.isomorphisms, HomologicalComplex.extendHomologyIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : L.HasHomology j
inst_5 : (K.extend e).HasHomology j'
inst_6 : (L.extend e).HasHomology j'
⊢ IsIso (X := (K.extend e).homology j') (Y := (L.extend e).homology j') (homologyMap (extendMap φ e) j') ↔
    IsIso (X := K.homology j) (Y := L.homology j) (homologyMap φ j)

Tactic:
exact (MorphismProperty.isomorphisms C).arrow_mk_iso_iff
    (Arrow.isoMk (K.extendHomologyIso e hj') (L.extendHomologyIso e hj'))

Premises used: CategoryTheory.MorphismProperty.isomorphisms, HomologicalComplex.extendHomologyIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
simp :
  (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) ↔
    ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
⊢ QuasiIso (K := K.extend e) (extendMap φ e) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, ← fun j ↦ quasiIsoAt_extendMap_iff φ e (j := j) (hj' := rfl)]

Premises used: HomologicalComplex.quasiIsoAt_extendMap_iff, quasiIso_iff, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
mp :
  (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) →
    ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
mpr :
  (∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)) →
    ∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i
⊢ (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) ↔
    ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
mp mp₁ mp₂ mp₃ mp₄ mp₅ mp₆ mp₇ :
  (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) →
    ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
⊢ (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) →
    ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)

Tactic:
tauto