awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
dsimp :
  Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        (𝟙 (K.X j') ≫
            CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
              (𝟙 (K.X (e.f j)) : K.X (e.f j) ⟶ K.X (e.f j))) ≫
          ((K.restriction e).sc j).pOpcycles :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
⊢ Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        (NatTrans.app (Iso.hom (natIsoSc' C c' i' j' k' hi'' hk'')) K ≫
              Iso.inv (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) (K.restriction e)).τ₂ ≫
          ((K.restriction e).sc j).pOpcycles :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
rw :
  Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
          (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
⊢ Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        (𝟙 (K.X j') ≫
            CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
              (𝟙 (K.X (e.f j)) : K.X (e.f j) ⟶ K.X (e.f j))) ≫
          ((K.restriction e).sc j).pOpcycles :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)

Tactic:
rw [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
          (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)

Tactic:
((ShortComplex.homology_π_ι_assoc _ _).trans ?_).symm

Premises used: CategoryTheory.ShortComplex.homology_π_ι_assoc, HomologicalComplex.opcycles, HomologicalComplex.homologyι, Eq.symm, HomologicalComplex.homology, Eq.trans
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
refine :
  Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        CategoryStruct.comp (Y := (K.sc j').opcycles) ((K.sc j').pOpcycles : (K.sc j').X₂ ⟶ (K.sc j').opcycles)
          (Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'') : K.opcycles j' ⟶ (K.restriction e).opcycles j) :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
          (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
⊢ Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
          (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)

Tactic:
refine ((ShortComplex.homology_π_ι_assoc _ _).trans ?_).symm

Premises used: CategoryTheory.ShortComplex.homology_π_ι_assoc, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
e_a :
  Eq (α := (K.sc j').X₂ ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').opcycles) ((K.sc j').pOpcycles : (K.sc j').X₂ ⟶ (K.sc j').opcycles)
        (Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'') : K.opcycles j' ⟶ (K.restriction e).opcycles j) :
      (K.sc j').X₂ ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
        (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
      K.X j' ⟶ ((K.restriction e).sc j).opcycles)
⊢ Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        CategoryStruct.comp (Y := (K.sc j').opcycles) ((K.sc j').pOpcycles : (K.sc j').X₂ ⟶ (K.sc j').opcycles)
          (Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'') : K.opcycles j' ⟶ (K.restriction e).opcycles j) :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
          (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ Eq (α := (K.sc j').X₂ ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').opcycles) ((K.sc j').pOpcycles : (K.sc j').X₂ ⟶ (K.sc j').opcycles)
        (Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'') : K.opcycles j' ⟶ (K.restriction e).opcycles j) :
      (K.sc j').X₂ ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
        (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
      K.X j' ⟶ ((K.restriction e).sc j).opcycles)

Tactic:
apply pOpcycles_restrictionOpcyclesIso_inv

Premises used: HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
rw :
  Eq (α := K.homology j' ⟶ K.opcycles j')
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'') ≫ K.homologyι j'))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      ((K.restriction e).homologyι j ≫ Iso.hom (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')))
rw₁ :
  Eq (α := K.homology j' ⟶ K.opcycles j') (K.homologyι j')
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      ((K.restriction e).homologyι j ≫ Iso.hom (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')))
rw₂ :
  Eq (α := K.homology j' ⟶ K.opcycles j') (K.homologyι j')
    (K.homologyι j' ≫
      CategoryStruct.comp (Y := (K.restriction e).opcycles j) (Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi''))
        (Iso.hom (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')))
rw₃ : K.homologyι j' = K.homologyι j' ≫ 𝟙 (K.opcycles j')
rw₄ rw₅ : Eq (α := K.homology j' ⟶ K.opcycles j') (K.homologyι j') (K.homologyι j')
⊢ Eq (α := (K.restriction e).homology j ⟶ K.opcycles j')
    (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'') ≫ K.homologyι j')
    ((K.restriction e).homologyι j ≫ Iso.hom (K.restrictionOpcyclesIso e i j hi hi' hj' hi''))

Tactic:
rw [← cancel_epi (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv,
    Iso.inv_hom_id_assoc, restrictionHomologyIso_inv_homologyι_assoc,
      Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Iso.inv_hom_id, HomologicalComplex.restrictionHomologyIso_inv_homologyι_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.restrictionHomologyIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
⊢ ((K.restriction e).extend e).IsStrictlySupported e

Tactic:
infer_instance
-- 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
i : ι
i' : ι'
hi' : e.f i = i'
subst : (K.restriction e).X i = K.X (e.f i)
⊢ (K.restriction e).X i = K.X 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 M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
⊢ (K.restriction e).X i = K.X (e.f i)

Tactic:
rfl
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')

Tactic:
isZero_extend_X _ _ _ hi'

Premises used: HomologicalComplex.isZero_extend_X
-- 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
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_4 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
pos : ∀ (hi'' : ∃ (i : ι), e.f i = i'), IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')
neg : ∀ (hi'' : ¬∃ (i : ι), e.f i = i'), IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')
⊢ IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')

Tactic:
by_cases hi'' : ∃ i, e.f i = i'
-- 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
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_4 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι) (hi : e.f i = i'), IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')
⊢ IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')

Tactic:
obtain ⟨i, hi⟩ := 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 M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_4 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
⊢ IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')

Tactic:
(K.isZero_X_of_isStrictlySupported e' i' hi').of_iso (K.stupidTruncXIso e hi)

Premises used: CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.stupidTruncXIso, HomologicalComplex.isZero_X_of_isStrictlySupported
-- 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
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_4 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
⊢ IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')

Tactic:
exact (K.isZero_X_of_isStrictlySupported e' i' hi').of_iso (K.stupidTruncXIso e hi)

Premises used: CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.stupidTruncXIso, HomologicalComplex.isZero_X_of_isStrictlySupported
-- 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
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_4 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ (i : ι), e.f i = i'
neg : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero.{v_1, u_3} ((K.stupidTrunc e).X i')

Tactic:
apply isZero_stupidTrunc_X

Premises used: HomologicalComplex.isZero_stupidTrunc_X
-- 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
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_4 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ (i : ι), e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi''
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
mp : IsZero (K.stupidTrunc e) → K.IsStrictlySupportedOutside e
mpr : K.IsStrictlySupportedOutside e → IsZero (K.stupidTrunc e)
⊢ IsZero (K.stupidTrunc e) ↔ K.IsStrictlySupportedOutside e

Tactic:
constructor
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
⊢ IsZero (K.stupidTrunc e) → K.IsStrictlySupportedOutside e

Tactic:
fun h ↦ ⟨fun i ↦
      ((eval _ _ (e.f i)).map_isZero h).of_iso (K.stupidTruncXIso e rfl).symm⟩

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero, CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.stupidTruncXIso, HomologicalComplex.IsStrictlySupportedOutside.mk, CategoryTheory.Iso.symm, ComplexShape.Embedding.f, rfl
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
⊢ IsZero (K.stupidTrunc e) → K.IsStrictlySupportedOutside e

Tactic:
exact fun h ↦ ⟨fun i ↦
      ((eval _ _ (e.f i)).map_isZero h).of_iso (K.stupidTruncXIso e rfl).symm⟩
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
h : K.IsStrictlySupportedOutside e
mpr : (K.stupidTrunc e).IsStrictlySupported e ∧ (K.stupidTrunc e).IsStrictlySupportedOutside e
⊢ IsZero (K.stupidTrunc e)

Tactic:
rw [isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside _ e]

Premises used: HomologicalComplex.isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
h : K.IsStrictlySupportedOutside e
mpr : (K.stupidTrunc e).IsStrictlySupported e
mpr₁ : (K.stupidTrunc e).IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupported e ∧ (K.stupidTrunc e).IsStrictlySupportedOutside e

Tactic:
constructor
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupported e

Tactic:
infer_instance
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupportedOutside e

Tactic:
⟨fun i ↦ (h.isZero i).of_iso (K.stupidTruncXIso e rfl)⟩

Premises used: HomologicalComplex.IsStrictlySupportedOutside.isZero, CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.stupidTruncXIso, HomologicalComplex.IsStrictlySupportedOutside.mk, rfl
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupportedOutside e

Tactic:
exact ⟨fun i ↦ (h.isZero i).of_iso (K.stupidTruncXIso e rfl)⟩
-- 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 : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_3 : e.IsRelIff
⊢ stupidTruncMap (𝟙 K) e = 𝟙 (K.stupidTrunc e)

Tactic:
simp [stupidTruncMap, stupidTrunc]

Premises used: HomologicalComplex.stupidTrunc, HomologicalComplex.stupidTruncMap