-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
lemma AB5OfSize_of_univLE [HasFilteredColimitsOfSize.{w₂, w₂'} C] [UnivLE.{w, w₂}]
    [UnivLE.{w', w₂'}] [AB5OfSize.{w₂, w₂'} C] :
    haveI : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_of_univLE.{w}
    AB5OfSize.{w, w'} C

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

Tactic:
intro J _ _

Result:
case ofShape
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsFiltered J
⊢ HasExactColimitsOfShape J C

Proof state:
case ofShape
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5OfSize.{w₂, w₂', v, u} C
this : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsFiltered J
⊢ HasExactColimitsOfShape J C

Tactic:
haveI := IsFiltered.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✝⁵ : HasFilteredColimitsOfSize.{w₂, w₂', v, u} C
inst✝⁴ : UnivLE.{w, w₂}
inst✝³ : UnivLE.{w', w₂'}
inst✝² : AB5OfSize.{w₂, w₂', v, u} C
this✝ : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
inst✝¹ : Category.{w, w'} J
inst✝ : IsFiltered J
this : IsFiltered (Shrink.{w₂', w'} (ShrinkHoms.{w'} J))
⊢ HasExactColimitsOfShape J C

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

Tactic:
haveI : HasFilteredColimitsOfSize.{w, w'} C := hasFilteredColimitsOfSize_of_univLE.{w}

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

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

Tactic:
constructor

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

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

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

Result:
no goals