-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
lemma AB5StarOfSize_of_univLE [HasCofilteredLimitsOfSize.{w₂, w₂'} C] [UnivLE.{w, w₂}]
    [UnivLE.{w', w₂'}] [AB5StarOfSize.{w₂, w₂'} C] :
    haveI : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}
    AB5StarOfSize.{w, w'} C

Proof state:
case ofShape
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5StarOfSize.{w₂, w₂', v, u} C
this✝ : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsCofiltered J
this : IsCofiltered (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactLimitsOfShape J C

Tactic:
exact HasExactLimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
  Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J)).symm

Result:
no goals

Proof state:
case ofShape
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
⊢ ∀ (J : Type w') [inst : Category.{w, w'} J] [inst_1 : IsCofiltered J], HasExactLimitsOfShape J C

Tactic:
intro J _ _

Result:
case ofShape
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsCofiltered J
⊢ HasExactLimitsOfShape J C

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
⊢ AB5StarOfSize.{w, w', v, u} C

Tactic:
haveI : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
⊢ AB5StarOfSize.{w, w', v, u} C

Proof state:
case ofShape
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsCofiltered J
⊢ HasExactLimitsOfShape J C

Tactic:
haveI := IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
  Shrink.equivalence.{w₂'} (ShrinkHoms.{w'} J))

Result:
case ofShape
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5StarOfSize.{w₂, w₂', v, u} C
this✝ : HasCofilteredLimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsCofiltered J
this : IsCofiltered (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactLimitsOfShape J C

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
⊢ AB5StarOfSize.{w, w', v, u} C

Tactic:
constructor

Result:
case ofShape
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
this : HasCofilteredLimitsOfSize.{w, w', v, u} C
⊢ ∀ (J : Type w') [inst : Category.{w, w'} J] [inst_1 : IsCofiltered J], HasExactLimitsOfShape J C