-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
Checking exactness of limits of shape `Discrete ℕ` and `Discrete J` for finite `J` is enough for
countable AB4*.
-/
lemma CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite [HasCountableProducts C]
    [HasFiniteColimits C] [∀ (J : Type) [Finite J], HasExactLimitsOfShape (Discrete J) C]
    [HasExactLimitsOfShape (Discrete ℕ) C] :
    CountableAB4Star C where
  ofShape J

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

Tactic:
have : Infinite J := ⟨h⟩

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

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

Tactic:
by_cases h : Finite J

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

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

Proof state:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (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
⊢ HasExactLimitsOfShape (Discrete J) C

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

Result:
no goals

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

Tactic:
let _ := Encodable.ofCountable J

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

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

Tactic:
let _ := Denumerable.ofEncodableOfInfinite J

Result:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (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
⊢ HasExactLimitsOfShape (Discrete J) C

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

Tactic:
infer_instance

Result:
no goals