Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
              ((CochainComplex.single₀ C).obj Z)).X₂,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
        X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
        f :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
              (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
        g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
        zero := ⋯ }.Exact ∧
    Mono
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
          (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂

pp: case zero.hf₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).f = 0

pp: case zero.hg₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).g = 0

pp: case zero.hf₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).f = 0

Tactic:
]

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
              ((CochainComplex.single₀ C).obj Z)).X₂,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
        X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
        f :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
              (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
        g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
        zero := ⋯ }.Exact ∧
    Mono
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
          (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂

case zero.hf₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).f = 0

case zero.hg₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj ((CochainComplex.single₀ C).obj Z)).g = 0

case zero.hf₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).f = 0