awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
F : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsIso α
⊢ whiskerRight (inv α) F = inv (whiskerRight α F)
have hom_inv_id : whiskerRight (inv α) F ≫ whiskerRight α F = 𝟙 (H ⋙ F)
Tactic: apply IsIso.eq_inv_of_inv_hom_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
inst_3 : IsIso α
⊢ inv (F.whiskerLeft α) = F.whiskerLeft (inv α)
have symm : F.whiskerLeft (inv α) = inv (F.whiskerLeft α)
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
inst_3 : IsIso α
⊢ F.whiskerLeft (inv α) = inv (F.whiskerLeft α)
have hom_inv_id : F.whiskerLeft (inv α) ≫ F.whiskerLeft α = 𝟙 (F ⋙ H)
Tactic: apply IsIso.eq_inv_of_inv_hom_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ≅ G
β : H ≅ K
⊢ F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β
have w : ∀ (x : C), (F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K).hom.app x = (isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β).hom.app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Widesubcategory (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty.{v₁, u₂} D
inst_1 : P.IsMultiplicative
X Y : InducedWideCategory D F P
f g : X ⟶ Y
eq :
  Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
    (Functor.map (wideInducedFunctor F P) f) (Functor.map (wideInducedFunctor F P) g)
⊢ f = g
have mk : ∀ (hom : F X ⟶ F Y) (property : P hom)
  (eq :
    Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
      (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom property)) (Functor.map (wideInducedFunctor F P) g)),
  Hom.mk (P := P) hom property = g
Tactic: cases f
Cleared hypotheses: f, eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Widesubcategory (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty.{v₁, u₂} D
inst_1 : P.IsMultiplicative
X Y : InducedWideCategory D F P
g : X ⟶ Y
hom : F X ⟶ F Y
property : P hom
eq :
  Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
    (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom property)) (Functor.map (wideInducedFunctor F P) g)
⊢ Hom.mk (P := P) hom property = g
have mk : ∀ (hom_1 : F X ⟶ F Y) (property_1 : P hom_1)
  (eq :
    Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
      (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom property))
      (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom_1 property_1))),
  Hom.mk (P := P) hom property = Hom.mk (P := P) hom_1 property_1
Tactic: cases g
Cleared hypotheses: g, eq
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
⊢ NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f))) = 𝟙 (map f.toFunctor).toCatHom
have h : ∀ (X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)),
  (NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app X =
    (Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
⊢ (NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app X =
    (Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app X
have h : ∀ (a_1 : (↑a : Type u_1)),
  Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map f.toFunctor).toCatHom.toFunctor.obj (of a_1))
    ((NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app (of a_1))
    ((Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app (of a_1))
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map f.toFunctor).toCatHom.toFunctor.obj (of a_1))
      ((NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app (of a_1))
      ((Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app (of a_1))
⊢ (NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app X =
    (Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app X
have h₁ : Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj star ⟶ (map f.toFunctor).toCatHom.toFunctor.obj star)
  ((NatTrans.toCatHom₂ (map₂ (Cat.Hom₂.toNatTrans (𝟙 f)))).toNatTrans.app star)
  ((Cat.Hom₂.toNatTrans (𝟙 (map f.toFunctor).toCatHom)).app star)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans) =
    NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)
have h : ∀ (X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)),
  (NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
⊢ (NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app X
have h : ∀ (a_1 : (↑a : Type u_1)),
  Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map h.toFunctor).toCatHom.toFunctor.obj (of a_1))
    ((NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app (of a_1))
    ((NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app (of a_1))
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f g h_1 : a ⟶ b
η : f ⟶ g
θ : g ⟶ h_1
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj (of a_1) ⟶ (map h_1.toFunctor).toCatHom.toFunctor.obj (of a_1))
      ((NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app (of a_1))
      ((NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app (of a_1))
⊢ (NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app X
have h₁ : Eq (α := (map f.toFunctor).toCatHom.toFunctor.obj star ⟶ (map h_1.toFunctor).toCatHom.toFunctor.obj star)
  ((NatTrans.toCatHom₂ (map₂ (η ≫ θ).toNatTrans)).toNatTrans.app star)
  ((NatTrans.toCatHom₂ (map₂ η.toNatTrans) ≫ NatTrans.toCatHom₂ (map₂ θ.toNatTrans)).toNatTrans.app star)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ prelaxfunctor.map₂ (Bicategory.whiskerLeft f η) =
    (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
      Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
        (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).inv
have h : ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
  (prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).inv).toNatTrans.app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
X : (↑(prelaxfunctor.obj a) : Type u_1)
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).inv).toNatTrans.app
      X
have h : ∀ (a_1 : (↑a : Type u_1)),
  Eq (α := (prelaxfunctor.map (f ≫ g)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (f ≫ h)).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app (of a_1))
    (((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).inv).toNatTrans.app
      (of a_1))
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f : a ⟶ b
g h_1 : b ⟶ c
η : g ⟶ h_1
X : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α := (prelaxfunctor.map (f ≫ g)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
              Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
                (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv).toNatTrans.app
        (of a_1))
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv).toNatTrans.app
      X
have h₁ : Eq (α := (prelaxfunctor.map (f ≫ g)).toFunctor.obj star ⟶ (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj star)
  ((prelaxfunctor.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app star)
  (((Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom ≫
          Bicategory.whiskerLeft (prelaxfunctor.map f) (prelaxfunctor.map₂ η) ≫
            (Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).inv).toNatTrans.app
    star)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ prelaxfunctor.map₂ (Bicategory.whiskerRight η h) =
    (Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).hom ≫
      Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h) ≫
        (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv
have h : ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
  (prelaxfunctor.map₂ (Bicategory.whiskerRight η h)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv).toNatTrans.app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
X : (↑(prelaxfunctor.obj a) : Type u_1)
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerRight η h)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv).toNatTrans.app
      X
have h : ∀ (a_1 : (↑a : Type u_1)),
  Eq (α := (prelaxfunctor.map (f ≫ h)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (g ≫ h)).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h)).toNatTrans.app (of a_1))
    (((Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv).toNatTrans.app
      (of a_1))
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h_1 : b ⟶ c
X : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α :=
      (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (g ≫ h_1)).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
              Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
                (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
        (of a_1))
⊢ (prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
      X
have h₁ : Eq (α := (prelaxfunctor.map (f ≫ h_1)).toFunctor.obj star ⟶ (prelaxfunctor.map (g ≫ h_1)).toFunctor.obj star)
  ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h_1)).toNatTrans.app star)
  (((Cat.Hom.isoMk (mapComp f.toFunctor h_1.toFunctor)).hom ≫
          Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h_1) ≫
            (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv).toNatTrans.app
    star)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c : Cat
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
a_1 : (↑a : Type u_1)
⊢ Eq (α := (prelaxfunctor.map (f ≫ h)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (g ≫ h)).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.whiskerRight η h)).toNatTrans.app (of a_1))
    (((Cat.Hom.isoMk (mapComp f.toFunctor h.toFunctor)).hom ≫
            Bicategory.whiskerRight (prelaxfunctor.map₂ η) (prelaxfunctor.map h) ≫
              (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv).toNatTrans.app
      (of a_1))
have h : h.toFunctor.map (η.toNatTrans.app a_1) = h.toFunctor.map (down (η.toNatTrans.app a_1))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ prelaxfunctor.map₂ (Bicategory.associator f g h).hom =
    (Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h.toFunctor)).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h) ≫
        (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h)).hom ≫
          Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h).toFunctor)).inv
