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
α : L ⋙ F' ⟶ F
inst_3 : F'.IsRightKanExtension α
G : Functor.{v_4, v_3, u_4, u_3} D H
β : L ⋙ G ⟶ F
⊢ L.whiskerLeft (F'.liftOfIsRightKanExtension α G β) ≫ α = β

Tactic:
(F'.isUniversalOfIsRightKanExtension α).fac (RightExtension.mk G β)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.isUniversalOfIsRightKanExtension, CategoryTheory.Functor.whiskerLeft, CategoryTheory.CostructuredArrow.IsUniversal.fac, CategoryTheory.Functor.RightExtension.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
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
α : L ⋙ F' ⟶ F
inst_3 : F'.IsRightKanExtension α
G : Functor.{v_4, v_3, u_4, u_3} D H
β : L ⋙ G ⟶ F
X : C
⊢ (F'.liftOfIsRightKanExtension α G β).app (L.obj X) ≫ α.app X = β.app X

Tactic:
NatTrans.congr_app (F'.liftOfIsRightKanExtension_fac α G β) X

Premises used: CategoryTheory.Functor.liftOfIsRightKanExtension_fac, CategoryTheory.NatTrans.congr_app
-- 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
α : L ⋙ F' ⟶ F
inst_3 : F'.IsRightKanExtension α
G : Functor.{v_4, v_3, u_4, u_3} D H
γ₁ γ₂ : G ⟶ F'
hγ : L.whiskerLeft γ₁ ≫ α = L.whiskerLeft γ₂ ≫ α
⊢ γ₁ = γ₂

Tactic:
(F'.isUniversalOfIsRightKanExtension α).hom_ext hγ

Premises used: CategoryTheory.Functor.isUniversalOfIsRightKanExtension, CategoryTheory.CostructuredArrow.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'
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
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
G : Functor.{v_4, v_3, u_4, u_3} D H
β : G ⟶ F'
⊢ L.whiskerLeft
        ((fun (β : L ⋙ G ⟶ F) ↦ F'.liftOfIsRightKanExtension α G β) ((fun (β : G ⟶ F') ↦ L.whiskerLeft β ≫ α) β)) ≫
      α =
    L.whiskerLeft β ≫ α

Tactic:
simp
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
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
F' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
h : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α'

Tactic:
isRightKanExtension_of_iso e α α' comm

Premises used: CategoryTheory.Functor.isRightKanExtension_of_iso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
h : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α'

Tactic:
exact isRightKanExtension_of_iso e α α' comm

Premises used: CategoryTheory.Functor.isRightKanExtension_of_iso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
h : F''.IsRightKanExtension α'
⊢ F'.IsRightKanExtension α

Tactic:
isRightKanExtension_of_iso e.symm α' α ?_

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.isRightKanExtension_of_iso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
h : F''.IsRightKanExtension α'
mpr : L.whiskerLeft e.symm.hom ≫ α = α'
⊢ F'.IsRightKanExtension α

Tactic:
refine isRightKanExtension_of_iso e.symm α' α ?_

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.isRightKanExtension_of_iso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
h : F''.IsRightKanExtension α'
mpr : L.whiskerLeft e.symm.hom ≫ L.whiskerLeft e.hom ≫ α' = α'
mpr₁ : L.whiskerLeft (e.symm.hom ≫ e.hom) ≫ α' = α'
mpr₂ : L.whiskerLeft (e.inv ≫ e.hom) ≫ α' = α'
mpr₃ : L.whiskerLeft (𝟙 F'') ≫ α' = α'
mpr₄ : 𝟙 (L ⋙ F'') ≫ α' = α'
mpr₅ mpr₆ : α' = α'
⊢ L.whiskerLeft e.symm.hom ≫ α = α'

Tactic:
rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Iso.symm_hom, CategoryTheory.Functor.whiskerLeft_comp_assoc, CategoryTheory.Functor.whiskerLeft_id', CategoryTheory.Category.id_comp
-- 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'
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
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
G : Functor.{v_1, v_3, u_1, u_3} C H
i : F ≅ G
G' : Functor.{v_4, v_3, u_4, u_3} D H
β : L ⋙ G' ⟶ G
inst_6 : G'.IsRightKanExtension β
⊢ L.whiskerLeft (G'.liftOfIsRightKanExtension β F' (α ≫ i.hom) ≫ F'.liftOfIsRightKanExtension α G' (β ≫ i.inv)) ≫ α =
    L.whiskerLeft (𝟙 F') ≫ α

Tactic:
simp
-- 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'
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
α : L ⋙ F' ⟶ F
inst_5 : F'.IsRightKanExtension α
G : Functor.{v_1, v_3, u_1, u_3} C H
i : F ≅ G
G' : Functor.{v_4, v_3, u_4, u_3} D H
β : L ⋙ G' ⟶ G
inst_6 : G'.IsRightKanExtension β
⊢ L.whiskerLeft (F'.liftOfIsRightKanExtension α G' (β ≫ i.inv) ≫ G'.liftOfIsRightKanExtension β F' (α ≫ i.hom)) ≫ β =
    L.whiskerLeft (𝟙 G') ≫ β

Tactic:
simp
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F'' ⟶ F'
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst_3 : F'.IsRightKanExtension α
mp : F''.IsRightKanExtension α' → IsIso φ
mpr : IsIso φ → F''.IsRightKanExtension α'
⊢ F''.IsRightKanExtension α' ↔ IsIso φ

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
F' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F'' ⟶ F'
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst_3 : F'.IsRightKanExtension α
h : F''.IsRightKanExtension α'
⊢ L.whiskerLeft φ ≫ α = L.whiskerLeft (F''.rightKanExtensionUnique α' F' α).hom ≫ α

Tactic:
simp [comm]
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F'' ⟶ F'
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst_3 : F'.IsRightKanExtension α
h : F''.IsRightKanExtension α'
mp : IsIso (F''.rightKanExtensionUnique α' F' α).hom
⊢ IsIso φ

Tactic:
rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom
      (by simp [comm])]

Premises used: CategoryTheory.Functor.hom_ext_of_isRightKanExtension, CategoryTheory.Functor.rightKanExtensionUnique, CategoryTheory.Iso.hom
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F'' ⟶ F'
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst_3 : F'.IsRightKanExtension α
h : F''.IsRightKanExtension α'
⊢ IsIso (F''.rightKanExtensionUnique α' F' α).hom

Tactic:
infer_instance
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F'' ⟶ F'
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst_3 : F'.IsRightKanExtension α
h : IsIso φ
mpr : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α'

Tactic:
rw [isRightKanExtension_iff_of_iso (asIso φ) α' α comm]

Premises used: CategoryTheory.Functor.isRightKanExtension_iff_of_iso, CategoryTheory.asIso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F'' ⟶ F'
L : Functor.{v_1, v_4, u_1, u_4} C D
F : Functor.{v_1, v_3, u_1, u_3} C H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst_3 : F'.IsRightKanExtension α
h : IsIso φ
⊢ F'.IsRightKanExtension α

Tactic:
infer_instance
-- 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 α
G : Functor.{v_4, v_3, u_4, u_3} D H
β : F ⟶ L ⋙ G
⊢ α ≫ L.whiskerLeft (F'.descOfIsLeftKanExtension α G β) = β

Tactic:
(F'.isUniversalOfIsLeftKanExtension α).fac (LeftExtension.mk G β)

Premises used: CategoryTheory.Functor.LeftExtension.mk, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.StructuredArrow.IsUniversal.fac, 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
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 α
G : Functor.{v_4, v_3, u_4, u_3} D H
β : F ⟶ L ⋙ G
X : C
⊢ α.app X ≫ (F'.descOfIsLeftKanExtension α G β).app (L.obj X) = β.app X

Tactic:
NatTrans.congr_app (F'.descOfIsLeftKanExtension_fac α G β) X

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.descOfIsLeftKanExtension_fac
-- 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 α
G : Functor.{v_4, v_3, u_4, u_3} D H
γ₁ γ₂ : F' ⟶ G
hγ : α ≫ L.whiskerLeft γ₁ = α ≫ L.whiskerLeft γ₂
⊢ γ₁ = γ₂

Tactic:
(F'.isUniversalOfIsLeftKanExtension α).hom_ext hγ

Premises used: CategoryTheory.StructuredArrow.IsUniversal.hom_ext, 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
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 α
G : Functor.{v_4, v_3, u_4, u_3} D H
β : F' ⟶ G
⊢ α ≫
      L.whiskerLeft
        ((fun (β : F ⟶ L ⋙ G) ↦ F'.descOfIsLeftKanExtension α G β) ((fun (β : F' ⟶ G) ↦ α ≫ L.whiskerLeft β) β)) =
    α ≫ L.whiskerLeft β

Tactic:
simp
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
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
F' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
h : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α'

Tactic:
isLeftKanExtension_of_iso e α α' comm

Premises used: CategoryTheory.Functor.isLeftKanExtension_of_iso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
h : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α'

Tactic:
exact isLeftKanExtension_of_iso e α α' comm

Premises used: CategoryTheory.Functor.isLeftKanExtension_of_iso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
h : F''.IsLeftKanExtension α'
⊢ F'.IsLeftKanExtension α

Tactic:
isLeftKanExtension_of_iso e.symm α' α ?_

Premises used: CategoryTheory.Functor.isLeftKanExtension_of_iso, CategoryTheory.Iso.symm
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
h : F''.IsLeftKanExtension α'
mpr : α' ≫ L.whiskerLeft e.symm.hom = α
⊢ F'.IsLeftKanExtension α

Tactic:
refine isLeftKanExtension_of_iso e.symm α' α ?_

Premises used: CategoryTheory.Functor.isLeftKanExtension_of_iso, CategoryTheory.Iso.symm
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
e : F' ≅ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft e.hom = α'
h : F''.IsLeftKanExtension α'
mpr : (α ≫ L.whiskerLeft e.hom) ≫ L.whiskerLeft e.symm.hom = α
mpr₁ : α ≫ L.whiskerLeft e.hom ≫ L.whiskerLeft e.symm.hom = α
mpr₂ : α ≫ L.whiskerLeft (e.hom ≫ e.symm.hom) = α
mpr₃ : α ≫ L.whiskerLeft (e.hom ≫ e.inv) = α
mpr₄ : α ≫ L.whiskerLeft (𝟙 F') = α
mpr₅ : α ≫ 𝟙 (L ⋙ F') = α
mpr₆ mpr₇ : α = α
⊢ α' ≫ L.whiskerLeft e.symm.hom = α

Tactic:
rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.whiskerLeft_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.whiskerLeft_id'
-- 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'
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 α
G : Functor.{v_1, v_3, u_1, u_3} C H
i : F ≅ G
G' : Functor.{v_4, v_3, u_4, u_3} D H
β : G ⟶ L ⋙ G'
inst_6 : G'.IsLeftKanExtension β
⊢ α ≫ L.whiskerLeft (F'.descOfIsLeftKanExtension α G' (i.hom ≫ β) ≫ G'.descOfIsLeftKanExtension β F' (i.inv ≫ α)) =
    α ≫ L.whiskerLeft (𝟙 F')

Tactic:
simp
-- 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'
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 α
G : Functor.{v_1, v_3, u_1, u_3} C H
i : F ≅ G
G' : Functor.{v_4, v_3, u_4, u_3} D H
β : G ⟶ L ⋙ G'
inst_6 : G'.IsLeftKanExtension β
⊢ β ≫ L.whiskerLeft (G'.descOfIsLeftKanExtension β F' (i.inv ≫ α) ≫ F'.descOfIsLeftKanExtension α G' (i.hom ≫ β)) =
    β ≫ L.whiskerLeft (𝟙 G')

Tactic:
simp
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F' ⟶ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst_3 : F'.IsLeftKanExtension α
mp : F''.IsLeftKanExtension α' → IsIso φ
mpr : IsIso φ → F''.IsLeftKanExtension α'
⊢ F''.IsLeftKanExtension α' ↔ IsIso φ

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
F' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F' ⟶ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst_3 : F'.IsLeftKanExtension α
h : F''.IsLeftKanExtension α'
⊢ α ≫ L.whiskerLeft φ = α ≫ L.whiskerLeft (F'.leftKanExtensionUnique α F'' α').hom

Tactic:
simp [comm]
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F' ⟶ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst_3 : F'.IsLeftKanExtension α
h : F''.IsLeftKanExtension α'
mp : IsIso (F'.leftKanExtensionUnique α F'' α').hom
⊢ IsIso φ

Tactic:
rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom
      (by simp [comm])]

Premises used: CategoryTheory.Functor.hom_ext_of_isLeftKanExtension, CategoryTheory.Functor.leftKanExtensionUnique, CategoryTheory.Iso.hom
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F' ⟶ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst_3 : F'.IsLeftKanExtension α
h : F''.IsLeftKanExtension α'
⊢ IsIso (F'.leftKanExtensionUnique α F'' α').hom

Tactic:
infer_instance
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F' ⟶ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst_3 : F'.IsLeftKanExtension α
h : IsIso φ
⊢ F''.IsLeftKanExtension α'

Tactic:
isLeftKanExtension_of_iso (asIso φ) α α' comm

Premises used: CategoryTheory.Functor.isLeftKanExtension_of_iso, CategoryTheory.asIso
-- 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' F'' : Functor.{v_4, v_3, u_4, u_3} D H
φ : F' ⟶ F''
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'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst_3 : F'.IsLeftKanExtension α
h : IsIso φ
⊢ F''.IsLeftKanExtension α'

Tactic:
exact isLeftKanExtension_of_iso (asIso φ) α α' comm

Premises used: CategoryTheory.Functor.isLeftKanExtension_of_iso, CategoryTheory.asIso
-- 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
α : L ⋙ F' ⟶ F
inst_3 : F'.IsRightKanExtension α
⊢ L.HasRightKanExtension F

Tactic:
(F'.isUniversalOfIsRightKanExtension α).hasTerminal

Premises used: CategoryTheory.Functor.isUniversalOfIsRightKanExtension, CategoryTheory.Limits.IsTerminal.hasTerminal