awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op K)) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (K.ιTruncLE e))) ↔
    K.op.IsSupported e.op

Tactic:
K.op.quasiIso_πTruncGE_iff_isSupported e.op

Premises used: HomologicalComplex.extend.d, HomologicalComplex.op, Quiver.Hom.op, HomologicalComplex.quasiIso_πTruncGE_iff_isSupported, Quiver.Hom.unop, HomologicalComplex.truncGE, ComplexShape.Embedding.liftExtend, HomologicalComplex.extend, dite, ComplexShape.Embedding.op, ComplexShape.Embedding.liftExtend.f, HomologicalComplex.extend.X, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op K)) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (K.ιTruncLE e))) ↔
    K.op.IsSupported e.op

Tactic:
exact K.op.quasiIso_πTruncGE_iff_isSupported e.op

Premises used: HomologicalComplex.op, HomologicalComplex.quasiIso_πTruncGE_iff_isSupported, ComplexShape.Embedding.op
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
rw : (K.truncLE e).op.Acyclic ↔ K.op.IsSupportedOutside e.op
⊢ (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e

Tactic:
rw [← acyclic_op_iff, ← isSupportedOutside_op_iff]

Premises used: HomologicalComplex.isSupportedOutside_op_iff, HomologicalComplex.acyclic_op_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ (K.truncLE e).op.Acyclic ↔ K.op.IsSupportedOutside e.op

Tactic:
K.op.acyclic_truncGE_iff_isSupportedOutside e.op

Premises used: HomologicalComplex.extend.d, HomologicalComplex.op, Quiver.Hom.op, Quiver.Hom.unop, HomologicalComplex.truncGE, HomologicalComplex.extend, ComplexShape.Embedding.op, HomologicalComplex.acyclic_truncGE_iff_isSupportedOutside, HomologicalComplex.extend.X
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ (K.truncLE e).op.Acyclic ↔ K.op.IsSupportedOutside e.op

Tactic:
exact K.op.acyclic_truncGE_iff_isSupportedOutside e.op

Premises used: HomologicalComplex.op, ComplexShape.Embedding.op, HomologicalComplex.acyclic_truncGE_iff_isSupportedOutside
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
rw :
  QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op (L.truncLE e))) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (truncLEMap φ e))) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
⊢ QuasiIso (K := K.truncLE e) (L := L.truncLE e) (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
rw [← quasiIso_opFunctor_map_iff]

Premises used: HomologicalComplex.quasiIso_opFunctor_map_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
simp :
  QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op (L.truncLE e))) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (truncLEMap φ e))) ↔
    ∀ (i : ι) (i' : ι'),
      e.f i = i' →
        QuasiIsoAt (K := Functor.obj (opFunctor C c') (Opposite.op L))
          (CategoryTheory.Functor.map (opFunctor C c') φ.op) i'
⊢ QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op (L.truncLE e))) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (truncLEMap φ e))) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
simp only [← quasiIsoAt_opFunctor_map_iff φ]

