awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
⊢ c'.Rel (c'.prev (e.f i)) (e.f i)

Tactic:
obtain ⟨hi₁, hi₂⟩ := hi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
hi₁ : c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ ∀ (i_1 : ι), ¬c'.Rel (e.f i_1) (e.f i)

Tactic:
obtain ⟨hi₁, hi₂⟩ := hi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi₁ : c'.Rel (c'.prev (e.f i)) (e.f i)
hi₂ : ∀ (i_1 : ι), ¬c'.Rel (e.f i_1) (e.f i)
j : ι
hj : e.f j = c'.prev (e.f i)
⊢ c'.Rel (e.f j) (e.f i)

Tactic:
simpa only [hj] using hi₁
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi₁ : c'.Rel (c'.prev (e.f i)) (e.f i)
hi₂ : ∀ (i_1 : ι), ¬c'.Rel (e.f i_1) (e.f i)
⊢ Eq (α := K.X (c'.prev (e.f i)) ⟶ K.X (e.f i)) (K.d (c'.prev (e.f i)) (e.f i)) 0

Tactic:
apply IsZero.eq_of_src (K.isZero_X_of_isStrictlySupported e _
        (fun j hj ↦ hi₂ j (by simpa only [hj] using hi₁)))

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, HomologicalComplex.isZero_X_of_isStrictlySupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
⊢ IsIso (X := K.X (e.f i)) (Y := K.opcycles (e.f i)) (K.pOpcycles (e.f i))

Tactic:
have : IsIso (K.pOpcycles (e.f i)) := K.isIso_pOpcycles _ _ rfl (by
      obtain ⟨hi₁, hi₂⟩ := hi
      apply IsZero.eq_of_src (K.isZero_X_of_isStrictlySupported e _
        (fun j hj ↦ hi₂ j (by simpa only [hj] using hi₁))))
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
this : IsIso (X := K.X (e.f i)) (Y := K.opcycles (e.f i)) (K.pOpcycles (e.f i))
⊢ IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e ⋯) ≫ K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi : ¬e.BoundaryGE i
neg :
  IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ hi))
⊢ IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)

Tactic:
rw [K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi]

