awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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_3 : F'.IsLeftKanExtension α
⊢ L.HasLeftKanExtension F

Tactic:
(F'.isUniversalOfIsLeftKanExtension α).hasInitial

Premises used: CategoryTheory.Limits.IsInitial.hasInitial, 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 : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasRightKanExtension F
G : Functor.{v_4, v_3, u_4, u_3} D H
γ₁ γ₂ : G ⟶ L.rightKanExtension F
hγ : L.whiskerLeft γ₁ ≫ L.rightKanExtensionCounit F = L.whiskerLeft γ₂ ≫ L.rightKanExtensionCounit F
⊢ γ₁ = γ₂

Tactic:
hom_ext_of_isRightKanExtension _ _ _ _ hγ

Premises used: CategoryTheory.Functor.hom_ext_of_isRightKanExtension
-- 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 : Functor.{v_1, v_3, u_1, u_3} C H
inst_3 : L.HasLeftKanExtension F
G : Functor.{v_4, v_3, u_4, u_3} D H
γ₁ γ₂ : L.leftKanExtension F ⟶ G
hγ : L.leftKanExtensionUnit F ≫ L.whiskerLeft γ₁ = L.leftKanExtensionUnit F ≫ L.whiskerLeft γ₂
⊢ γ₁ = γ₂

Tactic:
hom_ext_of_isLeftKanExtension _ _ _ _ hγ

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_5 : G.IsEquivalence
f : L' ⟶ L ⋙ G
inst_6 : IsIso f
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ (LeftExtension.postcomp₁ G f F).IsEquivalence

Tactic:
apply StructuredArrow.isEquivalenceMap₂

Premises used: CategoryTheory.StructuredArrow.isEquivalenceMap₂
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_5 : G.IsEquivalence
f : L ⋙ G ⟶ L'
inst_6 : IsIso f
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ (RightExtension.postcomp₁ G f F).IsEquivalence

Tactic:
apply CostructuredArrow.isEquivalenceMap₂

Premises used: CategoryTheory.CostructuredArrow.isEquivalenceMap₂
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ L'.HasLeftKanExtension F ↔ L.HasLeftKanExtension F

Tactic:
(LeftExtension.postcomp₁ G e.inv F).asEquivalence.hasInitial_iff

Premises used: CategoryTheory.Equivalence.hasInitial_iff, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.LeftExtension.postcomp₁, CategoryTheory.Iso.inv
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ L'.HasRightKanExtension F ↔ L.HasRightKanExtension F

Tactic:
(RightExtension.postcomp₁ G e.hom F).asEquivalence.hasTerminal_iff

Premises used: CategoryTheory.Equivalence.hasTerminal_iff, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.RightExtension.postcomp₁, CategoryTheory.Iso.hom
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_5 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
ex : L'.LeftExtension F
⊢ StructuredArrow.IsUniversal ex ≃ StructuredArrow.IsUniversal ((postcomp₁ G e.inv F).obj ex)

Tactic:
apply IsInitial.isInitialIffObj (LeftExtension.postcomp₁ G e.inv F)

Premises used: CategoryTheory.Functor.LeftExtension.postcomp₁, CategoryTheory.Limits.IsInitial.isInitialIffObj, CategoryTheory.Iso.inv
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_5 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
ex : L'.RightExtension F
⊢ CostructuredArrow.IsUniversal ex ≃ CostructuredArrow.IsUniversal ((postcomp₁ G e.hom F).obj ex)

Tactic:
apply IsTerminal.isTerminalIffObj (RightExtension.postcomp₁ G e.hom F)

Premises used: CategoryTheory.Limits.IsTerminal.isTerminalIffObj, CategoryTheory.Functor.RightExtension.postcomp₁, CategoryTheory.Iso.hom
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) :=
  Equiv.trans (LeftExtension.isUniversalPostcomp₁Equiv G e F (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.postcomp₁ G e.inv F).obj (LeftExtension.mk F' α)))) ⋯))
mp : F'.IsLeftKanExtension α → (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)
mpr : (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α
⊢ F'.IsLeftKanExtension α ↔ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)

Tactic:
constructor
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) :=
  Equiv.trans (LeftExtension.isUniversalPostcomp₁Equiv G e F (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.postcomp₁ G e.inv F).obj (LeftExtension.mk F' α)))) ⋯))
⊢ F'.IsLeftKanExtension α → (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)

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

Premises used: Nonempty.intro, CategoryTheory.Functor.IsLeftKanExtension.mk, DFunLike.coe, CategoryTheory.Functor.isUniversalOfIsLeftKanExtension
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) :=
  Equiv.trans (LeftExtension.isUniversalPostcomp₁Equiv G e F (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.postcomp₁ G e.inv F).obj (LeftExtension.mk F' α)))) ⋯))
⊢ F'.IsLeftKanExtension α → (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)

Tactic:
exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) :=
  Equiv.trans (LeftExtension.isUniversalPostcomp₁Equiv G e F (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.postcomp₁ G e.inv F).obj (LeftExtension.mk F' α)))) ⋯))
⊢ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α

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

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, Nonempty.intro, CategoryTheory.Functor.whiskerRight, CategoryTheory.CategoryStruct.comp, Equiv.symm, CategoryTheory.Functor.IsLeftKanExtension.mk, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Functor.isUniversalOfIsLeftKanExtension
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) :=
  Equiv.trans (LeftExtension.isUniversalPostcomp₁Equiv G e F (LeftExtension.mk F' α))
    (IsInitial.equivOfIso
      (StructuredArrow.isoMk
        (Iso.refl (StructuredArrow.right ((LeftExtension.postcomp₁ G e.inv F).obj (LeftExtension.mk F' α)))) ⋯))
⊢ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α

Tactic:
exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  Equiv.trans (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)))) ⋯))
mp : F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)
mpr : (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Tactic:
constructor
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  Equiv.trans (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

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
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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  Equiv.trans (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)))) ⋯))
⊢ F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Tactic:
exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  Equiv.trans (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)))) ⋯))
⊢ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α

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

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.isUniversalOfIsRightKanExtension, CategoryTheory.Functor.associator, Nonempty.intro, CategoryTheory.Functor.whiskerRight, CategoryTheory.CategoryStruct.comp, Equiv.symm, CategoryTheory.Functor.IsRightKanExtension.mk, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- 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_1, v_5, u_1, u_5} C D'
G : Functor.{v_4, v_5, u_4, u_5} D D'
inst_4 : G.IsEquivalence
e : L ⋙ G ≅ L'
F : Functor.{v_1, v_3, u_1, u_3} C H
F' : Functor.{v_5, v_3, u_5, u_3} D' H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  Equiv.trans (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α))
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk
        (Iso.refl (CostructuredArrow.left ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)))) ⋯))
