awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc
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 M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : e.IsRelIff
⊢ Eq (α := K.stupidTrunc e ⟶ M.stupidTrunc e) (stupidTruncMap (φ ≫ φ') e) (stupidTruncMap φ e ≫ stupidTruncMap φ' e)

Tactic:
simp [stupidTruncMap, stupidTrunc]

Premises used: HomologicalComplex.stupidTrunc, HomologicalComplex.stupidTruncMap
-- Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc
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_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
i' : ι'
hi : e.f i = i'
subst :
  Eq (α := (K.stupidTrunc e).X (e.f i) ⟶ L.X (e.f i))
    (Hom.f (stupidTruncMap φ e) (e.f i) ≫ Iso.hom (L.stupidTruncXIso e ⋯))
    (Iso.hom (K.stupidTruncXIso e ⋯) ≫ φ.f (e.f i))
⊢ Eq (α := (K.stupidTrunc e).X i' ⟶ L.X i') (Hom.f (stupidTruncMap φ e) i' ≫ Iso.hom (L.stupidTruncXIso e hi))
    (Iso.hom (K.stupidTruncXIso e hi) ≫ φ.f i')

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc
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_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
⊢ Eq (α := (K.stupidTrunc e).X (e.f i) ⟶ L.X (e.f i))
    (Hom.f (stupidTruncMap φ e) (e.f i) ≫ Iso.hom (L.stupidTruncXIso e ⋯))
    (Iso.hom (K.stupidTruncXIso e ⋯) ≫ φ.f (e.f i))

Tactic:
simp [stupidTruncMap, stupidTruncXIso, extendMap_f _ _ rfl]

Premises used: HomologicalComplex.extendMap_f, HomologicalComplex.stupidTruncXIso, HomologicalComplex.stupidTruncMap, 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 : 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 : ι
dsimp :
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
⊢ Eq (α := X K e i ⟶ X K e k) (d K e i j ≫ d K e j k) 0

Tactic:
dsimp [d]

Premises used: HomologicalComplex.truncGE'.d
-- 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 : 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 : ι
pos :
  ∀ (hij : c.Rel i j),
    Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (if hij : c.Rel i j then
          if hi : e.BoundaryGE i then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else 0)
        (if hij : c.Rel j k then
          if hi : e.BoundaryGE j then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else 0))
      0
neg :
  ∀ (hij : ¬c.Rel i j),
    Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (if hij : c.Rel i j then
          if hi : e.BoundaryGE i then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else 0)
        (if hij : c.Rel j k then
          if hi : e.BoundaryGE j then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else 0))
      0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- 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 : 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 : ι
hij : c.Rel i j
pos :
  ∀ (hjk : c.Rel j k),
    Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (if hij : c.Rel i j then
          if hi : e.BoundaryGE i then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else 0)
        (if hij : c.Rel j k then
          if hi : e.BoundaryGE j then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else 0))
      0
neg :
  ∀ (hjk : ¬c.Rel j k),
    Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (if hij : c.Rel i j then
          if hi : e.BoundaryGE i then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else 0)
        (if hij : c.Rel j k then
          if hi : e.BoundaryGE j then
            Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
          else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else 0))
      0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0

Tactic:
by_cases hjk : c.Rel j k

Premises used: ComplexShape.Rel
-- 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 : 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 : ι
hij : c.Rel i j
hjk : c.Rel j k
pos :
  Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hi : e.BoundaryGE i then Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
      (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
    0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0

Tactic:
rw [dif_pos hij, dif_pos hjk, dif_neg (e.not_boundaryGE_next hij)]

Premises used: dif_pos, dif_neg, ComplexShape.Embedding.not_boundaryGE_next
-- 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 : 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 : ι
hij : c.Rel i j
hjk : c.Rel j k
pos :
  ∀ (h : e.BoundaryGE i),
    Eq (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j)
        (Iso.hom (XIsoOpcycles K e h) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
        (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
      0
neg :
  ∀ (h : ¬e.BoundaryGE i),
    Eq (α := X K e i ⟶ X K e k)
      (CategoryStruct.comp (Y := X K e j) (Iso.hom (XIso K e h) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
        (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
      0
⊢ Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hi : e.BoundaryGE i then Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
      (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
    0

Tactic:
split_ifs
-- 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 : 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 : ι
hij : c.Rel i j
hjk : c.Rel j k
h : e.BoundaryGE i
⊢ Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (Iso.hom (XIsoOpcycles K e h) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
      (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
    0

Tactic:
simp
-- 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 : 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 : ι
hij : c.Rel i j
hjk : c.Rel j k
h : ¬e.BoundaryGE i
⊢ Eq (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j) (Iso.hom (XIso K e h) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯))
      (Iso.hom (XIso K e ⋯) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)))
    0

Tactic:
simp
-- 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 : 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 : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
neg :
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      0)
    0
neg₁ neg₂ : Eq.{v_1 + 1} (α := X K e i ⟶ X K e k) 0 0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0

Tactic:
rw [dif_neg hjk, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, dif_neg
-- 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 : 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 : ι
hij : ¬c.Rel i j
neg :
  Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j) 0
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0
neg₁ neg₂ : Eq.{v_1 + 1} (α := X K e i ⟶ X K e k) 0 0
⊢ Eq.{v_1 + 1} (α := X K e i ⟶ X K e k)
    (CategoryStruct.comp (Y := X K e j)
      (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (XIso K e ⋯)
      else 0)
      (if hij : c.Rel j k then
        if hi : e.BoundaryGE j then
          Iso.hom (XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
        else Iso.hom (XIso K e hi) ≫ K.d (e.f j) (e.f k) ≫ Iso.inv (XIso K e ⋯)
      else 0))
    0

Tactic:
rw [dif_neg hij, zero_comp]

Premises used: dif_neg, CategoryTheory.Limits.zero_comp
-- 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'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
subst : K.X (e.f i) = K.X (e.f i)
⊢ K.X (e.f i) = K.X i'

Tactic:
subst 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'
i : ι
hi : ¬e.BoundaryGE i
⊢ K.X (e.f i) = K.X (e.f i)

Tactic:
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'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
subst : K.opcycles (e.f i) = K.opcycles (e.f i)
⊢ K.opcycles (e.f i) = K.opcycles i'

Tactic:
subst 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'
i : ι
hi : e.BoundaryGE i
⊢ K.opcycles (e.f i) = K.opcycles (e.f i)

Tactic:
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 : 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 : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : ¬e.BoundaryGE i
dsimp :
  Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
        else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
      else 0 :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯) :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
⊢ (K.truncGE' e).d i j = Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)

Tactic:
dsimp [truncGE', truncGE'.d]

Premises used: HomologicalComplex.truncGE', HomologicalComplex.truncGE'.d
-- 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 : 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 : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : ¬e.BoundaryGE i
rw :
  Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯))
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
        else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
      else 0 :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯) :
      truncGE'.X K e i ⟶ truncGE'.X K e j)

Tactic:
rw [dif_pos hij, dif_neg hi]

Premises used: dif_pos, dif_neg
-- 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 : 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 : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : ¬e.BoundaryGE i
subst :
  Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯))
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (Iso.hom (K.truncGE'XIso e hi' hi) ≫ K.d i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯))

Tactic:
subst hi' hj'
-- 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 : 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 : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯))

Tactic:
simp [truncGE'XIso]

Premises used: HomologicalComplex.truncGE'XIso
-- 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 : 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 : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : e.BoundaryGE i
dsimp :
  Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
        else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
      else 0 :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
    (CategoryStruct.comp (Y := K.opcycles i') (Iso.hom (K.truncGE'XIsoOpcycles e hi' hi))
        (K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)) :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
⊢ (K.truncGE' e).d i j =
    Iso.hom (K.truncGE'XIsoOpcycles e hi' hi) ≫ K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)

Tactic:
dsimp [truncGE', truncGE'.d]

Premises used: HomologicalComplex.truncGE', HomologicalComplex.truncGE'.d
-- 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 : 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 : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : e.BoundaryGE i
rw :
  Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (CategoryStruct.comp (Y := K.opcycles i') (Iso.hom (K.truncGE'XIsoOpcycles e hi' hi))
      (K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)))
⊢ Eq (α := truncGE'.X K e i ⟶ truncGE'.X K e j)
    (if hij : c.Rel i j then
        if hi : e.BoundaryGE i then
          Iso.hom (truncGE'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
        else Iso.hom (truncGE'.XIso K e hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯)
      else 0 :
      truncGE'.X K e i ⟶ truncGE'.X K e j)
    (CategoryStruct.comp (Y := K.opcycles i') (Iso.hom (K.truncGE'XIsoOpcycles e hi' hi))
        (K.fromOpcycles i' j' ≫ Iso.inv (K.truncGE'XIso e hj' ⋯)) :
      truncGE'.X K e i ⟶ truncGE'.X K e j)

Tactic:
rw [dif_pos hij, dif_pos hi]

Premises used: dif_pos