-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
Checking exactness of colimits of shape `Discrete ℕ` and `Discrete J` for finite `J` is enough for
countable AB4.
-/
lemma CountableAB4.of_hasExactColimitsOfShape_nat_and_finite [HasCountableCoproducts C]
    [HasFiniteLimits C] [∀ (J : Type) [Finite J], HasExactColimitsOfShape (Discrete J) C]
    [HasExactColimitsOfShape (Discrete ℕ) C] :
    CountableAB4 C where
  ofShape J

Proof state:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
have : Infinite J := ⟨h⟩

Result:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
⊢ HasExactColimitsOfShape (Discrete J) C

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCountableCoproducts C
inst✝² : HasFiniteLimits C
inst✝¹ : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
⊢ ∀ [inst : Countable J], HasExactColimitsOfShape (Discrete J) C

Tactic:
by_cases h : Finite J

Result:
case pos
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

Proof state:
case pos
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
infer_instance

Result:
no goals

Proof state:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
x✝ : Encodable J := Encodable.ofCountable J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
let _ := Denumerable.ofEncodableOfInfinite J

Result:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
x✝¹ : Encodable J := Encodable.ofCountable J
x✝ : Denumerable J := Denumerable.ofEncodableOfInfinite J
⊢ HasExactColimitsOfShape (Discrete J) C

Proof state:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
let _ := Encodable.ofCountable J

Result:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
x✝ : Encodable J := Encodable.ofCountable J
⊢ HasExactColimitsOfShape (Discrete J) C

Proof state:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
this : Infinite J
x✝¹ : Encodable J := Encodable.ofCountable J
x✝ : Denumerable J := Denumerable.ofEncodableOfInfinite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
exact hasExactColimitsOfShape_of_final C (Discrete.equivalence (Denumerable.eqv J)).inverse

Result:
no goals