awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
i : ι
hi : e.f i = c'.prev j'
⊢ 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.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
hi : ¬∃ (i : ι), e.f i = c'.prev j'
⊢ ∀ (i : ι), e.f i ≠ c'.prev j'

Tactic:
simpa using hi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
hi : ¬∃ (i : ι), e.f i = c'.prev j'
⊢ Epi φ.τ₁

Tactic:
apply IsZero.epi (isZero_extend_X _ _ _ (by simpa using hi))

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.epi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
⊢ Epi φ.τ₁

Tactic:
have : Epi φ.τ₁ := by
      by_cases hi : ∃ i, e.f i = c'.prev j'
      · obtain ⟨i, hi⟩ := hi
        dsimp [φ, πTruncGE]
        rw [e.epi_liftExtend_f_iff _ _ hi]
        infer_instance
      · apply IsZero.epi (isZero_extend_X _ _ _ (by simpa using hi))
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this : Epi φ.τ₁
dsimp : IsIso (Y := (K.truncGE e).X j') (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) j')
⊢ IsIso φ.τ₂

Tactic:
dsimp [φ, πTruncGE]

Premises used: HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this : Epi φ.τ₁
rw : IsIso (X := (K.restriction e).X j) (Y := (K.truncGE' e).X j) (Hom.f (K.restrictionToTruncGE' e) j)
⊢ IsIso (Y := (K.truncGE e).X j') (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) j')

Tactic:
rw [e.isIso_liftExtend_f_iff _ _ hj']

Premises used: ComplexShape.Embedding.isIso_liftExtend_f_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this : Epi φ.τ₁
⊢ IsIso (X := (K.restriction e).X j) (Y := (K.truncGE' e).X j) (Hom.f (K.restrictionToTruncGE' e) j)

Tactic:
K.isIso_restrictionToTruncGE' e j hj

Premises used: HomologicalComplex.isIso_restrictionToTruncGE'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this : Epi φ.τ₁
⊢ IsIso (X := (K.restriction e).X j) (Y := (K.truncGE' e).X j) (Hom.f (K.restrictionToTruncGE' e) j)

Tactic:
exact K.isIso_restrictionToTruncGE' e j hj

Premises used: HomologicalComplex.isIso_restrictionToTruncGE'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this : Epi φ.τ₁
⊢ IsIso φ.τ₂

Tactic:
have : IsIso φ.τ₂ := by
      dsimp [φ, πTruncGE]
      rw [e.isIso_liftExtend_f_iff _ _ hj']
      exact K.isIso_restrictionToTruncGE' e j hj
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this : IsIso φ.τ₂
dsimp :
  IsIso (X := K.X (c'.next j')) (Y := (K.truncGE e).X (c'.next j'))
    (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) (c'.next j'))
⊢ IsIso φ.τ₃

Tactic:
dsimp [φ, πTruncGE]

Premises used: HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ c'.next j' = e.f (c.next j)

Tactic:
simpa only [← hj'] using e.next_f rfl

Premises used: ComplexShape.Embedding.next_f, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ c'.next j' = e.f (c.next j)

Tactic:
have : c'.next j' = e.f (c.next j) := by simpa only [← hj'] using e.next_f rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this_2 : IsIso φ.τ₂
this : c'.next j' = e.f (c.next j)
rw :
  IsIso (X := (K.restriction e).X (c.next j)) (Y := (K.truncGE' e).X (c.next j))
    (Hom.f (K.restrictionToTruncGE' e) (c.next j))
⊢ IsIso (X := K.X (c'.next j')) (Y := (K.truncGE e).X (c'.next j'))
    (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) (c'.next j'))

Tactic:
rw [e.isIso_liftExtend_f_iff _ _ this.symm]

Premises used: ComplexShape.Embedding.isIso_liftExtend_f_iff, Eq.symm
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this_2 : IsIso φ.τ₂
this : c'.next j' = e.f (c.next j)
⊢ IsIso (X := (K.restriction e).X (c.next j)) (Y := (K.truncGE' e).X (c.next j))
    (Hom.f (K.restrictionToTruncGE' e) (c.next j))

Tactic:
K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)

Premises used: ComplexShape.Embedding.not_boundaryGE_next', HomologicalComplex.isIso_restrictionToTruncGE', rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this_2 : IsIso φ.τ₂
this : c'.next j' = e.f (c.next j)
⊢ IsIso (X := (K.restriction e).X (c.next j)) (Y := (K.truncGE' e).X (c.next j))
    (Hom.f (K.restrictionToTruncGE' e) (c.next j))

Tactic:
exact K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)

Premises used: ComplexShape.Embedding.not_boundaryGE_next', HomologicalComplex.isIso_restrictionToTruncGE', rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ IsIso φ.τ₃

Tactic:
have : IsIso φ.τ₃ := by
      dsimp [φ, πTruncGE]
      have : c'.next j' = e.f (c.next j) := by simpa only [← hj'] using e.next_f rfl
      rw [e.isIso_liftExtend_f_iff _ _ this.symm]
      exact K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this_2 : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
    Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))

Tactic:
ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

Premises used: CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
this_1 : Epi φ.τ₁
this_2 : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
    Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))

Tactic:
exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

Premises used: CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
inst_5 : HasZeroObject.{v_1, u_3} C
i : ι
⊢ QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) (e.f i)

Tactic:
K.quasiIsoAt_πTruncGE e rfl

Premises used: HomologicalComplex.quasiIsoAt_πTruncGE, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
mp : QuasiIso (L := K.truncGE e) (K.πTruncGE e) → K.IsSupported e
mpr : K.IsSupported e → QuasiIso (L := K.truncGE e) (K.πTruncGE e)
⊢ QuasiIso (L := K.truncGE e) (K.πTruncGE e) ↔ K.IsSupported e

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : QuasiIso (L := K.truncGE e) (K.πTruncGE e)
⊢ K.IsSupported e

Tactic:
⟨fun i' hi' => ?_⟩

Premises used: HomologicalComplex.IsSupported.mk
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : QuasiIso (L := K.truncGE e) (K.πTruncGE e)
mp : ∀ (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i'), K.ExactAt i'
⊢ K.IsSupported e

Tactic:
refine ⟨fun i' hi' => ?_⟩
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : QuasiIso (L := K.truncGE e) (K.πTruncGE e)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
mp : (K.truncGE e).ExactAt i'
⊢ K.ExactAt i'

Tactic:
rw [exactAt_iff_of_quasiIsoAt (K.πTruncGE e) i']

Premises used: exactAt_iff_of_quasiIsoAt, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : QuasiIso (L := K.truncGE e) (K.πTruncGE e)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ (K.truncGE e).ExactAt i'

Tactic:
(K.truncGE e).exactAt_of_isSupported e i' hi'

Premises used: HomologicalComplex.truncGE, HomologicalComplex.exactAt_of_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : QuasiIso (L := K.truncGE e) (K.πTruncGE e)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ (K.truncGE e).ExactAt i'

Tactic:
exact (K.truncGE e).exactAt_of_isSupported e i' hi'

Premises used: HomologicalComplex.truncGE, HomologicalComplex.exactAt_of_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : K.IsSupported e
mpr : ∀ (i : ι'), QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) i
⊢ QuasiIso (L := K.truncGE e) (K.πTruncGE e)

Tactic:
rw [quasiIso_iff]

Premises used: quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : K.IsSupported e
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) i'
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) i'
⊢ QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : K.IsSupported e
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι), QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) (e.f i)
⊢ QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : K.IsSupported e
i : ι
⊢ QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) (e.f i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : K.IsSupported e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
neg : (K.truncGE e).ExactAt i'
neg₁ : K.ExactAt i'
⊢ QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) i'

Tactic:
rw [quasiIsoAt_iff_exactAt (K.πTruncGE e) i']

Premises used: quasiIsoAt_iff_exactAt, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : K.IsSupported e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
h : K.IsSupported e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ (K.truncGE e).ExactAt i'

Tactic:
exact exactAt_of_isSupported _ e i' (by simpa using hi')

Premises used: HomologicalComplex.exactAt_of_isSupported