-- Mathlib/CategoryTheory/Limits/Final.lean
/-- The functor `Grothendieck.map α` for a natural transformation `α : F ⟶ G`, with
`F G : C ⥤ Cat`, is final if for each `X : C`, the functor `α.app X` is final. -/
lemma Grothendieck.final_map {F G : C ⥤ Cat.{v₂, u₂}} (α : F ⟶ G) [hα : ∀ X, Final (α.app X)] :
    Final (map α)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
⊢ (map α).Final

Tactic:
let G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
⊢ (map α).Final

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor))).Final
⊢ (map α).Final

Tactic:
have i := mapWhiskerLeftIsoConjPreMap sC.symm (whiskerRight α Cat.asSmallFunctor)
  ≪≫ isoWhiskerLeft _ (isoWhiskerRight (mapWhiskerRightAsSmallFunctor α) _)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
⊢ (map α).Final

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
⊢ (map α).Final

Tactic:
have := final_of_natIso i

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this✝ : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
this :
  ((preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse).Final
⊢ (map α).Final

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this✝ : ∀ (X : AsSmall C), Final (α'.app X)
hα' : (map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (whiskerLeft sC.symm.functor (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
this :
  ((preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse).Final
⊢ (map α).Final

Tactic:
rwa [← final_iff_equivalence_comp, ← final_iff_comp_equivalence,
  ← final_iff_equivalence_comp, ← final_iff_comp_equivalence] at this

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
⊢ (map α).Final

Tactic:
have : ∀ X, Final (α'.app X) := fun X =>
  inferInstanceAs (AsSmall.equiv.inverse ⋙ _ ⋙ AsSmall.equiv.functor).Final

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := whiskerLeft sC.inverse (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), Final (α'.app X)
⊢ (map α).Final

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
⊢ (map α).Final

Tactic:
let sC : C ≌ AsSmall.{max u₁ u₂ v₁ v₂} C := AsSmall.equiv

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
⊢ (map α).Final

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
⊢ (map α).Final

Tactic:
let F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
⊢ (map α).Final