⊢ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α

Tactic:
exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩
-- 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 : 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_5 : G.IsEquivalence
⊢ (LeftExtension.precomp L F G).IsEquivalence

Tactic:
apply StructuredArrow.isEquivalenceMap₂

Premises used: CategoryTheory.StructuredArrow.isEquivalenceMap₂
-- 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 : 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_5 : G.IsEquivalence
⊢ (RightExtension.precomp L F G).IsEquivalence

Tactic:
apply CostructuredArrow.isEquivalenceMap₂

Premises used: CategoryTheory.CostructuredArrow.isEquivalenceMap₂
-- 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 : 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_5 : G.IsEquivalence
e : L.LeftExtension F
⊢ StructuredArrow.IsUniversal e ≃ StructuredArrow.IsUniversal ((precomp L F G).obj e)

Tactic:
apply IsInitial.isInitialIffObj (LeftExtension.precomp L F G)

Premises used: CategoryTheory.Functor.LeftExtension.precomp, CategoryTheory.Limits.IsInitial.isInitialIffObj
-- 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 : 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_5 : G.IsEquivalence
e : L.RightExtension F
⊢ CostructuredArrow.IsUniversal e ≃ CostructuredArrow.IsUniversal ((precomp L F G).obj e)

Tactic:
apply IsTerminal.isTerminalIffObj (RightExtension.precomp L F G)

Premises used: CategoryTheory.Limits.IsTerminal.isTerminalIffObj, CategoryTheory.Functor.RightExtension.precomp
-- 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' α)))) ⋯))
mp : F'.IsLeftKanExtension α → F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)
mpr : F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α
⊢ F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)

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
α : 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:
fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.IsLeftKanExtension.mk, DFunLike.coe, CategoryTheory.Functor.isUniversalOfIsLeftKanExtension