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
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) :=
  Equiv.trans (LeftExtension.isUniversalPrecompEquiv L F G (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.precomp L F G).obj (LeftExtension.mk F' α)))) ⋯))
⊢ F'.IsLeftKanExtension α → F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)

Tactic:
exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) :=
  Equiv.trans (LeftExtension.isUniversalPrecompEquiv L F G (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.precomp L F G).obj (LeftExtension.mk F' α)))) ⋯))
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α

Tactic:
fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩

Premises used: CategoryTheory.Functor.associator, CategoryTheory.Functor.whiskerLeft, Nonempty.intro, CategoryTheory.CategoryStruct.comp, Equiv.symm, CategoryTheory.Functor.IsLeftKanExtension.mk, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Functor.isUniversalOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) :=
  Equiv.trans (LeftExtension.isUniversalPrecompEquiv L F G (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.precomp L F G).obj (LeftExtension.mk F' α)))) ⋯))
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α

Tactic:
exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) :=
  Equiv.trans (RightExtension.isUniversalPrecompEquiv L F G (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.precomp L F G).obj (RightExtension.mk F' α)))) ⋯))
mp : F'.IsRightKanExtension α → F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)
mpr : F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α) → F'.IsRightKanExtension α
⊢ F'.IsRightKanExtension α ↔ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) :=
  Equiv.trans (RightExtension.isUniversalPrecompEquiv L F G (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.precomp L F G).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension α → F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)

Tactic:
fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩

Premises used: CategoryTheory.Functor.isUniversalOfIsRightKanExtension, Nonempty.intro, CategoryTheory.Functor.IsRightKanExtension.mk, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) :=
  Equiv.trans (RightExtension.isUniversalPrecompEquiv L F G (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.precomp L F G).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension α → F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)

Tactic:
exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) :=
  Equiv.trans (RightExtension.isUniversalPrecompEquiv L F G (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.precomp L F G).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α) → F'.IsRightKanExtension α

Tactic:
fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩

Premises used: CategoryTheory.Functor.isUniversalOfIsRightKanExtension, CategoryTheory.Functor.associator, CategoryTheory.Functor.whiskerLeft, Nonempty.intro, CategoryTheory.CategoryStruct.comp, Equiv.symm, CategoryTheory.Functor.IsRightKanExtension.mk, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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
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' : Functor.{v_4, v_3, u_4, u_3} D H
G : Functor.{v_2, v_1, u_2, u_1} C' C
inst_4 : G.IsEquivalence
α : L ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F' ((G.associator L F').hom ≫ G.whiskerLeft α)) :=
  Equiv.trans (RightExtension.isUniversalPrecompEquiv L F G (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.precomp L F G).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α) → F'.IsRightKanExtension α

Tactic:
exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
L L' : Functor.{v_1, v_4, u_1, u_4} C D
iso₁ : L ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ L.HasRightKanExtension F ↔ L'.HasRightKanExtension F

Tactic:
(rightExtensionEquivalenceOfIso₁ iso₁ F).hasTerminal_iff

Premises used: CategoryTheory.Equivalence.hasTerminal_iff, CategoryTheory.Functor.rightExtensionEquivalenceOfIso₁
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
L L' : Functor.{v_1, v_4, u_1, u_4} C D
iso₁ : L ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ L.HasLeftKanExtension F ↔ L'.HasLeftKanExtension F

Tactic:
(leftExtensionEquivalenceOfIso₁ iso₁ F).hasInitial_iff

Premises used: CategoryTheory.Equivalence.hasInitial_iff, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
iso₂ : F ≅ F'
⊢ L.HasRightKanExtension F ↔ L.HasRightKanExtension F'

Tactic:
(rightExtensionEquivalenceOfIso₂ L iso₂).hasTerminal_iff

Premises used: CategoryTheory.Equivalence.hasTerminal_iff, CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
iso₂ : F ≅ F'
⊢ L.HasLeftKanExtension F ↔ L.HasLeftKanExtension F'

Tactic:
(leftExtensionEquivalenceOfIso₂ L iso₂).hasInitial_iff

