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
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.ι (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 := ⋯ } } :
        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 := ⋯ } })
have simp : Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L X ⋙ F)) (colimit.ι (CostructuredArrow.proj L X ⋙ F) j)
  (colimit.ι (CostructuredArrow.proj L X ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)))
Tactic: simp only [comp_id, 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 : D
j : CostructuredArrow L X
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L X ⋙ F)) (colimit.ι (CostructuredArrow.proj L X ⋙ F) j)
    (colimit.ι (CostructuredArrow.proj L X ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)))
have h : j = CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)
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 : D
j : CostructuredArrow L X
⊢ j = CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)
have h : j = CostructuredArrow.mk j.hom
Tactic: rw [id_comp, ← CostructuredArrow.eq_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 : D
j : CostructuredArrow L X
h : j = CostructuredArrow.mk j.hom
⊢ j = CostructuredArrow.mk (𝟙 (L.obj j.left) ≫ j.hom)
have h₁ : j = j
Tactic: rw [id_comp, ← CostructuredArrow.eq_mk]
-- 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
inst_3 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun (Y : D) ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β
have hγ : L.pointwiseLeftKanExtensionUnit F ≫
    L.whiskerLeft ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α) =
  L.pointwiseLeftKanExtensionUnit F ≫ L.whiskerLeft β
Tactic: apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
-- 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
inst_3 : L.HasPointwiseLeftKanExtension F
G : Functor.{v_2, v_4, u_2, u_4} D H
α : F ⟶ L ⋙ G
Y : D
β : L.pointwiseLeftKanExtension F ⟶ G :=
  { app := fun (Y : D) ↦ colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y),
    naturality := ⋯ }
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)
have h : (L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α = β
Tactic: have h : (pointwiseLeftKanExtension L F).descOfIsLeftKanExtension
      (pointwiseLeftKanExtensionUnit L F) G α = β := by
    apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
    aesop
-- 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.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
⊢ CategoryStruct.comp (Y := limit (StructuredArrow.proj Y L ⋙ F))
      (limit.lift (StructuredArrow.proj Y L ⋙ F)
        { pt := limit (StructuredArrow.proj Y L ⋙ F),
          π :=
            {
              app := fun (g : StructuredArrow Y L) ↦
                limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) g),
              naturality := ⋯ } })
      (limit.π (StructuredArrow.proj Y L ⋙ F) j) =
    𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j
have simp : Eq (α := limit (StructuredArrow.proj Y L ⋙ F) ⟶ F.obj j.right)
  (limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) j))
  (limit.π (StructuredArrow.proj Y L ⋙ F) j)
Tactic: simp only [limit.lift_π, 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.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
⊢ Eq (α := limit (StructuredArrow.proj Y L ⋙ F) ⟶ F.obj j.right)
    (limit.π (StructuredArrow.proj Y L ⋙ F) (obj (StructuredArrow.map (𝟙 Y)) j))
    (limit.π (StructuredArrow.proj Y L ⋙ F) j)
have h : obj (StructuredArrow.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.HasPointwiseRightKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
⊢ Eq (α := limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶ F.obj j.right)
    (limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map (f ≫ f')) j) :
      limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶
        (StructuredArrow.proj Y₁ L ⋙ F).obj (obj (StructuredArrow.map (f ≫ f')) j))
    (limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) (obj (StructuredArrow.map f') j)))
have h : obj (StructuredArrow.map (f ≫ f')) j = obj (StructuredArrow.map f) (obj (StructuredArrow.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.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ 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₂)
have 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)
Tactic: simp only [comp_obj, pointwiseRightKanExtension_obj, comp_map,
      pointwiseRightKanExtension_map, limit.lift_π, StructuredArrow.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.HasPointwiseRightKanExtension F
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ 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)
have 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)
Tactic: rw [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.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ (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
have 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 := sorry :
              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: 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
inst_4 : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ 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))))
have 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))))
Tactic: simp only [limit.lift_π, StructuredArrow.map_mk, 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.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ 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))))
have h : j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))
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.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))
have h : j = StructuredArrow.mk j.hom
Tactic: rw [comp_id, ← StructuredArrow.eq_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.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
h : j = StructuredArrow.mk j.hom
⊢ j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))
have h₁ : j = j
Tactic: rw [comp_id, ← StructuredArrow.eq_mk]
-- 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
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 α = β
have hγ : L.whiskerLeft ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α) ≫
    L.pointwiseRightKanExtensionCounit F =
  L.whiskerLeft β ≫ L.pointwiseRightKanExtensionCounit F
Tactic: apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit L F)
-- 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
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 α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)
have h : (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Preserves (goal)
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 α'
⊢ (whiskerRight α G ≫ (L.associator F' G).hom) ≫
      L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom =
    whiskerRight α' G ≫ (L.associator F'' G).hom
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Preserves (goal)
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'
⊢ (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 η
have 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 η)
Tactic: apply hom_ext_of_isLeftKanExtension (L.leftKanExtension F ⋙ G)
        (whiskerRight (L.leftKanExtensionUnit F) G ≫ (Functor.associator _ _ _).hom)