awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
simp :
  Eq (α := limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶ F.obj X₂)
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))) :
      limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶
        (StructuredArrow.proj (L.obj X₁) L ⋙ F).obj (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))))
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f)
⊢ Eq (α := (L ⋙ L.pointwiseRightKanExtension F).obj X₁ ⟶ F.obj X₂)
    ((L ⋙ L.pointwiseRightKanExtension F).map f ≫
        limit.π (StructuredArrow.proj (L.obj X₂) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₂))) :
      (L ⋙ L.pointwiseRightKanExtension F).obj X₁ ⟶ F.obj X₂)
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f :
      (L ⋙ L.pointwiseRightKanExtension F).obj X₁ ⟶ F.obj X₂)

Tactic:
simp only [comp_obj, pointwiseRightKanExtension_obj, comp_map,
      pointwiseRightKanExtension_map, limit.lift_π, StructuredArrow.map_mk]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.pointwiseRightKanExtension_obj, CategoryTheory.StructuredArrow.map_mk, CategoryTheory.Functor.pointwiseRightKanExtension_map, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
rw :
  Eq (α := limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶ F.obj X₂)
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f)) :
      limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶
        (StructuredArrow.proj (L.obj X₁) L ⋙ F).obj (StructuredArrow.mk (L.map f)))
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f)
⊢ Eq (α := limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶ F.obj X₂)
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))) :
      limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶
        (StructuredArrow.proj (L.obj X₁) L ⋙ F).obj (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))))
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f)

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : StructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) := StructuredArrow.homMk f ⋯
⊢ Eq (α := limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶ F.obj X₂)
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f)) :
      limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶
        (StructuredArrow.proj (L.obj X₁) L ⋙ F).obj (StructuredArrow.mk (L.map f)))
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f)

Tactic:
(limit.w (StructuredArrow.proj (L.obj X₁) L ⋙ F) φ).symm

Premises used: CategoryTheory.Functor.comp, Eq.symm, CategoryTheory.StructuredArrow.proj, CategoryTheory.Functor.obj, CategoryTheory.Limits.limit.w
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : StructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) := StructuredArrow.homMk f ⋯
⊢ Eq (α := limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶ F.obj X₂)
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f)) :
      limit (StructuredArrow.proj (L.obj X₁) L ⋙ F) ⟶
        (StructuredArrow.proj (L.obj X₁) L ⋙ F).obj (StructuredArrow.mk (L.map f)))
    (limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f)

Tactic:
exact (limit.w (StructuredArrow.proj (L.obj X₁) L ⋙ F) φ).symm

Premises used: CategoryTheory.Functor.comp, Eq.symm, CategoryTheory.StructuredArrow.proj, CategoryTheory.Functor.obj, CategoryTheory.Limits.limit.w
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
dsimp :
  limit.π (StructuredArrow.proj X L ⋙ F) j =
    𝟙 (limit (StructuredArrow.proj X L ⋙ F)) ≫
      CategoryStruct.comp (Y := limit (StructuredArrow.proj (L.obj j.right) L ⋙ F))
        (limit.lift (StructuredArrow.proj (L.obj j.right) L ⋙ F)
          { pt := limit (StructuredArrow.proj X L ⋙ F),
            π :=
              {
                app := fun (g : StructuredArrow (L.obj j.right) L) ↦
                  limit.π (StructuredArrow.proj X L ⋙ F) (obj (StructuredArrow.map j.hom) g),
                naturality := ⋯ :
                NatTrans (obj (const (StructuredArrow (L.obj j.right) L)) (limit (StructuredArrow.proj X L ⋙ F)))
                  (StructuredArrow.proj (L.obj j.right) L ⋙ F) } :
            Cone (StructuredArrow.proj (L.obj j.right) L ⋙ F) })
        (limit.π (StructuredArrow.proj (L.obj j.right) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj j.right))))
⊢ (limit.cone (StructuredArrow.proj X L ⋙ F)).π.app j =
    Iso.hom (Iso.refl (limit.cone (StructuredArrow.proj X L ⋙ F)).pt) ≫
      ((RightExtension.mk (L.pointwiseRightKanExtension F) (L.pointwiseRightKanExtensionCounit F)).coneAt X).π.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
simp :
  Eq (α := limit (StructuredArrow.proj X L ⋙ F) ⟶ F.obj j.right) (limit.π (StructuredArrow.proj X L ⋙ F) j)
    (limit.π (StructuredArrow.proj X L ⋙ F) (StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))))
⊢ limit.π (StructuredArrow.proj X L ⋙ F) j =
    𝟙 (limit (StructuredArrow.proj X L ⋙ F)) ≫
      CategoryStruct.comp (Y := limit (StructuredArrow.proj (L.obj j.right) L ⋙ F))
        (limit.lift (StructuredArrow.proj (L.obj j.right) L ⋙ F)
          { pt := limit (StructuredArrow.proj X L ⋙ F),
            π :=
              {
                app := fun (g : StructuredArrow (L.obj j.right) L) ↦
                  limit.π (StructuredArrow.proj X L ⋙ F) (obj (StructuredArrow.map j.hom) g),
                naturality := ⋯ :
                NatTrans (obj (const (StructuredArrow (L.obj j.right) L)) (limit (StructuredArrow.proj X L ⋙ F)))
                  (StructuredArrow.proj (L.obj j.right) L ⋙ F) } :
            Cone (StructuredArrow.proj (L.obj j.right) L ⋙ F) })
        (limit.π (StructuredArrow.proj (L.obj j.right) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj j.right))))

Tactic:
simp only [limit.lift_π, StructuredArrow.map_mk, id_comp]

Premises used: CategoryTheory.StructuredArrow.map_mk, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
h : j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))
⊢ Eq (α := limit (StructuredArrow.proj X L ⋙ F) ⟶ F.obj j.right) (limit.π (StructuredArrow.proj X L ⋙ F) j)
    (limit.π (StructuredArrow.proj X L ⋙ F) (StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
h : j = StructuredArrow.mk j.hom
h₁ h₂ : j = j
⊢ j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))

Tactic:
rw [comp_id, ← StructuredArrow.eq_mk]

Premises used: CategoryTheory.StructuredArrow.eq_mk, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
⊢ L.HasRightKanExtension F

Tactic:
HasRightKanExtension.mk _ (pointwiseRightKanExtensionCounit L F)

Premises used: CategoryTheory.Functor.pointwiseRightKanExtensionCounit, CategoryTheory.Functor.HasRightKanExtension.mk
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseRightKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : L ⋙ G ⟶ F
Y : D
⊢ ∀ ⦃X Y_1 : StructuredArrow Y L⦄ (f : X ⟶ Y_1),
    map (obj (const (StructuredArrow Y L)) (G.obj Y)) f ≫ G.map Y_1.hom ≫ α.app Y_1.right =
      (G.map X.hom ≫ α.app X.right) ≫ (StructuredArrow.proj Y L ⋙ F).map f

Tactic:
simp [← α.naturality, ← G.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseRightKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun (Y : D) ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
hγ :
  L.whiskerLeft
        ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α) ≫
      L.pointwiseRightKanExtensionCounit F =
    L.whiskerLeft β ≫ L.pointwiseRightKanExtensionCounit F
⊢ (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β

Tactic:
apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit L F)

Premises used: CategoryTheory.Functor.pointwiseRightKanExtensionCounit, CategoryTheory.Functor.hom_ext_of_isRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseRightKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun (Y : D) ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ L.whiskerLeft
        ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α) ≫
      L.pointwiseRightKanExtensionCounit F =
    L.whiskerLeft β ≫ L.pointwiseRightKanExtensionCounit F

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseRightKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun (Y : D) ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β

Tactic:
have h : (pointwiseRightKanExtension L F).liftOfIsRightKanExtension
      (pointwiseRightKanExtensionCounit L F) G α = β := by
    apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit L F)
    aesop
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseRightKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun (Y : D) ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
h : (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
NatTrans.congr_app h Y

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Limits.limit.lift
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_3 : L.HasPointwiseRightKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun (Y : D) ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
h : (L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α = β
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
exact NatTrans.congr_app h Y

Premises used: 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
F' : Functor.{v_3, v_2, u_3, u_2} C B
α : F ⟶ L ⋙ F'
inst_4 : F'.IsLeftKanExtension α
h_1 : (F' ⋙ G).IsLeftKanExtension (whiskerRight α G ≫ (L.associator F' G).hom)
F'' : Functor.{v_3, v_2, u_3, u_2} C B
α' : F ⟶ L ⋙ F''
h : F''.IsLeftKanExtension α'
w :
  ∀ (x : A),
    ((whiskerRight α G ≫ (L.associator F' G).hom) ≫
            L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom).app
        x =
      (whiskerRight α' G ≫ (L.associator F'' G).hom).app x
⊢ (whiskerRight α G ≫ (L.associator F' G).hom) ≫
      L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom =
    whiskerRight α' G ≫ (L.associator F'' G).hom

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
α : F ⟶ L ⋙ F'
inst_4 : F'.IsLeftKanExtension α
h_1 : (F' ⋙ G).IsLeftKanExtension (whiskerRight α G ≫ (L.associator F' G).hom)
F'' : Functor.{v_3, v_2, u_3, u_2} C B
α' : F ⟶ L ⋙ F''
h : F''.IsLeftKanExtension α'
x : A
⊢ ((whiskerRight α G ≫ (L.associator F' G).hom) ≫
          L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom).app
      x =
    (whiskerRight α' G ≫ (L.associator F'' G).hom).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.LeftExtension F
hE : StructuredArrow.IsUniversal E
h : Nonempty (StructuredArrow.IsUniversal ((LeftExtension.postcompose₂ L F G).obj E))
⊢ G.PreservesLeftKanExtension F L

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

Premises used: CategoryTheory.Limits.IsInitial.uniqueUpToIso, CategoryTheory.Functor.PreservesLeftKanExtension.mk', Nonempty.some, CategoryTheory.Functor.LeftExtension.postcompose₂, Nonempty.intro, CategoryTheory.Limits.IsInitial.equivOfIso, 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.HasLeftKanExtension F
inst_5 : G.PreservesLeftKanExtension F L
⊢ (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit 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.HasPointwiseLeftKanExtension F
inst_5 : G.PreservesPointwiseLeftKanExtension F L
⊢ L.HasPointwiseLeftKanExtension (F ⋙ G)

Tactic:
(pointwiseLeftKanExtensionIsPointwiseLeftKanExtension
    L F |>.postcompose G).hasPointwiseLeftKanExtension

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.postcompose, CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension
-- 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
⊢ Eq (α := F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))
    (whiskerRight (L.leftKanExtensionUnit F) G ≫
        (L.associator (L.leftKanExtension F) G).hom ≫
          L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F L)) :
      F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))
    (L.leftKanExtensionUnit (F ⋙ G) : F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))

Tactic:
simpa [leftKanExtensionCompIsoOfPreserves] using
    descOfIsLeftKanExtension_fac
      (α := whiskerRight (L.leftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)
      (β := L.leftKanExtensionUnit (F ⋙ G))

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.Functor.leftKanExtensionUnit, CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves, CategoryTheory.Functor.whiskerRight, CategoryTheory.CategoryStruct.comp, 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.PreservesLeftKanExtension F L
inst_5 : L.HasLeftKanExtension F
a : A
⊢ Eq (α := G.obj (F.obj a) ⟶ (L.leftKanExtension (F ⋙ G)).obj (L.obj a))
    (CategoryStruct.comp (Y := G.obj ((L ⋙ L.leftKanExtension F).obj a))
        (G.map (NatTrans.app (L.leftKanExtensionUnit F) a))
        (NatTrans.app (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F L)) (L.obj a)) :
      G.obj (F.obj a) ⟶ (L.leftKanExtension (F ⋙ G)).obj (L.obj a))
    (NatTrans.app (L.leftKanExtensionUnit (F ⋙ G)) a : (F ⋙ G).obj a ⟶ (L ⋙ L.leftKanExtension (F ⋙ G)).obj a)

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

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_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.PreservesLeftKanExtension F L
inst_5 : L.HasLeftKanExtension F
⊢ CategoryStruct.comp (Y := L ⋙ L.leftKanExtension (F ⋙ G))
      (L.leftKanExtensionUnit (F ⋙ G) : F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))
      (L.whiskerLeft (Iso.inv (G.leftKanExtensionCompIsoOfPreserves F L)) :
        L ⋙ L.leftKanExtension (F ⋙ G) ⟶ L ⋙ L.leftKanExtension F ⋙ G) =
    whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom

Tactic:
simp [leftKanExtensionCompIsoOfPreserves]

Premises used: CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves