awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
x : C
hb_fac_app :
  Eq (α := F₁.obj (L.obj x) ⟶ (obj (obj (whiskeringLeft D D' H) L') (StructuredArrow.right u)).obj (L.obj x))
    ((StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (hb.desc u)).app (L.obj x))
    ((StructuredArrow.hom u).app (L.obj x))
⊢ NatTrans.app
      (StructuredArrow.hom (mk F₁ α) ≫
        map (obj (whiskeringLeft C D H) L)
          (hα.desc
            (mk (L' ⋙ StructuredArrow.right y)
              (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))))
      x =
    (StructuredArrow.hom
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))).app
      x

Tactic:
haveI hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
x : C
hb_fac_app :
  Eq (α := F₁.obj (L.obj x) ⟶ (StructuredArrow.right u).obj (L'.obj (L.obj x)))
    ((StructuredArrow.hom b).app (L.obj x) ≫ (hb.desc u).app (L'.obj (L.obj x))) ((StructuredArrow.hom u).app (L.obj x))
hα_fac_app :
  α.app x ≫
      NatTrans.app
        (hα.desc
          (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
        (L.obj x) =
    (StructuredArrow.hom y).app x ≫ 𝟙 ((StructuredArrow.right y).obj (L'.obj (L.obj x)))
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ map (obj (whiskeringLeft C D' H) (L ⋙ L')) (hb.desc u)).app x =
    (StructuredArrow.hom y).app x

Tactic:
simp [hb_fac_app, u, hα_fac_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'
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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
ext : ∀ (a : (precomp₂ L' α).obj b ⟶ y), a = default
⊢ Unique ((precomp₂ L' α).obj b ⟶ y)

Tactic:
refine
      ⟨⟨StructuredArrow.homMk (hb.desc u) <| by
          ext x
          haveI hb_fac_app := congr_app (hb.fac u) (L.obj x)
          haveI hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x
          dsimp at hα_fac_app hb_fac_app
          simp [hb_fac_app, u, hα_fac_app]⟩, fun a => ?_⟩
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
h : StructuredArrow.Hom.right a = StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)
⊢ a = StructuredArrow.homMk (hb.desc u) ⋯

Tactic:
ext1
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
h :
  StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right a) =
    StructuredArrow.hom b ≫
      map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯))
⊢ StructuredArrow.Hom.right a = StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)

Tactic:
apply hb.hom_ext

Premises used: CategoryTheory.StructuredArrow.IsUniversal.hom_ext
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
h :
  StructuredArrow.hom (mk F₁ α) ≫
      map (obj (whiskeringLeft C D H) L)
        (StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right a)) =
    StructuredArrow.hom (mk F₁ α) ≫
      map (obj (whiskeringLeft C D H) L)
        (StructuredArrow.hom b ≫
          map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)))
⊢ StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right a) =
    StructuredArrow.hom b ≫
      map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯))

Tactic:
apply hα.hom_ext

Premises used: CategoryTheory.StructuredArrow.IsUniversal.hom_ext
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
h :
  ∀ (t : C),
    (StructuredArrow.hom (mk F₁ α) ≫
            map (obj (whiskeringLeft C D H) L)
              (StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right a))).app
        t =
      (StructuredArrow.hom (mk F₁ α) ≫
            map (obj (whiskeringLeft C D H) L)
              (StructuredArrow.hom b ≫
                map (obj (whiskeringLeft D D' H) L')
                  (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)))).app
        t
⊢ StructuredArrow.hom (mk F₁ α) ≫
      map (obj (whiskeringLeft C D H) L)
        (StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right a)) =
    StructuredArrow.hom (mk F₁ α) ≫
      map (obj (whiskeringLeft C D H) L)
        (StructuredArrow.hom b ≫
          map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)))

Tactic:
ext t
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
h :
  α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) =
    α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))
⊢ (StructuredArrow.hom (mk F₁ α) ≫
          map (obj (whiskeringLeft C D H) L)
            (StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right a))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫
          map (obj (whiskeringLeft C D H) L)
            (StructuredArrow.hom b ≫
              map (obj (whiskeringLeft D D' H) L')
                (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)))).app
      t

Tactic:
dsimp
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom y).app t

