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 ((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 ((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
-- 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)
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
⊢ α.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

Premises used: CategoryTheory.Functor.LeftExtension.precomp₂_obj_hom_app, CategoryTheory.Category.assoc
-- 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)
t : C
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)
⊢ (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:
simp [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'
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 : ∀ (a : b ⟶ y), a = default
⊢ Unique (b ⟶ y)

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 => ?_⟩
-- 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)
a : b ⟶ y
h : StructuredArrow.Hom.right a = StructuredArrow.Hom.right default
⊢ a = default

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 ((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
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)
⊢ StructuredArrow.Hom.right a = StructuredArrow.Hom.right default

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 ((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
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
⊢ 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:
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 ((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 u)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t

Tactic:
have := congr_app u.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 ((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
⊢ α.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

Premises used: CategoryTheory.Functor.LeftExtension.precomp₂_obj_hom_app, CategoryTheory.Category.assoc
-- 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)
a : b ⟶ y
t : C
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)
⊢ (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:
simp [this, ← a.w]

Premises used: CategoryTheory.StructuredArrow.Hom.w
-- 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)
this : (y : L'.LeftExtension F₁) → Unique (b ⟶ y) :=
  fun (y : L'.LeftExtension F₁) ↦
    let u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y);
    { default := StructuredArrow.homMk (StructuredArrow.Hom.right u) ⋯, uniq := ⋯ }
⊢ StructuredArrow.IsUniversal 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₁
x : StructuredArrow.IsUniversal b
⊢ (fun (h : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)) ↦ isUniversalOfPrecomp₂ α hα h)
      ((fun (h : StructuredArrow.IsUniversal b) ↦ isUniversalPrecomp₂ α hα h) x) =
    x

Tactic:
subsingleton
-- 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₁
x : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
⊢ (fun (h : StructuredArrow.IsUniversal b) ↦ isUniversalPrecomp₂ α hα h)
      ((fun (h : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)) ↦ isUniversalOfPrecomp₂ α hα h) x) =
    x

Tactic:
subsingleton
-- 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₀
obtain : ∀ (hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)), F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ

Tactic:
obtain ⟨⟨hα⟩⟩ := (inferInstance : F₁.IsLeftKanExtension α)

Premises used: inferInstance
-- 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₁ α)
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ

Tactic:
⟨fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩, fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩⟩

Premises used: CategoryTheory.Functor.IsLeftKanExtension, Nonempty.intro, _private.0.CategoryTheory.Functor.isLeftKanExtension_iff_postcompose.match_2, Iff.intro, _private.0.CategoryTheory.Functor.isLeftKanExtension_iff_postcompose.match_1, CategoryTheory.Functor.IsLeftKanExtension.mk
-- 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₁ α)
refine_1 :
  F₂.IsLeftKanExtension β →
    (h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)) → StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
refine_2 :
  F₂.IsLeftKanExtension γ →
    (h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)) → StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
⊢ F₂.IsLeftKanExtension β ↔ F₂.IsLeftKanExtension γ

Tactic:
refine ⟨fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩, fun ⟨⟨h⟩⟩ => ⟨⟨?_⟩⟩⟩
-- 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_1 : IsInitial (Ψ.inverse.obj (LeftExtension.mk F₂ γ))
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)

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

Premises used: CategoryTheory.Limits.IsInitial.isInitialIffObj, Equiv.invFun, CategoryTheory.Equivalence.inverse
-- 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₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
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))
                ⋯)))
        x =
      (StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))).app x
⊢ 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₂ γ))

Tactic:
ext x
-- 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₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
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))
              ⋯)))
      x =
    (StructuredArrow.hom (Ψ.inverse.obj (LeftExtension.mk F₂ γ))).app x

Tactic:
simp [Ψ, ← congr_app hγ x, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.congr_app
-- 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₂ β)
this : StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))
i : (LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β) ≅ Ψ.inverse.obj (LeftExtension.mk F₂ γ) :=
  StructuredArrow.isoMk
    (NatIso.ofComponents
      (fun (x : D') ↦
        Iso.refl ((StructuredArrow.right ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))).obj x))
      ⋯)
    ⋯
⊢ IsInitial (Ψ.inverse.obj (LeftExtension.mk F₂ γ))

Tactic:
exact IsInitial.ofIso this i

Premises used: CategoryTheory.Limits.IsInitial.ofIso