awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : F ⟶ L ⋙ F'
inst_5 : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this :
  Eq (α := F'.obj (L.obj j) ⟶ s.pt)
    (NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m) (s.ι.app (L.obj j))
rw :
  Eq (α := F.obj j ⟶ s.pt)
    (α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
⊢ Eq (α := F.obj j ⟶ s.pt)
    ((α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j)) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
have rw₁ : α.app j ≫ s.ι.app (L.obj j) = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }
Tactic: rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : F ⟶ L ⋙ F'
inst_5 : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this :
  Eq (α := F'.obj (L.obj j) ⟶ s.pt)
    (NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m) (s.ι.app (L.obj j))
rw :
  Eq (α := F.obj j ⟶ s.pt)
    (α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
rw₁ : α.app j ≫ s.ι.app (L.obj j) = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }
⊢ Eq (α := F.obj j ⟶ s.pt)
    ((α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j)) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
have rw₂ : α.app j ≫ s.ι.app (L.obj j) = { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }.ι.app j
Tactic: rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : F ⟶ L ⋙ F'
inst_5 : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this :
  Eq (α := F'.obj (L.obj j) ⟶ s.pt)
    (NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m) (s.ι.app (L.obj j))
rw :
  Eq (α := F.obj j ⟶ s.pt)
    (α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
rw₁ : α.app j ≫ s.ι.app (L.obj j) = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }
rw₂ : α.app j ≫ s.ι.app (L.obj j) = { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }.ι.app j
⊢ Eq (α := F.obj j ⟶ s.pt)
    ((α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j)) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
have rw₃ : α.app j ≫ s.ι.app (L.obj j) = α.app j ≫ (L.whiskerLeft s.ι).app j
Tactic: rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : F ⟶ L ⋙ F'
inst_5 : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this :
  Eq (α := F'.obj (L.obj j) ⟶ s.pt)
    (NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m) (s.ι.app (L.obj j))
rw :
  Eq (α := F.obj j ⟶ s.pt)
    (α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
rw₁ : α.app j ≫ s.ι.app (L.obj j) = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }
rw₂ : α.app j ≫ s.ι.app (L.obj j) = { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }.ι.app j
rw₃ : α.app j ≫ s.ι.app (L.obj j) = α.app j ≫ (L.whiskerLeft s.ι).app j
⊢ Eq (α := F.obj j ⟶ s.pt)
    ((α.app j ≫ NatTrans.app (F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι) (L.obj j)) ≫ m : F.obj j ⟶ s.pt)
    (c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } : F.obj j ⟶ s.pt)
have rw₄ : α.app j ≫ s.ι.app (L.obj j) = α.app j ≫ s.ι.app (L.obj j)
Tactic: rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : F ⟶ L ⋙ F'
inst_3 : F'.IsLeftKanExtension α
inst_4 : HasColimit F
inst_5 : HasColimit F'
i : C
⊢ Eq (α := F.obj i ⟶ colimit F')
    (CategoryStruct.comp (Y := colimit F) (colimit.ι F i) (Iso.inv (F'.colimitIsoOfIsLeftKanExtension α)))
    (α.app i ≫ colimit.ι F' (L.obj i))
have rw : Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
  (CategoryStruct.comp (Y := colimit F') (α.app i ≫ colimit.ι F' (L.obj i))
    (Iso.hom (F'.colimitIsoOfIsLeftKanExtension α)))
Tactic: rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : F ⟶ L ⋙ F'
inst_3 : F'.IsLeftKanExtension α
inst_4 : HasColimit F
inst_5 : HasColimit F'
i : C
rw :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    (CategoryStruct.comp (Y := colimit F') (α.app i ≫ colimit.ι F' (L.obj i))
      (Iso.hom (F'.colimitIsoOfIsLeftKanExtension α)))
⊢ Eq (α := F.obj i ⟶ colimit F')
    (CategoryStruct.comp (Y := colimit F) (colimit.ι F i) (Iso.inv (F'.colimitIsoOfIsLeftKanExtension α)))
    (α.app i ≫ colimit.ι F' (L.obj i))
have rw₁ : Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
  (α.app i ≫
    CategoryStruct.comp (Y := colimit F') (colimit.ι F' (L.obj i)) (Iso.hom (F'.colimitIsoOfIsLeftKanExtension α)))
Tactic: rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : F ⟶ L ⋙ F'
inst_3 : F'.IsLeftKanExtension α
inst_4 : HasColimit F
inst_5 : HasColimit F'
i : C
rw :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    (CategoryStruct.comp (Y := colimit F') (α.app i ≫ colimit.ι F' (L.obj i))
      (Iso.hom (F'.colimitIsoOfIsLeftKanExtension α)))
rw₁ :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    (α.app i ≫
      CategoryStruct.comp (Y := colimit F') (colimit.ι F' (L.obj i)) (Iso.hom (F'.colimitIsoOfIsLeftKanExtension α)))
⊢ Eq (α := F.obj i ⟶ colimit F')
    (CategoryStruct.comp (Y := colimit F) (colimit.ι F i) (Iso.inv (F'.colimitIsoOfIsLeftKanExtension α)))
    (α.app i ≫ colimit.ι F' (L.obj i))
have rw₂ : Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i) (colimit.ι F i)
Tactic: rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (hypothesis)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
⊢ ∀ (j : D), hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
have this : map (const D) (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α : Cone F }) ≫
    F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π =
  s.π
Tactic: have : (Functor.const _).map (hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))) ≫
        F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π = s.π :=
      F'.hom_ext_of_isRightKanExtension α _ _ (by cat_disch)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (hypothesis)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
⊢ m ≫ c.π.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
have this : Eq (α := s.pt ⟶ F'.obj (L.obj j)) (m ≫ (F'.coneOfIsRightKanExtension α c).π.app (L.obj j)) (s.π.app (L.obj j))
Tactic: have := hm (L.obj j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : Eq (α := s.pt ⟶ F'.obj (L.obj j)) (m ≫ (F'.coneOfIsRightKanExtension α c).π.app (L.obj j)) (s.π.app (L.obj j))
⊢ m ≫ c.π.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
have nth_rw : Eq (α := s.pt ⟶ F.obj j)
  (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j) ≫ α.app j)
  (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j)
Tactic: nth_rw 1 [← F'.liftOfIsRightKanExtension_fac_app α ((const D).obj c.pt)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this :
  Eq (α := s.pt ⟶ F'.obj (L.obj j))
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) (s.π.app (L.obj j))
⊢ Eq (α := s.pt ⟶ F.obj j)
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j) ≫ α.app j)
    (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j)
have rw : (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) ≫ α.app j =
  hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
Tactic: rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this :
  Eq (α := s.pt ⟶ F'.obj (L.obj j))
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) (s.π.app (L.obj j))
rw :
  (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
⊢ Eq (α := s.pt ⟶ F.obj j)
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j) ≫ α.app j)
    (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j)
have rw₁ : s.π.app (L.obj j) ≫ α.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
Tactic: rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this :
  Eq (α := s.pt ⟶ F'.obj (L.obj j))
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) (s.π.app (L.obj j))
rw :
  (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
rw₁ : s.π.app (L.obj j) ≫ α.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
⊢ Eq (α := s.pt ⟶ F.obj j)
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j) ≫ α.app j)
    (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j)
have rw₂ : s.π.app (L.obj j) ≫ α.app j = { pt := s.1, π := L.whiskerLeft s.π ≫ α }.π.app j
Tactic: rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this :
  Eq (α := s.pt ⟶ F'.obj (L.obj j))
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) (s.π.app (L.obj j))
rw :
  (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
rw₁ : s.π.app (L.obj j) ≫ α.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
rw₂ : s.π.app (L.obj j) ≫ α.app j = { pt := s.1, π := L.whiskerLeft s.π ≫ α }.π.app j
⊢ Eq (α := s.pt ⟶ F.obj j)
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j) ≫ α.app j)
    (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j)
have rw₃ : s.π.app (L.obj j) ≫ α.app j = (L.whiskerLeft s.π).app j ≫ α.app j
Tactic: rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this :
  Eq (α := s.pt ⟶ F'.obj (L.obj j))
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) (s.π.app (L.obj j))
rw :
  (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j)) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
rw₁ : s.π.app (L.obj j) ≫ α.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
rw₂ : s.π.app (L.obj j) ≫ α.app j = { pt := s.1, π := L.whiskerLeft s.π ≫ α }.π.app j
rw₃ : s.π.app (L.obj j) ≫ α.app j = (L.whiskerLeft s.π).app j ≫ α.app j
⊢ Eq (α := s.pt ⟶ F.obj j)
    (m ≫ NatTrans.app (F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π) (L.obj j) ≫ α.app j)
    (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j)
have rw₄ : s.π.app (L.obj j) ≫ α.app j = s.π.app (L.obj j) ≫ α.app j
Tactic: rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_3 : F'.IsRightKanExtension α
inst_4 : HasLimit F
inst_5 : HasLimit F'
i : C
⊢ Eq (α := limit F' ⟶ F.obj i)
    (CategoryStruct.comp (Y := limit F) (Iso.hom (F'.limitIsoOfIsRightKanExtension α)) (limit.π F i))
    (limit.π F' (L.obj i) ≫ α.app i)
have rw : Eq (α := limit F ⟶ F.obj i) (limit.π F i)
  (CategoryStruct.comp (Y := limit F') (Iso.inv (F'.limitIsoOfIsRightKanExtension α)) (limit.π F' (L.obj i) ≫ α.app i))
Tactic: rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
F' : Functor.{v_4, v_3, u_4, u_3} D H
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
inst_3 : F'.IsRightKanExtension α
inst_4 : HasLimit F
inst_5 : HasLimit F'
i : C
rw :
  Eq (α := limit F ⟶ F.obj i) (limit.π F i)
    (CategoryStruct.comp (Y := limit F') (Iso.inv (F'.limitIsoOfIsRightKanExtension α))
      (limit.π F' (L.obj i) ≫ α.app i))
⊢ Eq (α := limit F' ⟶ F.obj i)
    (CategoryStruct.comp (Y := limit F) (Iso.hom (F'.limitIsoOfIsRightKanExtension α)) (limit.π F i))
    (limit.π F' (L.obj i) ≫ α.app i)
have rw₁ : Eq (α := limit F ⟶ F.obj i) (limit.π F i) (limit.π F i)
Tactic: rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : F₀ ≅ L.functor ⋙ F₁
⊢ F₁.IsLeftKanExtension α.hom
have refine : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α.hom)
Tactic: refine ⟨⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : F₀ ≅ L.functor ⋙ F₁
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₁ α.hom)
have apply : StructuredArrow.IsUniversal
  ((LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom))
Tactic: apply LeftExtension.isUniversalPostcomp₁Equiv
    (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
inst_2 : Category.{v_3, u_3} H
inst_3 : Category.{v_4, u_4} D
inst_4 : Category.{v_5, u_5} D'
L : Equivalence.{v_1, v_4, u_1, u_4} C D
F₀ : Functor.{v_1, v_3, u_1, u_3} C H
F₁ : Functor.{v_4, v_3, u_4, u_3} D H
α : F₀ ≅ L.functor ⋙ F₁
⊢ StructuredArrow.IsUniversal
    ((LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom))
have refine : ∀ (Y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C)))
  (m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ Y),
  m =
    (fun (y : StructuredArrow F₀ (obj (whiskeringLeft C C H) (𝟭 C))) ↦
        StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) sorry)
      Y
Tactic: refine IsInitial.ofUniqueHom
    (fun y ↦ StructuredArrow.homMk <| α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ?_