awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj 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 u))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.hom y)).app t
have this : (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
        map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right u)).app
    t =
  (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
Tactic: have := congr_app u.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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b)).app t ≫ (StructuredArrow.Hom.right u).app (L'.obj (L.obj t)) =
    (StructuredArrow.hom ((precomp₂ L' α).obj 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))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫ map (obj (whiskeringLeft C D H) L) (StructuredArrow.hom y)).app t
have this₁ : α.app t ≫ b.hom.app (L.obj t) ≫ (StructuredArrow.Hom.right u).app (L'.obj (L.obj t)) = α.app t ≫ y.hom.app (L.obj t)
Tactic: simp only [precomp₂_obj_hom_app, assoc] at this
Cleared hypotheses: this
-- 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)
⊢ Unique (b ⟶ y)
have apply : ∀ (a : b ⟶ y), a = default
Tactic: refine
      ⟨⟨StructuredArrow.homMk u.right <| by
          apply hα.hom_ext
          ext t
          have := congr_app u.w t
          dsimp at this
          simp only [precomp₂_obj_hom_app, assoc] at this
          simp [this]⟩, 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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
⊢ a = default
have h : StructuredArrow.Hom.right a = StructuredArrow.Hom.right default
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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
⊢ StructuredArrow.Hom.right a = StructuredArrow.Hom.right default
have h : StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a) =
  StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
    map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right default)
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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
⊢ StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
      map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a) =
    StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
      map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right default)
have h : ∀ (t : C),
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a)).app
      t =
    NatTrans.app
      (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
        map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right default))
      t
Tactic: ext 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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
t : C
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a)).app
      t =
    NatTrans.app
      (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
        map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right default))
      t
have this : (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
        map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right u)).app
    t =
  (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
Tactic: have := congr_app u.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 ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b)).app t ≫ (StructuredArrow.Hom.right u).app (L'.obj (L.obj t)) =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right a)).app
      t =
    NatTrans.app
      (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
        map (obj (whiskeringLeft C D' H) (L ⋙ L')) (StructuredArrow.Hom.right default))
      t
have this₁ : α.app t ≫ b.hom.app (L.obj t) ≫ (StructuredArrow.Hom.right u).app (L'.obj (L.obj t)) = α.app t ≫ y.hom.app (L.obj t)
Tactic: simp only [precomp₂_obj_hom_app, assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₀
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ
have obtain : ∀ (hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)), F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ
Tactic: obtain ⟨⟨hα⟩⟩ := (inferInstance : F₁.IsLeftKanExtension α)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₁ α)
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ
have refine_1 : F₂.IsLeftKanExtension β →
  (h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)) → StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
Tactic: refine ⟨fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩, fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₁ α)
refine_1 :
  F₂.IsLeftKanExtension β →
    (h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)) → StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ
have refine_2 : F₂.IsLeftKanExtension γ →
  (h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)) → StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
Tactic: refine ⟨fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩, fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₂ β)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
have refine_1 : IsInitial (Ψ.inverse.obj (LeftExtension.mk F₂ γ))
Tactic: apply IsInitial.isInitialIffObj Ψ.inverse _ |>.invFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
⊢ StructuredArrow.hom ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)) ≫
      map (obj (whiskeringLeft C D' H) (L ⋙ L'))
        (Iso.hom
          (NatIso.ofComponents
            (fun (x : D') ↦
              Iso.refl ((StructuredArrow.right ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))).obj x))
            ⋯)) =
    StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))
have w : ∀ (x : C),
  NatTrans.app
      (StructuredArrow.hom ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)) ≫
        map (obj (whiskeringLeft C D' H) (L ⋙ L'))
          (Iso.hom
            (NatIso.ofComponents
              (fun (x : D') ↦
                Iso.refl ((StructuredArrow.right ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))).obj x))
              sorry)))
      x =
    (StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))).app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₂ γ)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
have refine_2 : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
Tactic: apply LeftExtension.isUniversalOfPrecomp₂ α hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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₂ γ)
⊢ StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
have refine_2 : IsInitial (Ψ.functor.obj ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)))
Tactic: apply IsInitial.isInitialIffObj Ψ.functor _ |>.invFun
-- 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
α : F ⟶ L ⋙ F'
inst_5 : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
⊢ ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι } = s.ι.app j
have this : 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)
-- 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
α : 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
⊢ c.ι.app j ≫ m = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }
have this : 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)
-- 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) ((F'.coconeOfIsLeftKanExtension α c).ι.app (L.obj j) ≫ m) (s.ι.app (L.obj j))
⊢ c.ι.app j ≫ m = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }
have 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)
Tactic: nth_rw 1 [← F'.descOfIsLeftKanExtension_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
α : 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))
⊢ 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 : 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]