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 : 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'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (CategoryStruct.comp (Y := K.opcycles (e.f i)) (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi))
      (K.fromOpcycles (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'.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' ⋯)))

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'.XIsoOpcycles K e hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (truncGE'.XIso K e ⋯))
    (CategoryStruct.comp (Y := K.opcycles (e.f i)) (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi))
      (K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))

Tactic:
simp [truncGE'XIso, truncGE'XIsoOpcycles]

Premises used: HomologicalComplex.truncGE'XIso, 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'
i j : ι
hij : c.Rel i j
rw :
  (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫
      if hi : e.BoundaryGE j then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f j) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)

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

Premises used: 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 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 j : ι
hij : c.Rel i j
pos :
  ∀ (hi : e.BoundaryGE i),
    (if hi : e.BoundaryGE i then
          Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
        else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
        (L.truncGE' e).d i j =
      (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
neg :
  ∀ (hi : ¬e.BoundaryGE i),
    (if hi : e.BoundaryGE i then
          Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
        else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
        (L.truncGE' e).d i j =
      (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)

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'
i j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
pos :
  (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)

Tactic:
rw [dif_pos hi]

Premises used: dif_pos
-- 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 j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)

Tactic:
simp [truncGE'_d_eq_fromOpcycles _ e hij rfl rfl hi,
        ← cancel_epi (K.pOpcycles (e.f i))]

Premises used: HomologicalComplex.truncGE'_d_eq_fromOpcycles, ComplexShape.Embedding.f, HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi, 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 j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
neg :
  (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫ (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)
⊢ (if hi : e.BoundaryGE i then
        Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫
      (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)

Tactic:
rw [dif_neg hi]

Premises used: 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 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 j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi)) ≫ (L.truncGE' e).d i j =
    (K.truncGE' e).d i j ≫ Iso.hom (K.truncGE'XIso e ⋯ ⋯) ≫ φ.f (e.f j) ≫ Iso.inv (L.truncGE'XIso e ⋯ ⋯)

Tactic:
simp [truncGE'_d_eq _ e hij rfl rfl hi]

Premises used: HomologicalComplex.truncGE'_d_eq, 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 : 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 : ι
hi : e.BoundaryGE i
i' : ι'
h : e.f i = i'
subst :
  Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi))
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIsoOpcycles e h hi) ≫ opcyclesMap φ i' ≫ Iso.inv (L.truncGE'XIsoOpcycles e h hi))

Tactic:
subst h
-- 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'
i : ι
hi : e.BoundaryGE i
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi))

Tactic:
dif_pos hi

Premises used: dif_pos, dite
-- 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'
i : ι
hi : e.BoundaryGE i
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ opcyclesMap φ (e.f i) ≫ Iso.inv (L.truncGE'XIsoOpcycles e ⋯ hi))

Tactic:
exact dif_pos hi

Premises used: dif_pos
-- 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'
i : ι
hi : ¬e.BoundaryGE i
i' : ι'
h : e.f i = i'
subst :
  Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi))
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIso e h hi) ≫ φ.f i' ≫ Iso.inv (L.truncGE'XIso e h hi))

Tactic:
subst h
-- 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'
i : ι
hi : ¬e.BoundaryGE i
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi))

Tactic:
dif_neg hi

Premises used: dif_neg, dite
-- 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'
i : ι
hi : ¬e.BoundaryGE i
⊢ Eq (α := (K.truncGE' e).X i ⟶ (L.truncGE' e).X i) (Hom.f (truncGE'Map φ e) i)
    (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ φ.f (e.f i) ≫ Iso.inv (L.truncGE'XIso e ⋯ hi))

Tactic:
exact dif_neg hi

Premises used: 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'
h : ∀ (i : ι), Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
⊢ truncGE'Map (𝟙 K) e = 𝟙 (K.truncGE' e)

Tactic:
ext 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
pos : ∀ (hi : e.BoundaryGE i), Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
neg : ∀ (hi : ¬e.BoundaryGE i), Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i
⊢ Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i

Tactic:
simp [truncGE'Map_f_eq_opcyclesMap _ _ hi rfl]

Premises used: HomologicalComplex.truncGE'Map_f_eq_opcyclesMap, 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 : ι
hi : ¬e.BoundaryGE i
⊢ Hom.f (truncGE'Map (𝟙 K) e) i = Hom.f (𝟙 (K.truncGE' e)) i

Tactic:
simp [truncGE'Map_f_eq _ _ hi rfl]

Premises used: HomologicalComplex.truncGE'Map_f_eq, 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'
h :
  ∀ (i : ι),
    Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
      (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
⊢ Eq (α := K.truncGE' e ⟶ M.truncGE' e) (truncGE'Map (φ ≫ φ') e)
    (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e))

Tactic:
ext 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'
i : ι
pos :
  ∀ (hi : e.BoundaryGE i),
    Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
      (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
neg :
  ∀ (hi : ¬e.BoundaryGE i),
    Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
      (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)
⊢ Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) 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'
i : ι
hi : e.BoundaryGE i
⊢ Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)

Tactic:
simp [truncGE'Map_f_eq_opcyclesMap _ _ hi rfl, opcyclesMap_comp]

Premises used: HomologicalComplex.opcyclesMap_comp, HomologicalComplex.truncGE'Map_f_eq_opcyclesMap, 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 : ι
hi : ¬e.BoundaryGE i
⊢ Eq (α := (K.truncGE' e).X i ⟶ (M.truncGE' e).X i) (Hom.f (truncGE'Map (φ ≫ φ') e) i)
    (Hom.f (CategoryStruct.comp (Y := L.truncGE' e) (truncGE'Map φ e) (truncGE'Map φ' e)) i)

Tactic:
simp [truncGE'Map_f_eq _ _ hi rfl]

Premises used: HomologicalComplex.truncGE'Map_f_eq, 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'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ truncGEMap (𝟙 K) e = 𝟙 (K.truncGE e)

Tactic:
simp [truncGEMap, truncGE]

Premises used: HomologicalComplex.truncGE, HomologicalComplex.truncGEMap
-- 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
⊢ Eq (α := K.truncGE e ⟶ M.truncGE e) (truncGEMap (φ ≫ φ') e)
    (CategoryStruct.comp (Y := L.truncGE e) (truncGEMap φ e) (truncGEMap φ' e))

Tactic:
simp [truncGEMap, truncGE]

Premises used: HomologicalComplex.truncGE, HomologicalComplex.truncGEMap
-- 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 : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
dsimp :
  Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (if hi : e.BoundaryGE i then K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.inv (K.truncGE'XIso e ⋯ hi) :
      K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi) :
      K.X (e.f i) ⟶ (K.truncGE' e).X i)
⊢ Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X i) (f K e i)
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi))

Tactic:
dsimp [f]

Premises used: HomologicalComplex.restrictionToTruncGE'.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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
rw :
  Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi))
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (if hi : e.BoundaryGE i then K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi)
      else Iso.inv (K.truncGE'XIso e ⋯ hi) :
      K.X (e.f i) ⟶ (K.truncGE' e).X i)
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi) :
      K.X (e.f i) ⟶ (K.truncGE' e).X i)

Tactic:
rw [dif_pos hi]

Premises used: dif_pos
-- 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 : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
subst :
  Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
    (Iso.hom (K.restrictionXIso e ⋯) ≫ K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi))

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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
    (Iso.hom (K.restrictionXIso e ⋯) ≫ K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso