awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
T : H
f g : (StructuredArrow.right E).obj Y ⟶ T
hfg :
  ∀ ⦃X : C⦄ (φ : L.obj X ⟶ Y),
    (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ f =
      (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ g
j : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app j ≫ f = (E.coconeAt Y).ι.app j ≫ g

Tactic:
simpa using hfg j.hom

Premises used: CategoryTheory.CostructuredArrow.hom
-- 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
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
Z : H
φ : CostructuredArrow.proj L Y ⋙ F ⟶ obj (const (CostructuredArrow L Y)) Z
g : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app g.left ≫
      (StructuredArrow.right E).map g.hom ≫
        (Equiv.symm (IsColimit.homEquiv h) :
            (a : CostructuredArrow.proj L Y ⋙ F ⟶ (const (CostructuredArrow L Y)).obj Z) → (E.coconeAt Y).pt ⟶ Z)
          φ =
    φ.app g

Tactic:
simpa using h.ι_app_homEquiv_symm φ g

Premises used: CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm
-- 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
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
inst_3 : HasColimit (CostructuredArrow.proj L Y ⋙ F)
g : CostructuredArrow L Y
⊢ CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y ⋙ F)) (colimit.ι (CostructuredArrow.proj L Y ⋙ F) g)
      (Iso.inv h.isoColimit) =
    (StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- 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
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
inst_3 : HasColimit (CostructuredArrow.proj L Y ⋙ F)
g : CostructuredArrow L Y
⊢ Eq (α := F.obj g.left ⟶ colimit (CostructuredArrow.proj L Y ⋙ F))
    ((StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom ≫ Iso.hom h.isoColimit)
    (colimit.ι (CostructuredArrow.proj L Y ⋙ F) g)

Tactic:
simpa using h.comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) g

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
-- 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
E E' : L.LeftExtension F
e : E ≅ E'
h : E.IsPointwiseLeftKanExtension
⊢ (fun (h : E'.IsPointwiseLeftKanExtension) (Y : D) ↦
        (((isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm :
              (a : E'.IsPointwiseLeftKanExtensionAt Y) → E.IsPointwiseLeftKanExtensionAt Y)
            (h Y) :
          E.IsPointwiseLeftKanExtensionAt Y))
      ((fun (h : E.IsPointwiseLeftKanExtension) (Y : D) ↦
          ((isPointwiseLeftKanExtensionAtEquivOfIso e Y :
                (a : E.IsPointwiseLeftKanExtensionAt Y) → E'.IsPointwiseLeftKanExtensionAt Y)
              (h Y) :
            E'.IsPointwiseLeftKanExtensionAt Y))
        h) =
    h

Tactic:
simp
-- 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
E E' : L.LeftExtension F
e : E ≅ E'
h : E'.IsPointwiseLeftKanExtension
⊢ (fun (h : E.IsPointwiseLeftKanExtension) (Y : D) ↦
        ((isPointwiseLeftKanExtensionAtEquivOfIso e Y :
              (a : E.IsPointwiseLeftKanExtensionAt Y) → E'.IsPointwiseLeftKanExtensionAt Y)
            (h Y) :
          E'.IsPointwiseLeftKanExtensionAt Y))
      ((fun (h : E'.IsPointwiseLeftKanExtension) (Y : D) ↦
          (((isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm :
                (a : E'.IsPointwiseLeftKanExtensionAt Y) → E.IsPointwiseLeftKanExtensionAt Y)
              (h Y) :
            E.IsPointwiseLeftKanExtensionAt Y))
        h) =
    h

Tactic:
simp
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
⊢ L.HasPointwiseLeftKanExtension F

Tactic:
fun Y => (h Y).hasPointwiseLeftKanExtensionAt

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt
-- 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
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
rw :
  (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (G.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right G).map φ
⊢ Eq (α := (CostructuredArrow.proj L Y₁ ⋙ F).obj X ⟶ (StructuredArrow.right G).obj Y₂)
    ((E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) :
      (CostructuredArrow.proj L Y₁ ⋙ F).obj X ⟶ (StructuredArrow.right G).obj Y₂)
    ((E.coconeAt Y₁).ι.app X ≫ (h Y₁).desc (G.coconeAt Y₁) ≫ (StructuredArrow.right G).map φ :
      (CostructuredArrow.proj L Y₁ ⋙ F).obj X ⟶ (StructuredArrow.right G).obj Y₂)

Tactic:
rw [(h Y₁).fac_assoc (coconeAt G Y₁) X]

Premises used: CategoryTheory.Functor.LeftExtension.coconeAt, CategoryTheory.Limits.IsColimit.fac_assoc
-- 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
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (G.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right G).map φ

Tactic:
simpa using (h Y₂).fac (coconeAt G Y₂) ((CostructuredArrow.map φ).obj X)

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.LeftExtension.coconeAt, CategoryTheory.CostructuredArrow.map, CategoryTheory.Functor.obj
-- 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
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
w :
  ∀ (X : C),
    NatTrans.app
        (StructuredArrow.hom E ≫
          map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ })
        X =
      (StructuredArrow.hom G).app X
⊢ StructuredArrow.hom E ≫
      map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ } =
    StructuredArrow.hom G

Tactic:
ext X
-- 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
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
X : C
⊢ NatTrans.app
      (StructuredArrow.hom E ≫
        map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ })
      X =
    (StructuredArrow.hom G).app X

Tactic:
simpa using (h (L.obj X)).fac (LeftExtension.coconeAt G _) (CostructuredArrow.mk (𝟙 _))

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.LeftExtension.coconeAt, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Functor.obj
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
h₁ : ∀ (Y : D), (StructuredArrow.Hom.right f₁).app Y = (StructuredArrow.Hom.right f₂).app Y
⊢ f₁ = f₂

Tactic:
ext Y
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
h₁ :
  ∀ (j : CostructuredArrow L Y),
    (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₁).app Y =
      (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₂).app Y
⊢ (StructuredArrow.Hom.right f₁).app Y = (StructuredArrow.Hom.right f₂).app Y

Tactic:
apply (h Y).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
⊢ Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₁)).app X.left)
    ((StructuredArrow.hom G).app X.left)

Tactic:
have eq₁ := congr_app (StructuredArrow.w f₁) X.left
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₁)).app X.left)
    ((StructuredArrow.hom G).app X.left)
⊢ Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₂)).app X.left)
    ((StructuredArrow.hom G).app X.left)

Tactic:
have eq₂ := congr_app (StructuredArrow.w f₂) X.left
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₁)).app X.left)
    ((StructuredArrow.hom G).app X.left)
eq₂ :
  Eq (α := F.obj X.left ⟶ (obj (obj (whiskeringLeft C D H) L) (StructuredArrow.right G)).obj X.left)
    ((StructuredArrow.hom E ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.Hom.right f₂)).app X.left)
    ((StructuredArrow.hom G).app X.left)
h₁ :
  ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₁).app Y =
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₂).app Y
⊢ (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₁).app Y =
    (E.coconeAt Y).ι.app X ≫ (StructuredArrow.Hom.right f₂).app Y

Tactic:
dsimp at eq₁ eq₂ ⊢
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₁).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
eq₂ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₂).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
h₁ :
  (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.Hom.right f₁).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom =
    (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.Hom.right f₂).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom
⊢ ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₁).app Y =
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.right E).map X.hom) ≫ (StructuredArrow.Hom.right f₂).app Y

Tactic:
simp only [assoc, NatTrans.naturality]

Premises used: CategoryTheory.Category.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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
X : CostructuredArrow L Y
eq₁ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₁).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
eq₂ :
  Eq (α := F.obj X.left ⟶ (StructuredArrow.right G).obj (L.obj X.left))
    ((StructuredArrow.hom E).app X.left ≫ (StructuredArrow.Hom.right f₂).app (L.obj X.left))
    ((StructuredArrow.hom G).app X.left)
h₁ :
  (StructuredArrow.hom G).app X.left ≫ (StructuredArrow.right G).map X.hom =
    (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.Hom.right f₂).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom
h₂ h₃ :
  (StructuredArrow.hom G).app X.left ≫ (StructuredArrow.right G).map X.hom =
    (StructuredArrow.hom G).app X.left ≫ (StructuredArrow.right G).map X.hom
⊢ (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.Hom.right f₁).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom =
    (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.Hom.right f₂).app (L.obj X.left) ≫ (StructuredArrow.right G).map X.hom

Tactic:
rw [reassoc_of% eq₁, reassoc_of% eq₂]
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
⊢ L.HasLeftKanExtension F

Tactic:
have := h.isLeftKanExtension
  HasLeftKanExtension.mk E.right E.hom

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.HasLeftKanExtension.mk, CategoryTheory.StructuredArrow.right
-- 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
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
inst_3 : L.Full
inst_4 : L.Faithful
⊢ IsIso (StructuredArrow.hom E)

Tactic:
have := fun X => (h (L.obj X)).isIso_hom_app
  NatIso.isIso_of_isIso_app ..

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app, CategoryTheory.NatIso.isIso_of_isIso_app, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.obj
-- 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
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
dsimp :
  𝟙 ((CostructuredArrow.left E).obj Y) ≫
      (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    ((CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right) ≫ F.map φ.right
⊢ map (obj (const (StructuredArrow Y L)) ((CostructuredArrow.left E).obj Y)) φ ≫
      (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    ((CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right) ≫
      (StructuredArrow.proj Y L ⋙ F).map φ

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
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
rw :
  (CostructuredArrow.left E).map g₁.hom ≫
      (CostructuredArrow.left E).map (L.map (StructuredArrow.Hom.right φ)) ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right
⊢ 𝟙 ((CostructuredArrow.left E).obj Y) ≫
      (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    ((CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right) ≫ F.map φ.right

Tactic:
rw [assoc, id_comp, ← StructuredArrow.w φ, Functor.map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.StructuredArrow.w, CategoryTheory.Functor.map_comp, 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
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
e_a :
  (CostructuredArrow.left E).map (L.map (StructuredArrow.Hom.right φ)) ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right
⊢ (CostructuredArrow.left E).map g₁.hom ≫
      (CostructuredArrow.left E).map (L.map (StructuredArrow.Hom.right φ)) ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right

Tactic:
congr 1
-- 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
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.left E).map (L.map (StructuredArrow.Hom.right φ)) ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right

Tactic:
apply E.hom.naturality

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.NatTrans.naturality
-- 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
E_1 E'_1 : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
dsimp :
  φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫ (CostructuredArrow.hom E).app G.right
⊢ φ.left.app Y ≫ (E'.coneAt Y).π.app G = (E.coneAt Y).π.app G

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
E_1 E'_1 : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
rw :
  φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫
      (map (obj (whiskeringLeft C D H) L) φ.left ≫ CostructuredArrow.hom E').app G.right
⊢ φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫ (CostructuredArrow.hom E).app G.right

Tactic:
rw [← CostructuredArrow.w φ]

Premises used: CategoryTheory.CostructuredArrow.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
E_1 E'_1 : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫
      (map (obj (whiskeringLeft C D H) L) φ.left ≫ CostructuredArrow.hom E').app G.right

Tactic:
simp