awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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'') ≫ α' = α'
⊢ L.whiskerLeft e.symm.hom ≫ α = α'
have mpr₅ : α' = α'
Tactic: rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α
⊢ F''.IsRightKanExtension α' ↔ IsIso φ
have mp : F''.IsRightKanExtension α' → IsIso φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 φ
⊢ F''.IsRightKanExtension α' ↔ IsIso φ
have mpr : IsIso φ → F''.IsRightKanExtension α'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 φ
have mp : IsIso (F''.rightKanExtensionUnique α' F' α).hom
Tactic: rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom
      (by simp [comm])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 = α'
⊢ F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α'
have mp : F'.IsLeftKanExtension α → F''.IsLeftKanExtension α'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α'
⊢ F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α'
have mpr : F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α
have mpr : α' ≫ L.whiskerLeft e.symm.hom = α
Tactic: refine isLeftKanExtension_of_iso e.symm α' α ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α'
⊢ α' ≫ L.whiskerLeft e.symm.hom = α
have mpr : (α ≫ L.whiskerLeft e.hom) ≫ L.whiskerLeft e.symm.hom = α
Tactic: rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 = α
⊢ α' ≫ L.whiskerLeft e.symm.hom = α
have mpr₁ : α ≫ L.whiskerLeft e.hom ≫ L.whiskerLeft e.symm.hom = α
Tactic: rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 = α
⊢ α' ≫ L.whiskerLeft e.symm.hom = α
have mpr₂ : α ≫ L.whiskerLeft (e.hom ≫ e.symm.hom) = α
Tactic: rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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) = α
⊢ α' ≫ L.whiskerLeft e.symm.hom = α
have mpr₃ : α ≫ L.whiskerLeft (e.hom ≫ e.inv) = α
Tactic: rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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) = α
⊢ α' ≫ L.whiskerLeft e.symm.hom = α
have mpr₄ : α ≫ L.whiskerLeft (𝟙 F') = α
Tactic: rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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') = α
⊢ α' ≫ L.whiskerLeft e.symm.hom = α
have mpr₅ : α ≫ 𝟙 (L ⋙ F') = α
Tactic: rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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') = α
⊢ α' ≫ L.whiskerLeft e.symm.hom = α
have mpr₆ : α = α
Tactic: rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α
⊢ F''.IsLeftKanExtension α' ↔ IsIso φ
have mp : F''.IsLeftKanExtension α' → IsIso φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 φ
⊢ F''.IsLeftKanExtension α' ↔ IsIso φ
have mpr : IsIso φ → F''.IsLeftKanExtension α'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 φ
have mp : IsIso (F'.leftKanExtensionUnique α F'' α').hom
Tactic: rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom
      (by simp [comm])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
inst_3 : Category.{v_5, u_5} D'
L : Functor.{v_1, v_4, u_1, u_4} C D
L' : Functor.{v_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)
have mp : F'.IsLeftKanExtension α → (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
inst_3 : Category.{v_5, u_5} D'
L : Functor.{v_1, v_4, u_1, u_4} C D
L' : Functor.{v_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)
⊢ F'.IsLeftKanExtension α ↔ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)
have mpr : (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
inst_3 : Category.{v_5, u_5} D'
L : Functor.{v_1, v_4, u_1, u_4} C D
L' : Functor.{v_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' ≫ α)
have mp : F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} H
inst_2 : Category.{v_4, u_4} D
inst_3 : Category.{v_5, u_5} D'
L : Functor.{v_1, v_4, u_1, u_4} C D
L' : Functor.{v_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' ≫ α)
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)
have mpr : (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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)
have mp : F'.IsLeftKanExtension α → F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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)
⊢ F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)
have mpr : F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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 α)
have mp : F'.IsRightKanExtension α → F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
Goal:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
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 α)
⊢ F'.IsRightKanExtension α ↔ F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α)
have mpr : F'.IsRightKanExtension ((G.associator L F').hom ≫ G.whiskerLeft α) → F'.IsRightKanExtension α
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α₂
have mp : F₁'.IsLeftKanExtension α₁ → F₂'.IsLeftKanExtension α₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α₂
⊢ F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂
have mpr : F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Basic (goal)
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 α₂
have mp : F₁'.IsRightKanExtension α₁ → F₂'.IsRightKanExtension α₂
Tactic: constructor