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 : ι
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') ≫ Iso.inv (K.truncGE'XIso 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') ≫ Iso.inv (K.truncGE'XIso 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) (Iso.inv (K.truncGE'XIso e ⋯ hi))
    (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso 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') ≫ Iso.inv (K.truncGE'XIso e hi' hi) : K.X (e.f i) ⟶ (K.truncGE' e).X i)

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 : 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) (Iso.inv (K.truncGE'XIso e ⋯ hi))
    (Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ hi))
⊢ Eq (α := K.X (e.f i) ⟶ (K.truncGE' e).X i) (Iso.inv (K.truncGE'XIso e ⋯ hi))
    (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso 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) (Iso.inv (K.truncGE'XIso e ⋯ hi))
    (Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ hi))

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- 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 : ι
pos : ∀ (hij : c.Rel i j), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
neg : ∀ (hij : ¬c.Rel i j), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

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 : ι
hij : c.Rel i j
pos : ∀ (hi : e.BoundaryGE i), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
neg : ∀ (hi : ¬e.BoundaryGE i), f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

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 j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
pos :
  Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X j)
    (CategoryStruct.comp (Y := (K.truncGE' e).X i)
      (Iso.hom (K.restrictionXIso e ⋯) ≫ K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
      (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    ((K.restriction e).d i j ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯))
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
rw [f_eq_iso_hom_pOpcycles_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq_fromOpcycles e hij rfl rfl hi]

Premises used: HomologicalComplex.truncGE'_d_eq_fromOpcycles, HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_iso_inv, ComplexShape.Embedding.not_boundaryGE_next, 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
hi : e.BoundaryGE i
⊢ Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X j)
    (CategoryStruct.comp (Y := (K.truncGE' e).X i)
      (Iso.hom (K.restrictionXIso e ⋯) ≫ K.pOpcycles (e.f i) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hi))
      (Iso.hom (K.truncGE'XIsoOpcycles e ⋯ hi) ≫ K.fromOpcycles (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    ((K.restriction e).d i j ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯))

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- 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
neg :
  Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X j)
    (CategoryStruct.comp (Y := (K.truncGE' e).X i) (Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ hi))
      (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    ((K.restriction e).d i j ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯))
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
rw [f_eq_iso_hom_iso_inv K e rfl hi,
        f_eq_iso_hom_iso_inv K e rfl (e.not_boundaryGE_next hij),
        K.truncGE'_d_eq e hij rfl rfl hi]

Premises used: HomologicalComplex.truncGE'_d_eq, HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_iso_inv, ComplexShape.Embedding.not_boundaryGE_next, 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
hi : ¬e.BoundaryGE i
⊢ Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X j)
    (CategoryStruct.comp (Y := (K.truncGE' e).X i) (Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ hi))
      (Iso.hom (K.truncGE'XIso e ⋯ hi) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯)))
    ((K.restriction e).d i j ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ Iso.inv (K.truncGE'XIso e ⋯ ⋯))

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- 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
⊢ f K e i ≫ (K.truncGE' e).d i j = (K.restriction e).d i j ≫ f K e j

Tactic:
simp [HomologicalComplex.shape _ _ _ hij]

Premises used: HomologicalComplex.shape
-- 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'
j : ι
hj : e.BoundaryGE j
i' : ι'
_ : c'.Rel i' (e.f j) → Eq (α := K.X i' ⟶ (K.truncGE' e).X j) (K.d i' (e.f j) ≫ Hom.f (K.restrictionToTruncGE' e) j) 0
⊢ c'.Rel i' (e.f j) → Eq (α := K.X i' ⟶ (K.truncGE' e).X j) (K.d i' (e.f j) ≫ Hom.f (K.restrictionToTruncGE' e) j) 0

Tactic:
_
-- 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'
j : ι
hj : e.BoundaryGE j
i' : ι'
h : c'.Rel i' (e.f j)
dsimp : Eq (α := K.X i' ⟶ (K.truncGE' e).X j) (K.d i' (e.f j) ≫ restrictionToTruncGE'.f K e j) 0
⊢ Eq (α := K.X i' ⟶ (K.truncGE' e).X j) (K.d i' (e.f j) ≫ Hom.f (K.restrictionToTruncGE' e) j) 0

Tactic:
dsimp [restrictionToTruncGE']

Premises used: HomologicalComplex.restrictionToTruncGE'
-- 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'
j : ι
hj : e.BoundaryGE j
i' : ι'
h : c'.Rel i' (e.f j)
rw :
  Eq (α := K.X i' ⟶ (K.truncGE' e).X j)
    (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ K.pOpcycles (e.f j) ≫ Iso.inv (K.truncGE'XIsoOpcycles e ⋯ hj)) 0
⊢ Eq (α := K.X i' ⟶ (K.truncGE' e).X j) (K.d i' (e.f j) ≫ restrictionToTruncGE'.f K e j) 0

Tactic:
rw [restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv K e rfl hj]

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

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- 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
⊢ Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
    (Iso.hom (K.restrictionXIso e hi') ≫ K.pOpcycles i' ≫ Iso.inv (K.truncGE'XIsoOpcycles e hi' hi))

Tactic:
apply restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv

Premises used: HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv
-- 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
⊢ Eq (α := (K.restriction e).X i ⟶ (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
    (Iso.hom (K.restrictionXIso e hi') ≫ Iso.inv (K.truncGE'XIso e hi' hi))

Tactic:
apply restrictionToTruncGE'.f_eq_iso_hom_iso_inv

Premises used: HomologicalComplex.restrictionToTruncGE'.f_eq_iso_hom_iso_inv
-- 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
rw :
  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 : 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
⊢ 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 : 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'
h :
  ∀ (i : ι),
    Eq (α := (K.restriction e).X i ⟶ (L.truncGE' e).X i)
      (Hom.f (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e)) i)
      (Hom.f (restrictionMap φ e ≫ L.restrictionToTruncGE' e) i)
⊢ Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (restrictionMap φ e ≫ L.restrictionToTruncGE' 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 : 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 : ι
pos :
  ∀ (hi : e.BoundaryGE i),
    Eq (α := (K.restriction e).X i ⟶ (L.truncGE' e).X i)
      (Hom.f (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e)) i)
      (Hom.f (restrictionMap φ e ≫ L.restrictionToTruncGE' e) i)
neg :
  ∀ (hi : ¬e.BoundaryGE i),
    Eq (α := (K.restriction e).X i ⟶ (L.truncGE' e).X i)
      (Hom.f (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e)) i)
      (Hom.f (restrictionMap φ e ≫ L.restrictionToTruncGE' e) i)
⊢ Eq (α := (K.restriction e).X i ⟶ (L.truncGE' e).X i)
    (Hom.f (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e)) i)
    (Hom.f (restrictionMap φ e ≫ L.restrictionToTruncGE' 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 : 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.restriction e).X i ⟶ (L.truncGE' e).X i)
    (Hom.f (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e)) i)
    (Hom.f (restrictionMap φ e ≫ L.restrictionToTruncGE' e) i)

Tactic:
simp [restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv _ e rfl hi,
      truncGE'Map_f_eq_opcyclesMap φ e hi rfl, restrictionXIso]

Premises used: HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, HomologicalComplex.truncGE'Map_f_eq_opcyclesMap, HomologicalComplex.restrictionXIso, 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
⊢ Eq (α := (K.restriction e).X i ⟶ (L.truncGE' e).X i)
    (Hom.f (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e)) i)
    (Hom.f (restrictionMap φ e ≫ L.restrictionToTruncGE' e) i)

Tactic:
simp [restrictionToTruncGE'_f_eq_iso_hom_iso_inv _ e rfl hi,
      truncGE'Map_f_eq φ e hi rfl, restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso, HomologicalComplex.truncGE'Map_f_eq, 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'
i : ι
pos :
  ∀ (hi : e.BoundaryGE i),
    Epi (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
neg :
  ∀ (hi : ¬e.BoundaryGE i),
    Epi (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
⊢ Epi (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' 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
pos :
  Epi (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))
⊢ Epi (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_pOpcycles_iso_inv e rfl hi]

Premises used: HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_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'
i : ι
hi : e.BoundaryGE i
⊢ Epi (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'
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)

Tactic:
have := K.isIso_restrictionToTruncGE' e i 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
this : IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) 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 : K.IsStrictlySupported e
i : ι
pos :
  ∀ (hi : e.BoundaryGE i),
    IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
neg :
  ∀ (hi : ¬e.BoundaryGE i),
    IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
⊢ IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' 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'
inst_6 : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
pos :
  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))
⊢ 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_pOpcycles_iso_inv e rfl hi]

Premises used: HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, rfl