awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesLeftKanExtension F L
inst_5 : L.HasLeftKanExtension F
a : A
⊢ Eq (α := (F ⋙ G).obj a ⟶ (L.leftKanExtension F ⋙ G).obj (L.obj a))
    (CategoryStruct.comp (Y := (L ⋙ L.leftKanExtension (F ⋙ G)).obj a)
      (NatTrans.app (L.leftKanExtensionUnit (F ⋙ G)) a : (F ⋙ G).obj a ⟶ (L ⋙ L.leftKanExtension (F ⋙ G)).obj a)
      (NatTrans.app (Iso.inv (G.leftKanExtensionCompIsoOfPreserves F L)) (L.obj a) :
        (L.leftKanExtension (F ⋙ G)).obj (L.obj a) ⟶ (L.leftKanExtension F ⋙ G).obj (L.obj a)))
    (G.map (NatTrans.app (L.leftKanExtensionUnit F) a))

Tactic:
simpa [-leftKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (leftKanExtensionCompIsoOfPreserves_inv_fac G F L) a

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_inv_fac
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesPointwiseLeftKanExtension F L
inst_5 : L.HasPointwiseLeftKanExtension F
⊢ Eq (α := F ⋙ G ⟶ L ⋙ L.pointwiseLeftKanExtension (F ⋙ G))
    (whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫
        (L.associator (L.pointwiseLeftKanExtension F) G).hom ≫
          L.whiskerLeft (Iso.hom (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L)) :
      F ⋙ G ⟶ L ⋙ L.pointwiseLeftKanExtension (F ⋙ G))
    (L.pointwiseLeftKanExtensionUnit (F ⋙ G) : F ⋙ G ⟶ L ⋙ L.pointwiseLeftKanExtension (F ⋙ G))

Tactic:
simpa [pointwiseLeftKanExtensionCompIsoOfPreserves] using
    descOfIsLeftKanExtension_fac
      (α := whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)
      (β := L.pointwiseLeftKanExtensionUnit <| F ⋙ G)

Premises used: CategoryTheory.Functor.pointwiseLeftKanExtensionUnit, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.Functor.whiskerRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves, CategoryTheory.Functor.descOfIsLeftKanExtension_fac, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesPointwiseLeftKanExtension F L
inst_5 : L.HasPointwiseLeftKanExtension F
a : A
⊢ Eq (α := G.obj (F.obj a) ⟶ (L.pointwiseLeftKanExtension (F ⋙ G)).obj (L.obj a))
    (CategoryStruct.comp (Y := G.obj ((L ⋙ L.pointwiseLeftKanExtension F).obj a))
        (G.map (NatTrans.app (L.pointwiseLeftKanExtensionUnit F) a))
        (NatTrans.app (Iso.hom (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L)) (L.obj a)) :
      G.obj (F.obj a) ⟶ (L.pointwiseLeftKanExtension (F ⋙ G)).obj (L.obj a))
    (NatTrans.app (L.pointwiseLeftKanExtensionUnit (F ⋙ G)) a :
      (F ⋙ G).obj a ⟶ (L ⋙ L.pointwiseLeftKanExtension (F ⋙ G)).obj a)

Tactic:
simpa [-pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac] using
    NatTrans.congr_app (pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac G F L) a

Premises used: CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac, CategoryTheory.NatTrans.congr_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesPointwiseLeftKanExtension F L
inst_5 : L.HasPointwiseLeftKanExtension F
⊢ CategoryStruct.comp (Y := L ⋙ L.pointwiseLeftKanExtension (F ⋙ G))
      (L.pointwiseLeftKanExtensionUnit (F ⋙ G) : F ⋙ G ⟶ L ⋙ L.pointwiseLeftKanExtension (F ⋙ G))
      (L.whiskerLeft (Iso.inv (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L)) :
        L ⋙ L.pointwiseLeftKanExtension (F ⋙ G) ⟶ L ⋙ L.pointwiseLeftKanExtension F ⋙ G) =
    whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫ (L.associator (L.pointwiseLeftKanExtension F) G).hom

Tactic:
simp [pointwiseLeftKanExtensionCompIsoOfPreserves]

Premises used: CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesPointwiseLeftKanExtension F L
inst_5 : L.HasPointwiseLeftKanExtension F
a : A
⊢ Eq (α := (F ⋙ G).obj a ⟶ (L.pointwiseLeftKanExtension F ⋙ G).obj (L.obj a))
    (CategoryStruct.comp (Y := (L ⋙ L.pointwiseLeftKanExtension (F ⋙ G)).obj a)
      (NatTrans.app (L.pointwiseLeftKanExtensionUnit (F ⋙ G)) a :
        (F ⋙ G).obj a ⟶ (L ⋙ L.pointwiseLeftKanExtension (F ⋙ G)).obj a)
      (NatTrans.app (Iso.inv (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L)) (L.obj a) :
        (L.pointwiseLeftKanExtension (F ⋙ G)).obj (L.obj a) ⟶ (L.pointwiseLeftKanExtension F ⋙ G).obj (L.obj a)))
    (G.map (NatTrans.app (L.pointwiseLeftKanExtensionUnit F) a))

Tactic:
simpa [-pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac G F L) a

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesLeftKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasLeftKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
hγ :
  (whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
      L.whiskerLeft
        ((L.lan ⋙ obj (whiskeringRight C B D) G).map η ≫
          Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.leftKanExtensionCompIsoOfPreserves F L : L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)))
              F')) =
    (whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
      L.whiskerLeft
        (Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.leftKanExtensionCompIsoOfPreserves F L : L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)))
              F) ≫
          (obj (whiskeringRight A B D) G ⋙ L.lan).map η)
⊢ (L.lan ⋙ obj (whiskeringRight C B D) G).map η ≫
      Iso.hom
        ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
            (G.leftKanExtensionCompIsoOfPreserves F L : L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)))
          F') =
    Iso.hom
        ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
            (G.leftKanExtensionCompIsoOfPreserves F L : L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)))
          F) ≫
      (obj (whiskeringRight A B D) G ⋙ L.lan).map η

Tactic:
apply hom_ext_of_isLeftKanExtension (L.leftKanExtension F ⋙ G)
        (whiskerRight (L.leftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.Functor.leftKanExtension, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.Functor.leftKanExtensionUnit, CategoryTheory.Functor.whiskerRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesLeftKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasLeftKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
hγ :
  Eq (α := F ⋙ G ⟶ L ⋙ L.leftKanExtension (F' ⋙ G))
    ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
        CategoryStruct.comp (Y := L ⋙ L.leftKanExtension F' ⋙ G)
          (L.whiskerLeft
            (whiskerRight
              ((L.leftKanExtension F).descOfIsLeftKanExtension (L.leftKanExtensionUnit F) (L.leftKanExtension F')
                (η ≫ L.leftKanExtensionUnit F'))
              G))
          (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F' L))) :
      F ⋙ G ⟶ L ⋙ L.leftKanExtension (F' ⋙ G))
    ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
        CategoryStruct.comp (Y := L ⋙ L.leftKanExtension (F ⋙ G))
          (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F L)) :
            L ⋙ L.leftKanExtension F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))
          (L.whiskerLeft
              ((L.leftKanExtension (F ⋙ G)).descOfIsLeftKanExtension (L.leftKanExtensionUnit (F ⋙ G))
                (L.leftKanExtension (F' ⋙ G)) (whiskerRight η G ≫ L.leftKanExtensionUnit (F' ⋙ G))) :
            L ⋙ L.leftKanExtension (F ⋙ G) ⟶ L ⋙ L.leftKanExtension (F' ⋙ G)) :
      F ⋙ G ⟶ L ⋙ L.leftKanExtension (F' ⋙ G))
⊢ (whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
      L.whiskerLeft
        ((L.lan ⋙ obj (whiskeringRight C B D) G).map η ≫
          Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.leftKanExtensionCompIsoOfPreserves F L : L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)))
              F')) =
    (whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
      L.whiskerLeft
        (Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.leftKanExtensionCompIsoOfPreserves F L : L.leftKanExtension F ⋙ G ≅ L.leftKanExtension (F ⋙ G)))
              F) ≫
          (obj (whiskeringRight A B D) G ⋙ L.lan).map η)

Tactic:
dsimp [lan]

Premises used: CategoryTheory.Functor.lan
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesLeftKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasLeftKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
x : A
⊢ Eq (α := (F ⋙ G).obj x ⟶ (L ⋙ L.leftKanExtension (F' ⋙ G)).obj x)
    (NatTrans.app
        ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          CategoryStruct.comp (Y := L ⋙ L.leftKanExtension F' ⋙ G)
            (L.whiskerLeft
              (whiskerRight
                ((L.leftKanExtension F).descOfIsLeftKanExtension (L.leftKanExtensionUnit F) (L.leftKanExtension F')
                  (η ≫ L.leftKanExtensionUnit F'))
                G))
            (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F' L))))
        x :
      (F ⋙ G).obj x ⟶ (L ⋙ L.leftKanExtension (F' ⋙ G)).obj x)
    (NatTrans.app
        ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          CategoryStruct.comp (Y := L ⋙ L.leftKanExtension (F ⋙ G))
            (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F L)) :
              L ⋙ L.leftKanExtension F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))
            (L.whiskerLeft
                ((L.leftKanExtension (F ⋙ G)).descOfIsLeftKanExtension (L.leftKanExtensionUnit (F ⋙ G))
                  (L.leftKanExtension (F' ⋙ G)) (whiskerRight η G ≫ L.leftKanExtensionUnit (F' ⋙ G))) :
              L ⋙ L.leftKanExtension (F ⋙ G) ⟶ L ⋙ L.leftKanExtension (F' ⋙ G)))
        x :
      (F ⋙ G).obj x ⟶ (L ⋙ L.leftKanExtension (F' ⋙ G)).obj x)

Tactic:
simp [← G.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
F' : Functor.{v_3, v_2, u_3, u_2} C B
α : L ⋙ F' ⟶ F
inst_4 : F'.IsRightKanExtension α
h_1 : (F' ⋙ G).IsRightKanExtension ((L.associator F' G).inv ≫ whiskerRight α G)
F'' : Functor.{v_3, v_2, u_3, u_2} C B
α' : L ⋙ F'' ⟶ F
h : F''.IsRightKanExtension α'
w :
  ∀ (x : A),
    (L.whiskerLeft (isoWhiskerRight (F'.rightKanExtensionUnique α F'' α') G).hom ≫
            (L.associator F'' G).inv ≫ whiskerRight α' G).app
        x =
      ((L.associator F' G).inv ≫ whiskerRight α G).app x
⊢ L.whiskerLeft (isoWhiskerRight (F'.rightKanExtensionUnique α F'' α') G).hom ≫
      (L.associator F'' G).inv ≫ whiskerRight α' G =
    (L.associator F' G).inv ≫ whiskerRight α G

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
F' : Functor.{v_3, v_2, u_3, u_2} C B
α : L ⋙ F' ⟶ F
inst_4 : F'.IsRightKanExtension α
h_1 : (F' ⋙ G).IsRightKanExtension ((L.associator F' G).inv ≫ whiskerRight α G)
F'' : Functor.{v_3, v_2, u_3, u_2} C B
α' : L ⋙ F'' ⟶ F
h : F''.IsRightKanExtension α'
x : A
⊢ (L.whiskerLeft (isoWhiskerRight (F'.rightKanExtensionUnique α F'' α') G).hom ≫
          (L.associator F'' G).inv ≫ whiskerRight α' G).app
      x =
    ((L.associator F' G).inv ≫ whiskerRight α G).app x

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
E : L.RightExtension F
hE : CostructuredArrow.IsUniversal E
h : Nonempty (CostructuredArrow.IsUniversal ((RightExtension.postcompose₂ L F G).obj E))
⊢ G.PreservesRightKanExtension F L

Tactic:
.mk' G F L fun hE' ↦
    ⟨Limits.IsTerminal.equivOfIso
      (RightExtension.postcompose₂ L F G |>.mapIso
        <| Limits.IsTerminal.uniqueUpToIso hE hE') h.some⟩

Premises used: CategoryTheory.Limits.IsTerminal.equivOfIso, CategoryTheory.Functor.PreservesRightKanExtension.mk', CategoryTheory.Limits.IsTerminal.uniqueUpToIso, Nonempty.some, CategoryTheory.Functor.RightExtension.postcompose₂, Nonempty.intro, DFunLike.coe, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : L.HasRightKanExtension F
inst_5 : G.PreservesRightKanExtension F L
⊢ (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : L.HasPointwiseRightKanExtension F
inst_5 : G.PreservesPointwiseRightKanExtension F L
⊢ L.HasPointwiseRightKanExtension (F ⋙ G)

Tactic:
(pointwiseRightKanExtensionIsPointwiseRightKanExtension
    L F |>.postcompose G).hasPointwiseRightKanExtension

Premises used: CategoryTheory.Functor.pointwiseRightKanExtensionIsPointwiseRightKanExtension, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.postcompose, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtension F L
inst_5 : L.HasRightKanExtension F
⊢ CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F ⋙ G))
      (L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F L)) :
        L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F ⋙ G))
      (L.rightKanExtensionCounit (F ⋙ G) : L ⋙ L.rightKanExtension (F ⋙ G) ⟶ F ⋙ G) =
    (L.associator (L.rightKanExtension F) G).inv ≫ whiskerRight (L.rightKanExtensionCounit F) G

Tactic:
simp [rightKanExtensionCompIsoOfPreserves]

Premises used: CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtension F L
inst_5 : L.HasRightKanExtension F
a : A
⊢ Eq (α := (L.rightKanExtension F ⋙ G).obj (L.obj a) ⟶ (F ⋙ G).obj a)
    (CategoryStruct.comp (Y := (L.rightKanExtension (F ⋙ G)).obj (L.obj a))
      (NatTrans.app (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F L)) (L.obj a) :
        (L.rightKanExtension F ⋙ G).obj (L.obj a) ⟶ (L.rightKanExtension (F ⋙ G)).obj (L.obj a))
      (NatTrans.app (L.rightKanExtensionCounit (F ⋙ G)) a : (L ⋙ L.rightKanExtension (F ⋙ G)).obj a ⟶ (F ⋙ G).obj a))
    (G.map (NatTrans.app (L.rightKanExtensionCounit F) a))

Tactic:
simp [rightKanExtensionCompIsoOfPreserves]

Premises used: CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtension F L
inst_5 : L.HasRightKanExtension F
a : A
⊢ Eq (α := (L.rightKanExtension (F ⋙ G)).obj (L.obj a) ⟶ G.obj (F.obj a))
    (CategoryStruct.comp (Y := (L.rightKanExtension F ⋙ G).obj (L.obj a))
        (NatTrans.app (Iso.inv (G.rightKanExtensionCompIsoOfPreserves F L)) (L.obj a))
        (G.map (NatTrans.app (L.rightKanExtensionCounit F) a)) :
      (L.rightKanExtension (F ⋙ G)).obj (L.obj a) ⟶ G.obj (F.obj a))
    (NatTrans.app (L.rightKanExtensionCounit (F ⋙ G)) a : (L ⋙ L.rightKanExtension (F ⋙ G)).obj a ⟶ (F ⋙ G).obj a)

Tactic:
simpa [-rightKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (rightKanExtensionCompIsoOfPreserves_inv_fac G F L) a

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_inv_fac
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesPointwiseRightKanExtension F L
inst_5 : L.HasPointwiseRightKanExtension F
a : A
⊢ Eq (α := (L.pointwiseRightKanExtension F ⋙ G).obj (L.obj a) ⟶ (F ⋙ G).obj a)
    (CategoryStruct.comp (Y := (L.pointwiseRightKanExtension (F ⋙ G)).obj (L.obj a))
      (NatTrans.app (Iso.hom (G.pointwiseRightKanExtensionCompIsoOfPreserves F L)) (L.obj a) :
        (L.pointwiseRightKanExtension F ⋙ G).obj (L.obj a) ⟶ (L.pointwiseRightKanExtension (F ⋙ G)).obj (L.obj a))
      (NatTrans.app (L.pointwiseRightKanExtensionCounit (F ⋙ G)) a :
        (L ⋙ L.pointwiseRightKanExtension (F ⋙ G)).obj a ⟶ (F ⋙ G).obj a))
    (G.map (NatTrans.app (L.pointwiseRightKanExtensionCounit F) a))

Tactic:
simpa [-pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac] using
    NatTrans.congr_app (pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac G F L) a

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesPointwiseRightKanExtension F L
inst_5 : L.HasPointwiseRightKanExtension F
⊢ Eq (α := L ⋙ L.pointwiseRightKanExtension (F ⋙ G) ⟶ F ⋙ G)
    (L.whiskerLeft (Iso.inv (G.pointwiseRightKanExtensionCompIsoOfPreserves F L)) ≫
        (L.associator (L.pointwiseRightKanExtension F) G).inv ≫ whiskerRight (L.pointwiseRightKanExtensionCounit F) G :
      L ⋙ L.pointwiseRightKanExtension (F ⋙ G) ⟶ F ⋙ G)
    (L.pointwiseRightKanExtensionCounit (F ⋙ G) : L ⋙ L.pointwiseRightKanExtension (F ⋙ G) ⟶ F ⋙ G)

Tactic:
simp [pointwiseRightKanExtensionCompIsoOfPreserves]

Premises used: CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves