-- Mathlib/CategoryTheory/Limits/Final.lean
theorem final_of_final_comp [hF : Final F] [hFG : Final (F ⋙ G)] : Final G

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
rw [final_iff_comp_equivalence (F ⋙ G) s₃.functor, final_iff_equivalence_comp s₁.inverse,
  final_natIso_iff _i, final_iff_isIso_colimit_pre] at hFG

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
hFG :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
⊢ G.Final

Tactic:
let s₃ : E ≌ AsSmall.{max u₁ v₁ u₂ v₂ u₃ v₃} E := AsSmall.equiv

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
⊢ G.Final

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
rw [final_iff_comp_equivalence F s₂.functor, final_iff_equivalence_comp s₁.inverse,
  final_iff_isIso_colimit_pre] at hF

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ G.Final

Tactic:
rw [final_iff_comp_equivalence G s₃.functor, final_iff_equivalence_comp s₂.inverse,
  final_iff_isIso_colimit_pre]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
⊢ G.Final

Tactic:
let _i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅
    (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ (s₂.inverse ⋙ G ⋙ s₃.functor) :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ G.Final

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
⊢ G.Final

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

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
⊢ G.Final

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
hFG :
  IsIso
    (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor) ≫
      colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ IsIso (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
exact IsIso.of_isIso_comp_left (colimit.pre _ (s₁.inverse ⋙ F ⋙ s₂.functor)) _

Result:
no goals