Premises used: HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_iso_inv, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : K.IsStrictlySupported e
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ hi))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Epi (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), Epi (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
⊢ Epi (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι) (hi : e.f i = i'), Epi (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
⊢ Epi (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')

Tactic:
obtain ⟨i, hi⟩ := hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i' : ι'
i : ι
hi : e.f i = i'
pos : Epi (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
⊢ Epi (Y := (K.truncGE e).X i') (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) i')

Tactic:
rw [e.epi_liftExtend_f_iff _ _ hi]

Premises used: ComplexShape.Embedding.epi_liftExtend_f_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i' : ι'
i : ι
hi : e.f i = i'
⊢ Epi (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ Epi (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')

Tactic:
apply (isZero_extend_X _ _ _ (by simpa using hi')).epi

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.epi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
⊢ Epi (Y := K.truncGE e) (K.πTruncGE e)

Tactic:
epi_of_epi_f _ (fun _ => inferInstance)

Premises used: inferInstance, HomologicalComplex.epi_of_epi_f
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
⊢ ((K.truncGE' e).extend e).IsStrictlySupported e

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
a :
  Eq (α := { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
    ((e.homEquiv K (L.truncGE' e) :
          (a : K ⟶ (L.truncGE' e).extend e) → { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
        (CategoryStruct.comp (Y := K.truncGE e) (K.πTruncGE e) (truncGEMap φ e)) :
      { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
    ((e.homEquiv K (L.truncGE' e) :
          (a : K ⟶ (L.truncGE' e).extend e) → { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
        (φ ≫ L.πTruncGE e) :
      { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
⊢ Eq (α := K ⟶ L.truncGE e) (CategoryStruct.comp (Y := K.truncGE e) (K.πTruncGE e) (truncGEMap φ e)) (φ ≫ L.πTruncGE e)

Tactic:
apply (e.homEquiv _ _).injective

Premises used: ComplexShape.Embedding.homEquiv, Equiv.injective
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
a :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (↑((e.homEquiv K (L.truncGE' e) :
            (a : K ⟶ (L.truncGE' e).extend e) → { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
          (CategoryStruct.comp (Y := K.truncGE e) (K.πTruncGE e) (truncGEMap φ e))) :
      K.restriction e ⟶ L.truncGE' e)
    (↑((e.homEquiv K (L.truncGE' e) :
            (a : K ⟶ (L.truncGE' e).extend e) → { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
          (φ ≫ L.πTruncGE e)) :
      K.restriction e ⟶ L.truncGE' e)
⊢ Eq (α := { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
    ((e.homEquiv K (L.truncGE' e) :
          (a : K ⟶ (L.truncGE' e).extend e) → { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
        (CategoryStruct.comp (Y := K.truncGE e) (K.πTruncGE e) (truncGEMap φ e)) :
      { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
    ((e.homEquiv K (L.truncGE' e) :
          (a : K ⟶ (L.truncGE' e).extend e) → { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })
        (φ ≫ L.πTruncGE e) :
      { φ : K.restriction e ⟶ L.truncGE' e // e.HasLift φ })

Tactic:
ext1
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
a :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (e.homRestrict (e.liftExtend (K.restrictionToTruncGE' e) ⋯))
      (truncGE'Map φ e))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₁ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₂ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (restrictionMap φ e ≫ e.homRestrict (e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₃ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (restrictionMap φ e ≫ L.restrictionToTruncGE' e)
a₄ a₅ :
  Eq (α := K.restriction e ⟶ L.truncGE' e) (restrictionMap φ e ≫ L.restrictionToTruncGE' e)
    (restrictionMap φ e ≫ L.restrictionToTruncGE' e)
⊢ Eq (α := K.restriction e ⟶ L.truncGE' e)
    (e.homRestrict
      (CategoryStruct.comp (Y := K.truncGE e) (e.liftExtend (K.restrictionToTruncGE' e) ⋯)
        (extendMap (truncGE'Map φ e) e)))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))

Tactic:
rw [e.homRestrict_comp_extendMap, e.homRestrict_liftExtend, e.homRestrict_precomp,
    e.homRestrict_liftExtend, restrictionToTruncGE'_naturality]

Premises used: ComplexShape.Embedding.homRestrict_precomp, ComplexShape.Embedding.homRestrict_liftExtend, HomologicalComplex.restrictionToTruncGE'_naturality, ComplexShape.Embedding.homRestrict_comp_extendMap
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
pos : ∀ (hi'' : ∃ (i : ι), e.f i = i'), IsZero.{v_1, u_3} ((K.truncGE e).X i')
neg : ∀ (hi'' : ¬∃ (i : ι), e.f i = i'), IsZero.{v_1, u_3} ((K.truncGE e).X i')
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')

Tactic:
by_cases hi'' : ∃ i, e.f i = i'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι) (hi : e.f i = i'), IsZero.{v_1, u_3} ((K.truncGE e).X i')
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')

Tactic:
obtain ⟨i, hi⟩ := hi''
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
pos : ∀ (hi''' : e.BoundaryGE i), IsZero.{v_1, u_3} ((K.truncGE e).X i')
neg : ∀ (hi''' : ¬e.BoundaryGE i), IsZero.{v_1, u_3} ((K.truncGE e).X i')
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')

Tactic:
by_cases hi''' : e.BoundaryGE i

Premises used: ComplexShape.Embedding.BoundaryGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
hi''' : e.BoundaryGE i
pos :
  K.pOpcycles i' ≫
      Iso.inv ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''') ≫ 𝟙 ((K.truncGE e).X i') =
    K.pOpcycles i' ≫
      CategoryStruct.comp (Y := ((K.truncGE' e).extend e).X i')
        (Iso.inv ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''')) 0
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_epi
          ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''').inv,
          ← cancel_epi (HomologicalComplex.pOpcycles _ _)]

Premises used: CategoryTheory.Iso.trans, HomologicalComplex.truncGE', HomologicalComplex.pOpcycles, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi, HomologicalComplex.extendXIso, CategoryTheory.Iso.inv, HomologicalComplex.truncGE'XIsoOpcycles
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
hi''' : e.BoundaryGE i
⊢ K.pOpcycles i' ≫
      Iso.inv ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''') ≫ 𝟙 ((K.truncGE e).X i') =
    K.pOpcycles i' ≫
      CategoryStruct.comp (Y := ((K.truncGE' e).extend e).X i')
        (Iso.inv ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''')) 0

Tactic:
apply (K.isZero_X_of_isStrictlySupported e' i' hi').eq_of_src

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, HomologicalComplex.isZero_X_of_isStrictlySupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
hi''' : ¬e.BoundaryGE i
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')

Tactic:
(K.isZero_X_of_isStrictlySupported e' i' hi').of_iso
          ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIso e hi hi''')

Premises used: HomologicalComplex.truncGE'XIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.trans, HomologicalComplex.truncGE', HomologicalComplex.isZero_X_of_isStrictlySupported, HomologicalComplex.extendXIso
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
hi''' : ¬e.BoundaryGE i
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')

Tactic:
exact (K.isZero_X_of_isStrictlySupported e' i' hi').of_iso
          ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIso e hi hi''')

Premises used: HomologicalComplex.truncGE'XIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Iso.trans, HomologicalComplex.truncGE', HomologicalComplex.isZero_X_of_isStrictlySupported, HomologicalComplex.extendXIso
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGE
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
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ (i : ι), e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi''