awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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
⊢ (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
have 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
Tactic: rw [reassoc_of% eq₁, reassoc_of% eq₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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₂
⊢ 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 φ
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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).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
have 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
Tactic: rw [assoc, id_comp, ← StructuredArrow.w φ, Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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 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
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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 ≫ (E'.coneAt Y).π.app G = (E.coneAt Y).π.app G
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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 ≫ (CostructuredArrow.hom E).app G.right
have 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
Tactic: rw [← CostructuredArrow.w φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
⊢ ((CostructuredArrow.left G).map φ ≫ (h Y₂).lift (G.coneAt Y₂)) ≫ (E.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X
have rw : (CostructuredArrow.left G).map φ ≫ (G.coneAt Y₂).π.app X =
  ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X
Tactic: rw [assoc, (h Y₂).fac (coneAt G Y₂) X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
⊢ map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
      CostructuredArrow.hom E =
    CostructuredArrow.hom G
have w : ∀ (X : C),
  NatTrans.app
      (map (obj (whiskeringLeft C D H) L) { app := fun (Y : D) ↦ (h Y).lift (G.coneAt Y), naturality := sorry } ≫
        CostructuredArrow.hom E)
      X =
    (CostructuredArrow.hom G).app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
⊢ f₁ = f₂
have h₁ : ∀ (Y : D), f₁.left.app Y = f₂.left.app Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ f₁.left.app Y = f₂.left.app Y
have h₁ : ∀ (j : StructuredArrow Y L), f₁.left.app Y ≫ (E.coneAt Y).π.app j = f₂.left.app Y ≫ (E.coneAt Y).π.app j
Tactic: apply (h Y).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (hypothesis)
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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X
have eq₁ : Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
  ((map (obj (whiskeringLeft C D H) L) f₁.left ≫ CostructuredArrow.hom E).app X.right)
  ((CostructuredArrow.hom G).app X.right)
Tactic: have eq₁ := congr_app (CostructuredArrow.w f₁) X.right
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (hypothesis)
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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₁.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X
have eq₂ : Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
  ((map (obj (whiskeringLeft C D H) L) f₂.left ≫ CostructuredArrow.hom E).app X.right)
  ((CostructuredArrow.hom G).app X.right)
Tactic: have eq₂ := congr_app (CostructuredArrow.w f₂) X.right
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₁.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)
eq₂ :
  Eq (α := (obj (obj (whiskeringLeft C D H) L) G.left).obj X.right ⟶ F.obj X.right)
    ((map (obj (whiskeringLeft C D H) L) f₂.left ≫ CostructuredArrow.hom E).app X.right)
    ((CostructuredArrow.hom G).app X.right)
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X
have h₁ : f₁.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right =
  f₂.left.app Y ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right
Tactic: dsimp at eq₁ eq₂ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.HasPointwiseLeftKanExtension F
Y : D
j : CostructuredArrow L Y
⊢ CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y ⋙ F)) (colimit.ι (CostructuredArrow.proj L Y ⋙ F) j)
      (colimit.desc (CostructuredArrow.proj L Y ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y ⋙ F),
          ι :=
            {
              app := fun (g : CostructuredArrow L Y) ↦
                colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } }) =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))
have simp : Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y ⋙ F))
  (colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) j))
  (colimit.ι (CostructuredArrow.proj L Y ⋙ F) j)
Tactic: simp only [colimit.ι_desc, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.HasPointwiseLeftKanExtension F
Y : D
j : CostructuredArrow L Y
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y ⋙ F) (obj (CostructuredArrow.map (𝟙 Y)) j))
    (colimit.ι (CostructuredArrow.proj L Y ⋙ F) j)
have h : obj (CostructuredArrow.map (𝟙 Y)) j = j
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y₁ ⋙ F))
        (colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j)
        (colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              {
                app := fun (g : CostructuredArrow L Y₁) ↦
                  colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map (f ≫ f')) g),
                naturality := ⋯ } }) :
      F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y₁ ⋙ F))
        (colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j)
        (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y₂ ⋙ F))
          (colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
              { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
                ι :=
                  {
                    app := fun (g : CostructuredArrow L Y₁) ↦
                      colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) (obj (CostructuredArrow.map f) g),
                    naturality := ⋯ } } :
            colimit (CostructuredArrow.proj L Y₁ ⋙ F) ⟶
              Cocone.pt (J := CostructuredArrow L Y₁) (F := CostructuredArrow.proj L Y₁ ⋙ F)
                { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
                  ι :=
                    {
                      app := fun (g : CostructuredArrow L Y₁) ↦
                        colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) (obj (CostructuredArrow.map f) g),
                      naturality := ⋯ } })
          (colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
            { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
              ι :=
                {
                  app := fun (g : CostructuredArrow L Y₂) ↦
                    colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map f') g),
                  naturality := ⋯ } })) :
      F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
have simp : Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
  (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map (f ≫ f')) j) :
    (CostructuredArrow.proj L Y₃ ⋙ F).obj (obj (CostructuredArrow.map (f ≫ f')) j) ⟶
      colimit (CostructuredArrow.proj L Y₃ ⋙ F))
  (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map f') (obj (CostructuredArrow.map f) j)))
Tactic: simp only [colimit.ι_desc, colimit.ι_desc_assoc, comp_obj, CostructuredArrow.proj_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map (f ≫ f')) j) :
      (CostructuredArrow.proj L Y₃ ⋙ F).obj (obj (CostructuredArrow.map (f ≫ f')) j) ⟶
        colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map f') (obj (CostructuredArrow.map f) j)))
have h : obj (CostructuredArrow.map (f ≫ f')) j = obj (CostructuredArrow.map f') (obj (CostructuredArrow.map f) j)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))) =
    colimit.ι (CostructuredArrow.proj L (L.obj X₁) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁))) ≫
      (L ⋙ L.pointwiseLeftKanExtension F).map f
have simp : Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
  (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
  (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁) ≫ L.map f)))
Tactic: simp only [comp_obj, pointwiseLeftKanExtension_obj, comp_map,
      pointwiseLeftKanExtension_map, colimit.ι_desc, CostructuredArrow.map_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.HasPointwiseLeftKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
    (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
    (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₁) ≫ L.map f)))
have rw : Eq (α := F.obj X₁ ⟶ colimit (J := CostructuredArrow L (L.obj X₂)) (CostructuredArrow.proj L (L.obj X₂) ⋙ F))
  (F.map f ≫ colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X₂))))
  (colimit.ι (CostructuredArrow.proj L (L.obj X₂) ⋙ F) (CostructuredArrow.mk (L.map f)))
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Pointwise (goal)
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.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
⊢ (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).ι.app j ≫
      Iso.hom (Iso.refl (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).pt) =
    ((LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).coconeAt X).ι.app j
have dsimp : colimit.ι (CostructuredArrow.proj L X ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L X ⋙ F)) =
  CategoryStruct.comp (Y :=
    colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F))
    (colimit.ι (CostructuredArrow.proj L (L.obj j.left) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left))) :
      obj (CostructuredArrow.proj L (L.obj j.left) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left))) ⟶
        colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F))
    (colimit.desc (CostructuredArrow.proj L (L.obj j.left) ⋙ F)
        { pt := colimit (CostructuredArrow.proj L X ⋙ F),
          ι :=
            {
              app := fun (g : CostructuredArrow L (L.obj j.left)) ↦
                colimit.ι (CostructuredArrow.proj L X ⋙ F) (obj (CostructuredArrow.map j.hom) g),
              naturality := sorry } } :
      colimit (J := CostructuredArrow L (L.obj j.left)) (CostructuredArrow.proj L (L.obj j.left) ⋙ F) ⟶
        Cocone.pt (J := CostructuredArrow L (L.obj j.left)) (F := CostructuredArrow.proj L (L.obj j.left) ⋙ F)
          { pt := colimit (CostructuredArrow.proj L X ⋙ F),
            ι :=
              {
                app := fun (g : CostructuredArrow L (L.obj j.left)) ↦
                  colimit.ι (CostructuredArrow.proj L X ⋙ F) (obj (CostructuredArrow.map j.hom) g),
                naturality := sorry } })
Tactic: dsimp