awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C H
φ : F₁ ⟶ F₂
⊢ Eq (α := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F₁ ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₂)
    (map (L.ran ⋙ obj (whiskeringLeft C D H) L) φ ≫ L.rightKanExtensionCounit F₂)
    (L.rightKanExtensionCounit F₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) φ)
have w : ∀ (x : C),
  Eq (α :=
    (obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F₁).obj x ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F₂).obj x)
    (NatTrans.app (map (L.ran ⋙ obj (whiskeringLeft C D H) L) φ ≫ L.rightKanExtensionCounit F₂) x)
    (NatTrans.app (L.rightKanExtensionCounit F₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) φ) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ (obj L.ran F).IsRightKanExtension (NatTrans.app L.ranCounit F)
have dsimp : (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)
Tactic: dsimp [ran, ranCounit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D H
G : Functor.{v_1, v_3, u_1, u_3} C H
β : F₁ ⟶ F₂
f : F₂ ⟶ obj L.ran G
⊢ Eq (α := obj (obj (whiskeringLeft C D H) L) F₁ ⟶ G)
    ((((obj L.ran G).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G) F₁).symm.symm :
          (a : F₁ ⟶ L.ran.obj G) → ((whiskeringLeft C D H).obj L).obj F₁ ⟶ G)
        (β ≫ f) :
      obj (obj (whiskeringLeft C D H) L) F₁ ⟶ G)
    (map (obj (whiskeringLeft C D H) L) β ≫
        (((obj L.ran G).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G) F₂).symm.symm :
            (a : F₂ ⟶ L.ran.obj G) → ((whiskeringLeft C D H).obj L).obj F₂ ⟶ G)
          f :
      obj (obj (whiskeringLeft C D H) L) F₁ ⟶ G)
have dsimp : (L.whiskerLeft β ≫ L.whiskerLeft f) ≫ NatTrans.app L.ranCounit G =
  L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G
Tactic: dsimp [homEquivOfIsRightKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F₁ F₂ : Functor.{v_2, v_3, u_2, u_3} D H
G : Functor.{v_1, v_3, u_1, u_3} C H
β : F₁ ⟶ F₂
f : F₂ ⟶ obj L.ran G
⊢ (L.whiskerLeft β ≫ L.whiskerLeft f) ≫ NatTrans.app L.ranCounit G =
    L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G
have rw : L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G =
  L.whiskerLeft β ≫ L.whiskerLeft f ≫ NatTrans.app L.ranCounit G
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
⊢ Eq (α := L ⋙ F ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂)
    (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
      (L.whiskerLeft
        ((((obj L.ran G₂).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F).symm :
            (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₂) → F ⟶ L.ran.obj G₂)
          (β ≫ f)))
      (NatTrans.app L.ranCounit G₂))
    (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
      (L.whiskerLeft
        ((((obj L.ran G₁).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F).symm :
              (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁) → F ⟶ L.ran.obj G₁)
            β ≫
          map L.ran f))
      (NatTrans.app L.ranCounit G₂))
have w : ∀ (X : C),
  Eq (α := (L ⋙ F).obj X ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂).obj X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
        (L.whiskerLeft
          ((((obj L.ran G₂).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F).symm :
              (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₂) → F ⟶ L.ran.obj G₂)
            (β ≫ f)))
        (NatTrans.app L.ranCounit G₂))
      X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
        (L.whiskerLeft
          ((((obj L.ran G₁).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F).symm :
                (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁) → F ⟶ L.ran.obj G₁)
              β ≫
            map L.ran f))
        (NatTrans.app L.ranCounit G₂))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ Eq (α := (L ⋙ F).obj X ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂).obj X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
        (L.whiskerLeft
          ((((obj L.ran G₂).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F).symm :
              (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₂) → F ⟶ L.ran.obj G₂)
            (β ≫ f)))
        (NatTrans.app L.ranCounit G₂))
      X)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ obj L.ran G₂)
        (L.whiskerLeft
          ((((obj L.ran G₁).homEquivOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F).symm :
                (a : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁) → F ⟶ L.ran.obj G₁)
              β ≫
            map L.ran f))
        (NatTrans.app L.ranCounit G₂))
      X)
have w : ((obj L.ran G₂).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F (β ≫ f)).app (L.obj X) ≫
    NatTrans.app (NatTrans.app L.ranCounit G₂) X =
  (((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X)) ≫
    NatTrans.app (NatTrans.app L.ranCounit G₂) X
Tactic: dsimp [homEquivOfIsRightKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ ((obj L.ran G₂).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₂) F (β ≫ f)).app (L.obj X) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₂) X =
    (((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
        NatTrans.app (map L.ran f) (L.obj X)) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₂) X
have w : β.app X ≫ f.app X =
  ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
    NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X
Tactic: rw [liftOfIsRightKanExtension_fac_app, NatTrans.comp_app, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X
have h : Eq (α := (obj (L.ran ⋙ obj (whiskeringLeft C D H) L) G₁).obj X ⟶ (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G₂).obj X)
  (NatTrans.app (map (L.ran ⋙ obj (whiskeringLeft C D H) L) f ≫ NatTrans.app L.ranCounit G₂) X)
  (NatTrans.app (NatTrans.app L.ranCounit G₁ ≫ map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) f) X)
Tactic: have h := congr_app (L.ranCounit.naturality f) X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
h :
  Eq (α := (obj L.ran G₁).obj (L.obj X) ⟶ G₂.obj X)
    (NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X)
    (NatTrans.app (NatTrans.app L.ranCounit G₁) X ≫ f.app X)
⊢ β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X
have w : β.app X ≫ f.app X =
  ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
    NatTrans.app (NatTrans.app L.ranCounit G₁) X ≫ f.app X
Tactic: rw [h, liftOfIsRightKanExtension_fac_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_2, v_3, u_2, u_3} D H
G₁ G₂ : Functor.{v_1, v_3, u_1, u_3} C H
β : obj (obj (whiskeringLeft C D H) L) F ⟶ G₁
f : G₁ ⟶ G₂
X : C
h :
  Eq (α := (obj L.ran G₁).obj (L.obj X) ⟶ G₂.obj X)
    (NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X)
    (NatTrans.app (NatTrans.app L.ranCounit G₁) X ≫ f.app X)
w :
  β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (NatTrans.app L.ranCounit G₁) X ≫ f.app X
⊢ β.app X ≫ f.app X =
    ((obj L.ran G₁).liftOfIsRightKanExtension (NatTrans.app L.ranCounit G₁) F β).app (L.obj X) ≫
      NatTrans.app (map L.ran f) (L.obj X) ≫ NatTrans.app (NatTrans.app L.ranCounit G₂) X
have w₁ : β.app X ≫ f.app X = β.app X ≫ f.app X
Tactic: rw [h, liftOfIsRightKanExtension_fac_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_1, v_3, u_1, u_3} C H ⥤ Functor.{v_1, v_3, u_1, u_3} C H)
      (L.ran ⋙ obj (whiskeringLeft C D H) L) (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)))
    (Adjunction.counit (L.ranAdjunction H)) L.ranCounit
have w : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H),
  Eq (α := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F)
    (NatTrans.app (Adjunction.counit (L.ranAdjunction H)) F) (NatTrans.app L.ranCounit F)
Tactic: ext F : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
F : Functor.{v_1, v_3, u_1, u_3} C H
⊢ Eq (α := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F ⟶ obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) F)
    (NatTrans.app (Adjunction.counit (L.ranAdjunction H)) F) (NatTrans.app L.ranCounit F)
have w : 𝟙 (L ⋙ obj L.ran F) ≫ NatTrans.app L.ranCounit F = NatTrans.app L.ranCounit F
Tactic: dsimp [ranAdjunction, homEquivOfIsRightKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} D H
X Y : Functor.{v_1, v_3, u_1, u_3} C H
f : X ⟶ Y
i : C
⊢ Eq (α := obj (L.ran ⋙ lim) X ⟶ Y.obj i)
    (CategoryStruct.comp (Y := limit Y)
      (map (L.ran ⋙ lim) f ≫
        Iso.hom
          ((fun (G : Functor.{v_1, v_3, u_1, u_3} C H) ↦
              ((obj L.ran G).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit G) :
                limit (obj L.ran G) ≅ limit (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G)))
            Y))
      (limit.π Y i))
    (CategoryStruct.comp (Y := limit Y)
      (Iso.hom
            ((fun (G : Functor.{v_1, v_3, u_1, u_3} C H) ↦
                ((obj L.ran G).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit G) :
                  limit (obj L.ran G) ≅ limit (obj (𝟭 (Functor.{v_1, v_3, u_1, u_3} C H)) G)))
              X) ≫
          map lim f :
        obj (L.ran ⋙ lim) X ⟶ obj lim Y)
      (limit.π Y i))
have dsimp : Eq (α := limit (obj L.ran X) ⟶ Y.obj i)
  (CategoryStruct.comp (Y := limit Y)
    (CategoryStruct.comp (Y := limit (obj L.ran Y)) (limMap (map L.ran f))
      (Iso.hom ((obj L.ran Y).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit Y))))
    (limit.π Y i))
  (CategoryStruct.comp (Y := limit Y)
    (CategoryStruct.comp (Y := limit X)
      (Iso.hom ((obj L.ran X).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit X))) (limMap f))
    (limit.π Y i))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} D H
X Y : Functor.{v_1, v_3, u_1, u_3} C H
f : X ⟶ Y
i : C
⊢ Eq (α := limit (obj L.ran X) ⟶ Y.obj i)
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := limit (obj L.ran Y)) (limMap (map L.ran f))
        (Iso.hom ((obj L.ran Y).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit Y))))
      (limit.π Y i))
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := limit X)
        (Iso.hom ((obj L.ran X).limitIsoOfIsRightKanExtension (NatTrans.app L.ranCounit X))) (limMap f))
      (limit.π Y i))
have rw : Eq (α := limit (obj L.ran X) ⟶ Y.obj i)
  (limit.π (obj L.ran X) (L.obj i) ≫ NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
  (limit.π (obj L.ran X) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app i)
Tactic: rw [assoc, assoc, limMap_π, limitIsoOfIsRightKanExtension_hom_π_assoc,
        limitIsoOfIsRightKanExtension_hom_π, limMap_π_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L_1 : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L_1.HasRightKanExtension F
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : ∀ (G : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension G
inst_5 : HasLimitsOfShape.{v_1, u_1, v_3, u_3} C H
inst_6 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} D H
X Y : Functor.{v_1, v_3, u_1, u_3} C H
f : X ⟶ Y
i : C
⊢ Eq (α := limit (obj L.ran X) ⟶ Y.obj i)
    (limit.π (obj L.ran X) (L.obj i) ≫
      NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
    (limit.π (obj L.ran X) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app i)
have e_a : Eq (α := (obj L.ran X).obj (L.obj i) ⟶ Y.obj i)
  (NatTrans.app (map L.ran f) (L.obj i) ≫ NatTrans.app (NatTrans.app L.ranCounit Y) i)
  (NatTrans.app (NatTrans.app L.ranCounit X) i ≫ f.app i)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Adjunction (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
H : Type u_3
inst_2 : Category.{v_3, u_3} H
inst_3 : L.Full
inst_4 : L.Faithful
F : Functor.{v_1, v_3, u_1, u_3} C H
inst_5 : L.HasPointwiseRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_3, u_1, u_3} C H), L.HasRightKanExtension F
⊢ IsIso (X := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app (Adjunction.counit (L.ranAdjunction H)) F)
have rw : IsIso (X := obj (L.ran ⋙ obj (whiskeringLeft C D H) L) F) (NatTrans.app L.ranCounit F)
Tactic: rw [ranAdjunction_counit]
-- 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 ≫ α' = α
⊢ F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'
have mp : F'.IsRightKanExtension α → 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
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 α'
⊢ F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'
have mpr : F''.IsRightKanExtension α' → 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
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 α
have mpr : L.whiskerLeft e.symm.hom ≫ α = α'
Tactic: refine isRightKanExtension_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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
h : F''.IsRightKanExtension α'
⊢ L.whiskerLeft e.symm.hom ≫ α = α'
have mpr : L.whiskerLeft e.symm.hom ≫ L.whiskerLeft e.hom ≫ α' = α'
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
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 ≫ α' = α'
⊢ L.whiskerLeft e.symm.hom ≫ α = α'
have mpr₁ : L.whiskerLeft (e.symm.hom ≫ e.hom) ≫ α' = α'
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
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) ≫ α' = α'
⊢ L.whiskerLeft e.symm.hom ≫ α = α'
have mpr₂ : L.whiskerLeft (e.inv ≫ e.hom) ≫ α' = α'
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
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) ≫ α' = α'
⊢ L.whiskerLeft e.symm.hom ≫ α = α'
have mpr₃ : L.whiskerLeft (𝟙 F'') ≫ α' = α'
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
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'') ≫ α' = α'
⊢ L.whiskerLeft e.symm.hom ≫ α = α'
have mpr₄ : 𝟙 (L ⋙ F'') ≫ α' = α'
Tactic: rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]