Premises used: CategoryTheory.Equivalence.hasInitial_iff, CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂
-- 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
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
α₁ : L.LeftExtension F₁
α₂ : L.LeftExtension F₂
e : F₁ ≅ F₂
e' : StructuredArrow.right α₁ ≅ StructuredArrow.right α₂
h : StructuredArrow.hom α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ StructuredArrow.hom α₂
⊢ StructuredArrow.hom ((L.leftExtensionEquivalenceOfIso₂ e).functor.obj α₁) ≫
      map (obj (whiskeringLeft C D H) L) e'.hom =
    StructuredArrow.hom α₂

Tactic:
simp [leftExtensionEquivalenceOfIso₂, h]

Premises used: CategoryTheory.Functor.leftExtensionEquivalenceOfIso₂
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
mp : F₁'.IsLeftKanExtension α₁ → F₂'.IsLeftKanExtension α₂
mpr : F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁
⊢ F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ F₁'.IsLeftKanExtension α₁ → F₂'.IsLeftKanExtension α₂

Tactic:
fun _ => ⟨⟨eq.1 (isUniversalOfIsLeftKanExtension F₁' α₁)⟩⟩

Premises used: Equiv.toFun, Nonempty.intro, CategoryTheory.Functor.IsLeftKanExtension.mk, CategoryTheory.Functor.isUniversalOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ F₁'.IsLeftKanExtension α₁ → F₂'.IsLeftKanExtension α₂

Tactic:
exact fun _ => ⟨⟨eq.1 (isUniversalOfIsLeftKanExtension F₁' α₁)⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁

Tactic:
fun _ => ⟨⟨eq.2 (isUniversalOfIsLeftKanExtension F₂' α₂)⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.IsLeftKanExtension.mk, Equiv.invFun, CategoryTheory.Functor.isUniversalOfIsLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ L.whiskerLeft e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁

Tactic:
exact fun _ => ⟨⟨eq.2 (isUniversalOfIsLeftKanExtension F₂' α₂)⟩⟩
-- 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
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
α₁ : L.RightExtension F₁
α₂ : L.RightExtension F₂
e : F₁ ≅ F₂
e' : CostructuredArrow.left α₁ ≅ CostructuredArrow.left α₂
h : L.whiskerLeft e'.hom ≫ CostructuredArrow.hom α₂ = CostructuredArrow.hom α₁ ≫ e.hom
⊢ map (obj (whiskeringLeft C D H) L) e'.hom ≫ CostructuredArrow.hom α₂ =
    CostructuredArrow.hom ((L.rightExtensionEquivalenceOfIso₂ e).functor.obj α₁)

Tactic:
simp [rightExtensionEquivalenceOfIso₂, h]

Premises used: CategoryTheory.Functor.rightExtensionEquivalenceOfIso₂
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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 α₂
mpr : F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁
⊢ F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
⊢ F₁'.IsRightKanExtension α₁ → F₂'.IsRightKanExtension α₂

Tactic:
fun _ => ⟨⟨eq.1 (isUniversalOfIsRightKanExtension F₁' α₁)⟩⟩

Premises used: CategoryTheory.Functor.isUniversalOfIsRightKanExtension, Equiv.toFun, Nonempty.intro, CategoryTheory.Functor.IsRightKanExtension.mk
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
⊢ F₁'.IsRightKanExtension α₁ → F₂'.IsRightKanExtension α₂

Tactic:
exact fun _ => ⟨⟨eq.1 (isUniversalOfIsRightKanExtension F₁' α₁)⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
⊢ F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁

Tactic:
fun _ => ⟨⟨eq.2 (isUniversalOfIsRightKanExtension F₂' α₂)⟩⟩

Premises used: CategoryTheory.Functor.isUniversalOfIsRightKanExtension, Nonempty.intro, CategoryTheory.Functor.IsRightKanExtension.mk, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
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
⊢ F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁

Tactic:
exact fun _ => ⟨⟨eq.2 (isUniversalOfIsRightKanExtension F₂' α₂)⟩⟩
-- 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)))
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
⊢ StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ map (obj (whiskeringLeft C D' H) (L ⋙ L')) (hb.desc u) =
    StructuredArrow.hom y

Tactic:
ext 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
⊢ 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)