awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
L : Functor.{v_1, v_4, u_1, u_4} C D
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
F₁' F₂' : Functor.{v_4, v_3, u_4, u_3} D H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
eq : CostructuredArrow.IsUniversal (RightExtension.mk F₁' α₁) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F₂' α₂) :=
  (RightExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (RightExtension.mk F₂' α₂) e e' h
mp : F₁'.IsRightKanExtension α₁ → F₂'.IsRightKanExtension α₂
⊢ F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂
have mpr : F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁
Tactic: constructor
-- 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 : 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)))
⊢ StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ map (obj (whiskeringLeft C D' H) (L ⋙ L')) (hb.desc u) =
    StructuredArrow.hom y
have w : ∀ (x : C),
  (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: ext x
-- 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'
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
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ map (obj (whiskeringLeft C D' H) (L ⋙ L')) (hb.desc u)).app x =
    (StructuredArrow.hom y).app x
have 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))
Tactic: haveI hb_fac_app := congr_app (hb.fac u) (L.obj x)
-- 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'
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))
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ map (obj (whiskeringLeft C D' H) (L ⋙ L')) (hb.desc u)).app x =
    (StructuredArrow.hom y).app x
have hα_fac_app : 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
-- 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 : 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)))
⊢ Unique ((precomp₂ L' α).obj b ⟶ y)
have ext : ∀ (a : (precomp₂ L' α).obj b ⟶ y), a = default
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 => ?_⟩
-- 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 : 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
⊢ a = StructuredArrow.homMk (hb.desc u) ⋯
have h : StructuredArrow.Hom.right a = StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) sorry)
Tactic: ext1
-- 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 : 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
⊢ StructuredArrow.Hom.right a = StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)
have 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) sorry))
Tactic: apply hb.hom_ext
-- 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 : 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
⊢ 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) ⋯))
have 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) sorry)))
Tactic: apply hα.hom_ext
-- 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 : 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
⊢ 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) ⋯)))
have 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) sorry)))).app
      t
Tactic: ext t
-- 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 : 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 (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
have 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))
Tactic: dsimp
-- 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'
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
⊢ α.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))
have 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
Tactic: have a_w_t := congr_app a.w t
-- 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'
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
⊢ α.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))
have 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))
Tactic: have hb_fac_app := congr_app (hb.fac u) (L.obj t)
-- 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'
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))
⊢ α.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))
have hα_fac_app : 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
-- 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'
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 ≫ (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))
have 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
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
Cleared hypotheses: a_w_t
-- 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 : 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)
⊢ StructuredArrow.hom b ≫ map (obj (whiskeringLeft D D' H) L') (StructuredArrow.Hom.right u) = StructuredArrow.hom y
have 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)
Tactic: apply hα.hom_ext
-- 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 : 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)
⊢ 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)
have 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
Tactic: ext t