-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem succ_exact :
    (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho))
    (by ext : 2; apply CC_comp_zero)).Exact

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho) = 0

Tactic:
ext : 2

Result:
case hf.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝ : ↑(ModuleCat.of ℤ (LocallyConstant ↑(π C fun x => ord I x < o) ℤ))
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho))) x✝ = (ModuleCat.Hom.hom 0) x✝

Proof state:
case hf.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝ : ↑(ModuleCat.of ℤ (LocallyConstant ↑(π C fun x => ord I x < o) ℤ))
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho))) x✝ = (ModuleCat.Hom.hom 0) x✝

Tactic:
apply CC_comp_zero

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
f : ↑(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).X₂
⊢ (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g) f =
      0 →
    ∃ x₁,
      (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f)
          x₁ =
        f

Tactic:
exact CC_exact C hC hsC ho

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ ∀ (x₂ : ↑(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).X₂),
    (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g) x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f)
            x₁ =
          x₂

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ ∀ (x₂ : ↑(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).X₂),
    (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g) x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f)
            x₁ =
          x₂

Tactic:
intro f

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
f : ↑(ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).X₂
⊢ (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g) f =
      0 →
    ∃ x₁,
      (ConcreteCategory.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f)
          x₁ =
        f