-- Mathlib/Condensed/AB.lean
lemma hasExactLimitsOfShape [HasLimitsOfShape J A] [HasExactLimitsOfShape J A]
    [HasFiniteColimits A] : HasExactLimitsOfShape 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✝² : HasLimitsOfShape J A
inst✝¹ : HasExactLimitsOfShape J A
inst✝ : HasFiniteColimits A
⊢ HasExactLimitsOfShape 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✝² : HasLimitsOfShape J A
inst✝¹ : HasExactLimitsOfShape J A
inst✝ : HasFiniteColimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
⊢ HasExactLimitsOfShape 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✝² : HasLimitsOfShape J A
inst✝¹ : HasExactLimitsOfShape J A
inst✝ : HasFiniteColimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
⊢ HasExactLimitsOfShape J (Condensed A)

Tactic:
have : HasLimitsOfShape J (Sheaf (extensiveTopology Stonean.{u}) A) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape 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✝² : HasLimitsOfShape J A
inst✝¹ : HasExactLimitsOfShape J A
inst✝ : HasFiniteColimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
this : HasLimitsOfShape J (Sheaf (extensiveTopology Stonean) A)
⊢ HasExactLimitsOfShape 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✝² : HasLimitsOfShape J A
inst✝¹ : HasExactLimitsOfShape J A
inst✝ : HasFiniteColimits A
e : Condensed A ≌ Sheaf (extensiveTopology Stonean) A :=
  (StoneanCompHaus.equivalence A).symm.trans Presheaf.coherentExtensiveEquivalence
this : HasLimitsOfShape J (Sheaf (extensiveTopology Stonean) A)
⊢ HasExactLimitsOfShape J (Condensed A)

Tactic:
exact HasExactLimitsOfShape.domain_of_functor _ e.functor

Result:
no goals