-- Mathlib/Condensed/AB.lean
lemma hasExactColimitsOfShape [HasColimitsOfShape J A] [HasExactColimitsOfShape J A]
    [HasFiniteLimits A] : HasExactColimitsOfShape J (Condensed.{u} A)

Proof state:
A : Type u_1
J : Type u_2
inst✝⁸ : Category.{u_4, u_1} A
inst✝⁷ : Category.{u_3, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
⊢ HasExactColimitsOfShape J (Condensed A)

Tactic:
have : HasColimitsOfShape J (Sheaf (extensiveTopology Stonean.{u}) A) :=
  hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape e.inverse

Result:
A : Type u_1
J : Type u_2
inst✝⁸ : Category.{u_4, u_1} A
inst✝⁷ : Category.{u_3, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
this : HasColimitsOfShape J (Sheaf (extensiveTopology Stonean) A)
⊢ HasExactColimitsOfShape J (Condensed A)

Proof state:
A : Type u_1
J : Type u_2
inst✝⁸ : Category.{u_4, u_1} A
inst✝⁷ : Category.{u_3, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
this : HasColimitsOfShape J (Sheaf (extensiveTopology Stonean) A)
⊢ HasExactColimitsOfShape J (Condensed A)

Tactic:
exact HasExactColimitsOfShape.domain_of_functor _ e.functor

Result:
no goals

Proof state:
A : Type u_1
J : Type u_2
inst✝⁸ : Category.{u_4, u_1} A
inst✝⁷ : Category.{u_3, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
⊢ HasExactColimitsOfShape J (Condensed A)

Tactic:
let e : Condensed.{u} A ≌ Sheaf (extensiveTopology Stonean.{u}) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence

Result:
A : Type u_1
J : Type u_2
inst✝⁸ : Category.{u_4, u_1} A
inst✝⁷ : Category.{u_3, u_2} J
inst✝⁶ : Preadditive A
inst✝⁵ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝⁴ : HasWeakSheafify (coherentTopology CompHaus) A
inst✝³ : HasWeakSheafify (extensiveTopology Stonean) A
inst✝² : HasColimitsOfShape J A
inst✝¹ : HasExactColimitsOfShape J A
inst✝ : HasFiniteLimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
⊢ HasExactColimitsOfShape J (Condensed A)