awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
pos : ∀ (hjk : c.Rel j k), (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
neg : ∀ (hjk : ¬c.Rel j k), (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0

Tactic:
by_cases hjk : c.Rel j k

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
pos :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
      (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
pos₁ :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (K.homologyι j' ≫
      CategoryStruct.comp (Y := (K.truncGE' e).X j) (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj))
        (Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    0
pos₂ :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (K.homologyι j' ≫ K.fromOpcycles j' (e.f k) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)) 0
pos₃ : Eq (α := K.homology j' ⟶ (K.truncGE' e).X k) (0 ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)) 0
pos₄ pos₅ : Eq.{v_1 + 1} (α := K.homology j' ⟶ (K.truncGE' e).X k) 0 0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0

Tactic:
rw [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj, assoc, Iso.inv_hom_id_assoc,
    homologyι_comp_fromOpcycles_assoc, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.homologyι_comp_fromOpcycles_assoc, HomologicalComplex.truncGE'_d_eq_fromOpcycles, CategoryTheory.Limits.zero_comp, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
neg :
  Eq (α := K.homology j' ⟶ (K.truncGE' e).X k)
    (CategoryStruct.comp (Y := (K.truncGE' e).X j) (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) 0) 0
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.homology j' ⟶ (K.truncGE' e).X k) 0 0
⊢ (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ≫ (K.truncGE' e).d j k = 0

Tactic:
rw [shape _ _ _ hjk, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ c'.next j' = e.f k

Tactic:
simpa only [hj'] using e.next_f hk

Premises used: ComplexShape.Embedding.next_f
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ c'.next j' = e.f k

Tactic:
have hk' : c'.next j' = e.f k := by simpa only [hj'] using e.next_f hk
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
pos :
  (hjk : c.Rel j k) →
    IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
      (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)
neg :
  (hjk : ¬c.Rel j k) →
    IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
      (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)
⊢ IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)

Tactic:
by_cases hjk : c.Rel j k

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : c.Rel j k
⊢ (parallelPair ((K.truncGE' e).d j k) 0).map WalkingParallelPairHom.left ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) =
    Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫
      (parallelPair (X := K.opcycles j') (Y := K.X (e.f k)) (K.fromOpcycles j' (e.f k)) 0).map
        WalkingParallelPairHom.left

Tactic:
simp [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj]

Premises used: HomologicalComplex.truncGE'_d_eq_fromOpcycles, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : c.Rel j k
⊢ (parallelPair ((K.truncGE' e).d j k) 0).map WalkingParallelPairHom.right ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) =
    Iso.hom (K.truncGE'XIsoOpcycles e hj' hj) ≫
      (parallelPair (X := K.opcycles j') (Y := K.X (e.f k)) (K.fromOpcycles j' (e.f k)) 0).map
        WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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_1 : c.Embedding c'
inst_2 : e_1.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e_1.f j = j'
hj : e_1.BoundaryGE j
hk' : c'.next j' = e_1.f k
hjk : c.Rel j k
e : parallelPair ((K.truncGE' e_1).d j k) 0 ≅
  parallelPair (X := K.opcycles j') (Y := K.X (e_1.f k)) (K.fromOpcycles j' (e_1.f k)) 0 :=
  parallelPair.ext (K.truncGE'XIsoOpcycles e_1 hj' hj) (K.truncGE'XIso e_1 ⋯ ⋯) ⋯ ⋯
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F := parallelPair (X := K.opcycles j') (Y := K.X (e_1.f k)) (K.fromOpcycles j' (e_1.f k)) 0)
            (KernelFork.ofι (K.homologyι j') ⋯))) ≫
      Fork.ι
        ((Cone.postcompose e.hom).obj
          (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e_1 hj' hj)) ⋯)) =
    Fork.ι (KernelFork.ofι (K.homologyι j') ⋯)

Tactic:
simp [e, Fork.ι]

Premises used: CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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_1 : c.Embedding c'
inst_2 : e_1.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e_1.f j = j'
hj : e_1.BoundaryGE j
hk' : c'.next j' = e_1.f k
hjk : c.Rel j k
e : parallelPair ((K.truncGE' e_1).d j k) 0 ≅
  parallelPair (X := K.opcycles j') (Y := K.X (e_1.f k)) (K.fromOpcycles j' (e_1.f k)) 0 :=
  parallelPair.ext (K.truncGE'XIsoOpcycles e_1 hj' hj) (K.truncGE'XIso e_1 ⋯ ⋯) ⋯ ⋯
⊢ IsLimit (F := parallelPair ((K.truncGE' e_1).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e_1 hj' hj)) ⋯)

Tactic:
exact (IsLimit.postcomposeHomEquiv e _).1
      (IsLimit.ofIsoLimit (K.homologyIsKernel _ _ hk')
      (Fork.ext (Iso.refl _) (by simp [e, Fork.ι])))

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Equiv.toFun, CategoryTheory.Limits.Fork.ext, HomologicalComplex.homologyIsKernel, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : ¬c.Rel j k
⊢ ¬c'.Rel j' (e.f k)

Tactic:
simpa only [← hj', e.rel_iff] using hjk

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : ¬c.Rel j k
⊢ IsIso (X := K.homology j') (K.homologyι j')

Tactic:
have := K.isIso_homologyι _ _ hk'
      (shape _ _ _ (by simpa only [← hj', e.rel_iff] using hjk))
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : ¬c.Rel j k
this : IsIso (X := K.homology j') (K.homologyι j')
⊢ IsLimit (F := parallelPair ((K.truncGE' e).d j k) 0)
    (KernelFork.ofι (K.homologyι j' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) ⋯)

Tactic:
exact IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (shape _ _ _ hjk))
      (Fork.ext ((truncGE'XIsoOpcycles K e hj' hj) ≪≫ (asIso (K.homologyι j')).symm))
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ ShortComplex.RightHomologyData.g' (ShortComplex.HomologyData.right (homologyData K e i j k hk hj' hj)) =
    (K.truncGE' e).d j k

Tactic:
rfl

Premises used: dite, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ShortComplex.RightHomologyData.descQ, rfl, HomologicalComplex.truncGE'.d, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i_1 j k : ι
hi : c.prev j = i_1
hk : c.next j = k
i : ι
pos : ∀ (hi : e.BoundaryGE i), (K.truncGE' e).HasHomology i
neg : ∀ (hi : ¬e.BoundaryGE i), (K.truncGE' e).HasHomology i
⊢ (K.truncGE' e).HasHomology i

Tactic:
by_cases hi : e.BoundaryGE i

Premises used: ComplexShape.Embedding.BoundaryGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i_1 j k : ι
hi_1 : c.prev j = i_1
hk : c.next j = k
i : ι
hi : e.BoundaryGE i
⊢ (K.truncGE' e).HasHomology i

Tactic:
ShortComplex.HasHomology.mk' (homologyData K e _ _ _ rfl rfl hi)

Premises used: HomologicalComplex.truncGE'.homologyData, CategoryTheory.ShortComplex.HasHomology.mk', rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i_1 j k : ι
hi_1 : c.prev j = i_1
hk : c.next j = k
i : ι
hi : e.BoundaryGE i
⊢ (K.truncGE' e).HasHomology i

Tactic:
exact ShortComplex.HasHomology.mk' (homologyData K e _ _ _ rfl rfl hi)

Premises used: HomologicalComplex.truncGE'.homologyData, CategoryTheory.ShortComplex.HasHomology.mk', rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i_1 j k : ι
hi_1 : c.prev j = i_1
hk : c.next j = k
i : ι
hi : ¬e.BoundaryGE i
⊢ (K.truncGE' e).HasHomology i

Tactic:
hasHomology_of_not_mem_boundary K e i hi

Premises used: HomologicalComplex.truncGE'.hasHomology_of_not_mem_boundary
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
i_1 j k : ι
hi_1 : c.prev j = i_1
hk : c.next j = k
i : ι
hi : ¬e.BoundaryGE i
⊢ (K.truncGE' e).HasHomology i

Tactic:
exact hasHomology_of_not_mem_boundary K e i hi

Premises used: HomologicalComplex.truncGE'.hasHomology_of_not_mem_boundary
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
i' : ι'
dsimp : ((K.truncGE' e).extend e).HasHomology i'
⊢ (K.truncGE e).HasHomology i'

Tactic:
dsimp [truncGE]

Premises used: HomologicalComplex.truncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
i' : ι'
⊢ ((K.truncGE' e).extend e).HasHomology i'

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
⊢ Eq (α :=
    K.X j' ⟶
      ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
        (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
          (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j') (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj)) :
      K.X j' ⟶
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
    (ShortComplex.Hom.τ₂ (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)) ≫
        ShortComplex.RightHomologyData.p
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))) :
      (Functor.obj (shortComplexFunctor C c' j') K).X₂ ⟶
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))

Tactic:
simp [truncGE'.homologyData, πTruncGE, e.liftExtend_f _ _ hj',
      K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e hj' hj]

Premises used: HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, HomologicalComplex.truncGE'.homologyData, ComplexShape.Embedding.liftExtend_f, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
rw : e.f k = c'.next (e.f j)
rw₁ rw₂ : e.f k = e.f k
⊢ e.f k = c'.next j'

Tactic:
rw [← hj', e.next_f hk]

Premises used: ComplexShape.Embedding.next_f
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
⊢ e.f k = c'.next j'

Tactic:
have hk' : e.f k = c'.next j' := by rw [← hj', e.next_f hk]
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
dsimp :
  Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := (K.truncGE' e).sc' i j k)
          (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))
        (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) : K.opcycles j' ⟶ (K.truncGE' e).X j)
        (ShortComplex.RightHomologyData.g'
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))) :
      (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫ Hom.f (K.πTruncGE e) (c'.next j') :
      (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
⊢ Eq (α :=
    (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
      (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
    (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj))))
        (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) : K.opcycles j' ⟶ (K.truncGE' e).X j)
        (ShortComplex.RightHomologyData.g'
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))) :
      (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
        (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)
    ((ShortComplex.RightHomologyData.canonical (K.sc j')).g' ≫
        ShortComplex.Hom.τ₃ (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)) :
      (ShortComplex.RightHomologyData.canonical (K.sc j')).Q ⟶
        (Functor.obj (shortComplexFunctor C c' j') (K.truncGE e)).X₃)

Tactic:
dsimp