Premises used: HomologicalComplex.quasiIsoAt_opFunctor_map_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
⊢ QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op (L.truncLE e))) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (truncLEMap φ e))) ↔
    ∀ (i : ι) (i' : ι'),
      e.f i = i' →
        QuasiIsoAt (K := Functor.obj (opFunctor C c') (Opposite.op L))
          (CategoryTheory.Functor.map (opFunctor C c') φ.op) i'

Tactic:
apply quasiIso_truncGEMap_iff

Premises used: HomologicalComplex.quasiIso_truncGEMap_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
dsimp : Mono (X := K.truncLE e) (K.ιTruncLE e)
⊢ Mono (K.shortComplexTruncLE e).f

Tactic:
dsimp [shortComplexTruncLE]

Premises used: HomologicalComplex.shortComplexTruncLE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
⊢ Mono (X := K.truncLE e) (K.ιTruncLE e)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
dsimp : Epi (Y := cokernel (X := K.truncLE e) (K.ιTruncLE e)) (cokernel.π (K.ιTruncLE e))
⊢ Epi (K.shortComplexTruncLE e).g

Tactic:
dsimp [shortComplexTruncLE]

Premises used: HomologicalComplex.shortComplexTruncLE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
⊢ Epi (Y := cokernel (X := K.truncLE e) (K.ιTruncLE e)) (cokernel.π (K.ιTruncLE e))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ { X₁ := (K.shortComplexTruncLE e).X₁.homology i', X₂ := (K.shortComplexTruncLE e).X₂.homology i',
        X₃ := (K.shortComplexTruncLE e).X₃.homology i', f := homologyMap (K.shortComplexTruncLE e).f i',
        g := homologyMap (K.shortComplexTruncLE e).g i', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f =
    0

Tactic:
apply ((K.truncLE e).exactAt_of_isSupported e i' hi').isZero_homology.eq_of_src

Premises used: HomologicalComplex.exactAt_of_isSupported, HomologicalComplex.truncLE, CategoryTheory.Limits.IsZero.eq_of_src, HomologicalComplex.ExactAt.isZero_homology
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
pos :
  ∀ (hj : ∃ (j : ι), e.f j = j'),
    Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
      (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0
neg :
  ∀ (hj : ¬∃ (j : ι), e.f j = j'),
    Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
      (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0

Tactic:
by_cases hj : ∃ j, e.f j = j'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
hj : ∃ (j : ι), e.f j = j'
pos :
  ∀ (j : ι) (hij' : c'.Rel i' (e.f j)),
    Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology (e.f j))
      (ShortComplex.ShortExact.δ ⋯ i' (e.f j) hij') 0
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0

Tactic:
obtain ⟨j, rfl⟩ := hj

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
j : ι
hij' : c'.Rel i' (e.f j)
pos :
  Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ K.homology (e.f j))
    (ShortComplex.ShortExact.δ ⋯ i' (e.f j) hij' ≫ homologyMap (K.ιTruncLE e) (e.f j)) 0
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology (e.f j))
    (ShortComplex.ShortExact.δ ⋯ i' (e.f j) hij') 0

Tactic:
rw [← cancel_mono (homologyMap (K.ιTruncLE e) (e.f j)), zero_comp]

Premises used: HomologicalComplex.ιTruncLE, CategoryTheory.cancel_mono, ComplexShape.Embedding.f, HomologicalComplex.homologyMap, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
j : ι
hij' : c'.Rel i' (e.f j)
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ K.homology (e.f j))
    (ShortComplex.ShortExact.δ ⋯ i' (e.f j) hij' ≫ homologyMap (K.ιTruncLE e) (e.f j)) 0

Tactic:
(K.shortComplexTruncLE_shortExact e).δ_comp i' _ hij'

Premises used: HomologicalComplex.unop, HomologicalComplex.ιTruncLE, HomologicalComplex.truncLE, HomologicalComplex.shortComplexTruncLE_shortExact, CategoryTheory.ShortComplex.ShortExact.δ_comp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
j : ι
hij' : c'.Rel i' (e.f j)
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ K.homology (e.f j))
    (ShortComplex.ShortExact.δ ⋯ i' (e.f j) hij' ≫ homologyMap (K.ιTruncLE e) (e.f j)) 0

Tactic:
exact (K.shortComplexTruncLE_shortExact e).δ_comp i' _ hij'

Premises used: HomologicalComplex.shortComplexTruncLE_shortExact, CategoryTheory.ShortComplex.ShortExact.δ_comp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
hj : ¬∃ (j : ι), e.f j = j'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
simpa using hj
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
hj : ¬∃ (j : ι), e.f j = j'
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0

Tactic:
apply ((K.truncLE e).exactAt_of_isSupported e j'
      (by simpa using hj)).isZero_homology.eq_of_tgt

Premises used: HomologicalComplex.exactAt_of_isSupported, HomologicalComplex.truncLE, CategoryTheory.Limits.IsZero.eq_of_tgt, HomologicalComplex.ExactAt.isZero_homology
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
pos :
  ∀ (hi' : ∃ (j' : ι'), c'.Rel i' j'),
    Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
      (homologyMap (K.shortComplexTruncLE e).g i')
neg :
  ∀ (hi' : ¬∃ (j' : ι'), c'.Rel i' j'),
    Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
      (homologyMap (K.shortComplexTruncLE e).g i')
⊢ Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
by_cases hi' : ∃ j', c'.Rel i' j'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∃ (j' : ι'), c'.Rel i' j'
pos :
  ∀ (j' : ι') (hj' : c'.Rel i' j'),
    Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
      (homologyMap (K.shortComplexTruncLE e).g i')
⊢ Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
obtain ⟨j', hj'⟩ := hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' j' : ι'
hj' : c'.Rel i' j'
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology i', X₂ := (K.shortComplexTruncLE e).X₃.homology i',
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g i',
        g := ShortComplex.ShortExact.δ ⋯ i' j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.g =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' j' : ι'
hj' : c'.Rel i' j'
⊢ Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
exact ((K.shortComplexTruncLE_shortExact e).homology_exact₃ i' j' hj').epi_f (by simp)

Premises used: CategoryTheory.ShortComplex.Exact.epi_f, CategoryTheory.ShortComplex.ShortExact.homology_exact₃, HomologicalComplex.shortComplexTruncLE_shortExact
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ¬∃ (j' : ι'), c'.Rel i' j'
⊢ ∀ (j : ι'), ¬c'.Rel i' j

Tactic:
simpa using hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ¬∃ (j' : ι'), c'.Rel i' j'
⊢ Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
exact epi_homologyMap_of_epi_of_not_rel _ _ (by simpa using hi')

Premises used: HomologicalComplex.epi_homologyMap_of_epi_of_not_rel
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Mono (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
have := K.mono_homologyMap_shortComplexTruncLE_g e i' hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
this :
  Mono (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
⊢ IsIso (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
rw :
  IsIso (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
⊢ QuasiIsoAt (K.shortComplexTruncLE e).g i'

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]

Premises used: quasiIsoAt_iff_isIso_homologyMap
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsIso (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
K.isIso_homologyMap_shortComplexTruncLE_g e i' hi'

Premises used: HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsIso (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
exact K.isIso_homologyMap_shortComplexTruncLE_g e i' hi'

Premises used: HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
rw : IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
⊢ (K.shortComplexTruncLE e).X₃.ExactAt (e.f i)

Tactic:
rw [exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
pos : ∀ (hi : ∃ (j' : ι'), c'.Rel (e.f i) j'), IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
neg : ∀ (hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'), IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
by_cases hi : ∃ j', c'.Rel (e.f i) j'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ∃ (j' : ι'), c'.Rel (e.f i) j'
pos : ∀ (j' : ι') (hj' : c'.Rel (e.f i) j'), IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))

Tactic:
obtain ⟨j', hj'⟩ := hi