have dsimp : NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom) =
  NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
    Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom) (map h.toFunctor).toCatHom ≫
      (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom (map h.toFunctor).toCatHom).hom ≫
        Bicategory.whiskerLeft (map f.toFunctor).toCatHom (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
          NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom) =
    NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
      Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom) (map h.toFunctor).toCatHom ≫
        (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom (map h.toFunctor).toCatHom).hom ≫
          Bicategory.whiskerLeft (map f.toFunctor).toCatHom (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
            NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv
have h : ∀ (X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)),
  (NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv).toNatTrans.app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
⊢ (NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv).toNatTrans.app
      X
have h : ∀ (a_1 : (↑a : Type u_1)),
  Eq (α :=
    (map ((f.toFunctor ⋙ g.toFunctor) ⋙ h.toFunctor)).toCatHom.toFunctor.obj (of a_1) ⟶
      (map (f.toFunctor ⋙ g.toFunctor ⋙ h.toFunctor)).toCatHom.toFunctor.obj (of a_1))
    ((NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h.toFunctor).hom)).toNatTrans.app (of a_1))
    ((NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h.toFunctor)).inv).toNatTrans.app
      (of a_1))
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b c d : Cat
f : a ⟶ b
g : b ⟶ c
h_1 : c ⟶ d
X : (↑(Cat.of (WithTerminal (↑a : Type u_1))) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α :=
      (map ((f.toFunctor ⋙ g.toFunctor) ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj (of a_1) ⟶
        (map (f.toFunctor ⋙ g.toFunctor ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj (of a_1))
      ((NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom)).toNatTrans.app (of a_1))
      ((NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
              Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                  (map h_1.toFunctor).toCatHom ≫
                (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                      (map h_1.toFunctor).toCatHom).hom ≫
                  Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                      (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
                    NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv).toNatTrans.app
        (of a_1))
⊢ (NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom)).toNatTrans.app X =
    (NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
            Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
                (map h_1.toFunctor).toCatHom ≫
              (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                    (map h_1.toFunctor).toCatHom).hom ≫
                Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                    (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
                  NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv).toNatTrans.app
      X
have h₁ : Eq (α :=
  (map ((f.toFunctor ⋙ g.toFunctor) ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj star ⟶
    (map (f.toFunctor ⋙ g.toFunctor ⋙ h_1.toFunctor)).toCatHom.toFunctor.obj star)
  ((NatTrans.toCatHom₂ (map₂ (f.toFunctor.associator g.toFunctor h_1.toFunctor).hom)).toNatTrans.app star)
  ((NatTrans.toCatHom₂ (mapComp (f.toFunctor ⋙ g.toFunctor) h_1.toFunctor).hom ≫
          Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f.toFunctor g.toFunctor).hom)
              (map h_1.toFunctor).toCatHom ≫
            (Bicategory.associator (map f.toFunctor).toCatHom (map g.toFunctor).toCatHom
                  (map h_1.toFunctor).toCatHom).hom ≫
              Bicategory.whiskerLeft (map f.toFunctor).toCatHom
                  (NatTrans.toCatHom₂ (mapComp g.toFunctor h_1.toFunctor).inv) ≫
                NatTrans.toCatHom₂ (mapComp f.toFunctor (g.toFunctor ⋙ h_1.toFunctor)).inv).toNatTrans.app
    star)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a b : Cat
f : a ⟶ b
⊢ prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom =
    (Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
      Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
        (Bicategory.leftUnitor (prelaxfunctor.map f)).hom
have h : ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
  (prelaxfunctor.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp (Cat.Hom.toFunctor (𝟙 a)) f.toFunctor)).hom ≫
            Bicategory.whiskerRight (Iso.hom (Cat.Hom.isoMk (mapId (↑a : Type u_1)))) (prelaxfunctor.map f) ≫
              (Bicategory.leftUnitor (prelaxfunctor.map f)).hom).toNatTrans.app
      X
Tactic: ext X