awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      (K.sc j).homologyData.left.i ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj')))
⊢ Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      CategoryStruct.comp (Y := (K.extend e).X j') ((K.sc j).homologyData.left.i ≫ Iso.inv (K.extendXIso e hj'))
        (Iso.hom (K.extendXIso e hj')))
have rw₁ : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
  (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.i ≫ 𝟙 (K.X j))
Tactic: rw [assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      (K.sc j).homologyData.left.i ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj')))
rw₁ :
  Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.i ≫ 𝟙 (K.X j))
⊢ Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      CategoryStruct.comp (Y := (K.extend e).X j') ((K.sc j).homologyData.left.i ≫ Iso.inv (K.extendXIso e hj'))
        (Iso.hom (K.extendXIso e hj')))
have rw₂ : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
  (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.i)
Tactic: rw [assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      (K.sc j).homologyData.left.i ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj')))
rw₁ :
  Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.i ≫ 𝟙 (K.X j))
rw₂ :
  Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫ (K.sc j).homologyData.left.i)
⊢ Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      CategoryStruct.comp (Y := (K.extend e).X j') ((K.sc j).homologyData.left.i ≫ Iso.inv (K.extendXIso e hj'))
        (Iso.hom (K.extendXIso e hj')))
have rw₃ : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles (K.sc j).iCycles
Tactic: rw [assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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).cycles j' ⟶ K.homology j) ((K.extend e).homologyπ j' ≫ Iso.hom (K.extendHomologyIso e hj'))
    (Iso.hom (K.extendCyclesIso e hj') ≫ K.homologyπ j)
have dsimp : 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' sorry sorry (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: dsimp [extendHomologyIso, homologyπ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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).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)
have 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' sorry sorry (K.sc j).homologyData)))
      (Iso.hom
        (ShortComplex.LeftHomologyData.cyclesIso
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' sorry sorry (K.sc j).homologyData))))
      (ShortComplex.LeftHomologyData.π
        (ShortComplex.HomologyData.left (extend.homologyData' K e hj' sorry sorry (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: 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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)
    (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)
have 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' sorry sorry (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' sorry sorry (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: dsimp [extendCyclesIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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.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')
have 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')))
Tactic: rw [← cancel_mono (K.extendOpcyclesIso e hj').hom, assoc, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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.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')))
have 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' sorry sorry (K.sc j).homologyData))) :
          (K.extend e).opcycles j' ⟶ (K.sc j).homologyData.right.Q)
        (Iso.inv (K.sc j).homologyData.right.opcyclesIso)))
Tactic: dsimp [extendOpcyclesIso, pOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
    (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)))
have 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' sorry sorry (K.sc j).homologyData)))
      (ShortComplex.RightHomologyData.p
        (ShortComplex.HomologyData.right (extend.homologyData' K e hj' sorry sorry (K.sc j).homologyData)))
      (Iso.inv (K.sc j).homologyData.right.opcyclesIso)))
Tactic: rw [ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
    (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)))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
    (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))
have rw : Eq (α := K.X j ⟶ K.opcycles j) (K.sc j).pOpcycles (K.sc' (c.prev j) j (c.next j)).pOpcycles
Tactic: rw [assoc, Iso.inv_hom_id_assoc, ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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'
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j' ↔ QuasiIsoAt φ j
have 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)
Tactic: simp only [quasiIsoAt_iff_isIso_homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
⊢ QuasiIso (K := K.extend e) (extendMap φ e) ↔ QuasiIso φ
have simp : (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) ↔
  ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
Tactic: simp only [quasiIso_iff, ← fun j ↦ quasiIsoAt_extendMap_iff φ e (j := j) (hj' := rfl)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
⊢ (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) ↔
    ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
have mp : (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) →
  ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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)
⊢ (∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i) ↔
    ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
have mpr : (∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)) →
  ∀ (i : ι'), QuasiIsoAt (K := K.extend e) (extendMap φ e) i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
have pos : ∀ (hj' : ∃ (j : ι), e.f j = j'), QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
pos : ∀ (hj' : ∃ (j : ι), e.f j = j'), QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
have neg : ∀ (hj' : ¬∃ (j : ι), e.f j = j'), QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ (j : ι), e.f j = j'
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
have neg : (L.extend e).ExactAt j'
Tactic: rw [quasiIsoAt_iff_exactAt]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (goal)
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
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ (j : ι), e.f j = j'
neg : (L.extend e).ExactAt j'
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
have neg₁ : (K.extend e).ExactAt j'
Tactic: rw [quasiIsoAt_iff_exactAt]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : (i j : ι) → K.X i ⟶ L.X j
i' j' : Option ι
i j : ι
hi : i' = some i
hj : j' = some j
⊢ Eq (α := extend.X K i' ⟶ extend.X L j') (homAux φ i' j')
    (Iso.hom (extend.XIso K hi) ≫ φ i j ≫ Iso.inv (extend.XIso L hj))
have subst : Eq (α := extend.X K (some i) ⟶ extend.X L (some j)) (homAux φ (some i) (some j))
  (Iso.hom (extend.XIso K sorry) ≫ φ i j ≫ Iso.inv (extend.XIso L sorry))
Tactic: subst hi hj
Cleared hypotheses: i', j', hi, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' j' : ι'
hij' : ¬c'.Rel j' i'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' j' : ι'
hij' : ¬c'.Rel j' i'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' j' : ι'
hij' : ¬c'.Rel j' i'
hi' : ∃ (i : ι), e.f i = i'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
have pos : ∀ (i : ι) (hij' : ¬c'.Rel j' (e.f i)),
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0
Tactic: obtain ⟨i, rfl⟩ := hi'
Cleared hypotheses: i', hij', hi'