awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
inst_3 : Category.{v_5, u_5} D'
L : Functor.{v_1, v_4, u_1, u_4} C D
L' : Functor.{v_4, v_5, u_4, u_5} D 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 ⋙ F₁
inst_4 : F₁.IsLeftKanExtension α
F₂ : Functor.{v_5, v_3, u_5, u_3} D' H
L'' : Functor.{v_1, v_5, u_1, u_5} C D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
h_1 : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
refine_2 : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)

Tactic:
apply LeftExtension.isUniversalOfPrecomp₂ α hα

Premises used: CategoryTheory.Functor.LeftExtension.isUniversalOfPrecomp₂
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
inst_3 : Category.{v_5, u_5} D'
L : Functor.{v_1, v_4, u_1, u_4} C D
L' : Functor.{v_4, v_5, u_4, u_5} D 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 ⋙ F₁
inst_4 : F₁.IsLeftKanExtension α
F₂ : Functor.{v_5, v_3, u_5, u_3} D' H
L'' : Functor.{v_1, v_5, u_1, u_5} C D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
h_1 : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
refine_2 : IsInitial (Ψ.functor.obj ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)))
⊢ StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))

Tactic:
apply IsInitial.isInitialIffObj Ψ.functor _ |>.invFun

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Limits.IsInitial.isInitialIffObj, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
inst_3 : Category.{v_5, u_5} D'
L : Functor.{v_1, v_4, u_1, u_4} C D
L' : Functor.{v_4, v_5, u_4, u_5} D 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 ⋙ F₁
inst_4 : F₁.IsLeftKanExtension α
F₂ : Functor.{v_5, v_3, u_5, u_3} D' H
L'' : Functor.{v_1, v_5, u_1, u_5} C D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
h_1 : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
i : LeftExtension.mk F₂ γ ≅ Ψ.functor.obj ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)) :=
  StructuredArrow.isoMk
    (NatIso.ofComponents (fun (x : D') ↦ Iso.refl ((StructuredArrow.right (LeftExtension.mk F₂ γ)).obj x)) ⋯) ⋯
⊢ IsInitial (Ψ.functor.obj ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)))

Tactic:
exact IsInitial.ofIso h i

Premises used: CategoryTheory.Limits.IsInitial.ofIso
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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'
⊢ F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι ≫
      map (const D) (hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι : Cocone F }) =
    s.ι

Tactic:
have : F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
        (Functor.const _).map (hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))) = s.ι :=
      F'.hom_ext_of_isLeftKanExtension α _ _ (by cat_disch)
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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'
this :
  F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι ≫
      map (const D) (hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι : Cocone F }) =
    s.ι
⊢ ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } = s.ι.app j

Tactic:
congr_app this

Premises used: CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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'
this :
  F'.descOfIsLeftKanExtension α (obj (const D) c.pt) c.ι ≫
      map (const D) (hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι : Cocone F }) =
    s.ι
⊢ ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } = s.ι.app j

Tactic:
exact congr_app this

Premises used: CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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
⊢ Eq (α := F'.obj (L.obj j) ⟶ s.pt) ((F'.coconeOfIsLeftKanExtension α c).ι.app (L.obj j) ≫ m) (s.ι.app (L.obj j))

Tactic:
have := hm (L.obj j)
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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) ((F'.coconeOfIsLeftKanExtension α c).ι.app (L.obj j) ≫ m) (s.ι.app (L.obj j))
nth_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)
⊢ c.ι.app j ≫ m = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }

Tactic:
nth_rw 1 [← F'.descOfIsLeftKanExtension_fac_app α ((const D).obj c.pt)]

Premises used: CategoryTheory.Functor.const, CategoryTheory.Functor.descOfIsLeftKanExtension_fac_app, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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) ((F'.coconeOfIsLeftKanExtension α c).ι.app (L.obj j) ≫ m) (s.ι.app (L.obj j))
dsimp :
  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)

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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
rw₄ rw₅ : α.app j ≫ s.ι.app (L.obj j) = α.app j ≫ s.ι.app (L.obj 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)

Tactic:
rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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)
    (α.app i ≫
      CategoryStruct.comp (Y := colimit F') (colimit.ι F' (L.obj i)) (Iso.hom (F'.colimitIsoOfIsLeftKanExtension α)))
    (colimit.ι F i)

Tactic:
simp [colimitIsoOfIsLeftKanExtension]

Premises used: CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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 α)))
rw₂ rw₃ : Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i) (colimit.ι F i)
⊢ 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))

Tactic:
rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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'
⊢ 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)
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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'
this :
  map (const D) (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α : Cone F }) ≫
      F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π =
    s.π
⊢ ∀ (j : D), hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j

Tactic:
congr_app this

Premises used: CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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'
this :
  map (const D) (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α : Cone F }) ≫
      F'.liftOfIsRightKanExtension α (obj (const D) c.pt) c.π =
    s.π
⊢ ∀ (j : D), hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j

Tactic:
exact congr_app this

Premises used: CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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
⊢ 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)
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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))
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)
⊢ m ≫ c.π.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)]

Premises used: CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app, CategoryTheory.Limits.Cone.pt, CategoryTheory.Functor.const, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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))
dsimp :
  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)
⊢ 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:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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
rw₄ rw₅ : s.π.app (L.obj j) ≫ α.app j = s.π.app (L.obj 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)

Tactic:
rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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.inv (F'.limitIsoOfIsRightKanExtension α))
      (limit.π F' (L.obj i) ≫ α.app i))
    (limit.π F i)

Tactic:
simp [limitIsoOfIsRightKanExtension]

Premises used: CategoryTheory.Functor.limitIsoOfIsRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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))
rw₁ rw₂ : Eq (α := limit F ⟶ F.obj i) (limit.π F i) (limit.π F 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)

Tactic:
rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]

Premises used: CategoryTheory.Iso.eq_inv_comp, CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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

Tactic:
⟨⟨?_⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.IsLeftKanExtension.mk
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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₁
refine : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α.hom)
⊢ F₁.IsLeftKanExtension α.hom

Tactic:
refine ⟨⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
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₁
apply :
  StructuredArrow.IsUniversal
    ((LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom))
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₁ α.hom)

Tactic:
apply LeftExtension.isUniversalPostcomp₁Equiv
    (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.leftUnitor, CategoryTheory.Functor.LeftExtension.isUniversalPostcomp₁Equiv, Equiv.invFun