Tactic:
have a_w_t := congr_app a.w t
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
a_w_t :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom y).app t
⊢ Eq (α := F₁.obj (L.obj t) ⟶ (obj (obj (whiskeringLeft D D' H) L') (StructuredArrow.right u)).obj (L.obj t))
    ((StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (hb.desc u)).app (L.obj t))
    ((StructuredArrow.hom u).app (L.obj t))

Tactic:
have hb_fac_app := congr_app (hb.fac u) (L.obj t)
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
a_w_t :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom y).app t
hb_fac_app :
  Eq (α := F₁.obj (L.obj t) ⟶ (obj (obj (whiskeringLeft D D' H) L') (StructuredArrow.right u)).obj (L.obj t))
    ((StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (hb.desc u)).app (L.obj t))
    ((StructuredArrow.hom u).app (L.obj t))
⊢ NatTrans.app
      (StructuredArrow.hom (mk F₁ α) ≫
        map (obj (whiskeringLeft C D H) L)
          (hα.desc
            (mk (L' ⋙ StructuredArrow.right y)
              (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))))
      t =
    (StructuredArrow.hom
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))).app
      t

Tactic:
have hα_fac_app :=
      congr_app
        (hα.fac <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom) t
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
a_w_t :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom y).app t
hb_fac_app :
  Eq (α := F₁.obj (L.obj t) ⟶ (StructuredArrow.right u).obj (L'.obj (L.obj t)))
    ((StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))) ((StructuredArrow.hom u).app (L.obj t))
hα_fac_app :
  α.app t ≫
      NatTrans.app
        (hα.desc
          (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
        (L.obj t) =
    (StructuredArrow.hom y).app t ≫ 𝟙 ((StructuredArrow.right y).obj (L'.obj (L.obj t)))
⊢ α.app t ≫ b.hom.app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) = (StructuredArrow.hom y).app t

Tactic:
simp only [whiskeringLeft_obj_obj, comp_obj,
      precomp₂_obj_right, whiskeringLeft_obj_map, NatTrans.comp_app,
      precomp₂_obj_hom_app, whiskerLeft_app, assoc] at a_w_t

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.LeftExtension.precomp₂_obj_hom_app, CategoryTheory.Category.assoc, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.whiskeringLeft_obj_map, CategoryTheory.Functor.LeftExtension.precomp₂_obj_right, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.whiskeringLeft_obj_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'
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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
hb_fac_app :
  Eq (α := F₁.obj (L.obj t) ⟶ (StructuredArrow.right u).obj (L'.obj (L.obj t)))
    ((StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))) ((StructuredArrow.hom u).app (L.obj t))
hα_fac_app :
  α.app t ≫
      NatTrans.app
        (hα.desc
          (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
        (L.obj t) =
    (StructuredArrow.hom y).app t ≫ 𝟙 ((StructuredArrow.right y).obj (L'.obj (L.obj t)))
a_w_t :
  α.app t ≫ b.hom.app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) = (StructuredArrow.hom y).app t
⊢ α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) =
    α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))

Tactic:
simp [← a_w_t, hb_fac_app, u, hα_fac_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'
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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
this : (y : (L ⋙ L').LeftExtension F₀) → Unique ((precomp₂ L' α).obj b ⟶ y) :=
  fun (y : (L ⋙ L').LeftExtension F₀) ↦
    let u : L'.LeftExtension F₁ :=
      mk (StructuredArrow.right y)
        (hα.desc
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)));
    { default := StructuredArrow.homMk (hb.desc u) ⋯, uniq := ⋯ }
⊢ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

Tactic:
apply IsInitial.ofUnique

Premises used: CategoryTheory.Limits.IsInitial.ofUnique
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
apply :
  StructuredArrow.hom (mk F₁ α) ≫
      map (obj (whiskeringLeft C D H) L)
        (StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right u)) =
    StructuredArrow.hom (mk F₁ α) ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.hom y)
⊢ StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right u) = StructuredArrow.hom y

Tactic:
apply hα.hom_ext

Premises used: CategoryTheory.StructuredArrow.IsUniversal.hom_ext
-- 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 : 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₂ : Functor.{v_5, v_3, u_5, u_3} D' H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
w :
  ∀ (t : C),
    (StructuredArrow.hom (mk F₁ α) ≫
            map (obj (whiskeringLeft C D H) L)
              (StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right u))).app
        t =
      (StructuredArrow.hom (mk F₁ α) ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.hom y)).app t
⊢ StructuredArrow.hom (mk F₁ α) ≫
      map (obj (whiskeringLeft C D H) L)
        (StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right u)) =
    StructuredArrow.hom (mk F₁ α) ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.hom y)

Tactic:
ext t