awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x : WithTerminal (Discrete J)
⊢ (fun (x : WidePullbackShape J) ↦
        (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
          | some x => of { as := x }
          | none => star :
          WithTerminal (Discrete J)))
      ((fun (x : WithTerminal (Discrete J)) ↦
          (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
            | of x => some x.as
            | star => none :
            WidePullbackShape J))
        x) =
    x
have of : ∀ (a : Discrete J),
  (fun (x : WidePullbackShape J) ↦
        (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
          | some x => of { as := x }
          | none => star :
          WithTerminal (Discrete J)))
      ((fun (x : WithTerminal (Discrete J)) ↦
          (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
            | of x => some x.as
            | star => none :
            WidePullbackShape J))
        (of a)) =
    of a
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
J : Type u_1
x : WithTerminal (Discrete J)
of :
  ∀ (a : Discrete J),
    (fun (x : WidePullbackShape J) ↦
          (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
            | some x => WithTerminal.of { as := x }
            | none => star :
            WithTerminal (Discrete J)))
        ((fun (x : WithTerminal (Discrete J)) ↦
            (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
              | WithTerminal.of x => some x.as
              | star => none :
              WidePullbackShape J))
          (WithTerminal.of a)) =
      WithTerminal.of a
⊢ (fun (x : WidePullbackShape J) ↦
        (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
          | some x => WithTerminal.of { as := x }
          | none => star :
          WithTerminal (Discrete J)))
      ((fun (x : WithTerminal (Discrete J)) ↦
          (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
            | WithTerminal.of x => some x.as
            | star => none :
            WidePullbackShape J))
        x) =
    x
have star : Eq.{u_1 + 1} (α := WithTerminal (Discrete J))
  ((fun (x : WidePullbackShape J) ↦
      (match (motive := WidePullbackShape J → WithTerminal (Discrete J)) x with
        | some x => WithTerminal.of { as := x }
        | none => star :
        WithTerminal (Discrete J)))
    ((fun (x : WithTerminal (Discrete J)) ↦
        (match (motive := WithTerminal (Discrete J) → WidePullbackShape J) x with
          | WithTerminal.of x => some x.as
          | star => none :
          WidePullbackShape J))
      star))
  star
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x_1 y_1 : WidePullbackShape J
x y : J
f :
  Quiver.Hom (V := WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some x) :
      WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
      WithTerminal (Discrete J))
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)
have eq : x = y
Tactic: have eq : x = y := PLift.down (ULift.down (down f))
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
x_1 y_1 : WidePullbackShape J
x y : J
f :
  Quiver.Hom (V := WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some x) :
      WithTerminal (Discrete J))
    ((widePullbackShapeEquivObj : (a : WidePullbackShape J) → WithTerminal (Discrete J)) (some y) :
      WithTerminal (Discrete J))
eq : x = y
⊢ WidePullbackShape.Hom (some y) (some y) = (some x ⟶ some y)
have rw : WidePullbackShape.Hom (some y) (some y) = (some y ⟶ some y)
Tactic: rw [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 (WithInitial (↑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 (WithInitial (↑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 (WithInitial (↑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 (WithInitial (↑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 (WithInitial (↑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 (WithInitial (↑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 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 h : ∀ (X : (↑(prelaxfunctor.obj a) : Type u_1)),
  (prelaxfunctor.map₂ (Bicategory.associator f g h).hom).toNatTrans.app X =
    ((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).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 : (↑(prelaxfunctor.obj a) : Type u_1)
⊢ (prelaxfunctor.map₂ (Bicategory.associator f g h).hom).toNatTrans.app X =
    ((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).toNatTrans.app
      X
have h : ∀ (a_1 : (↑a : Type u_1)),
  Eq (α :=
    (prelaxfunctor.map ((f ≫ g) ≫ h)).toFunctor.obj (of a_1) ⟶ (prelaxfunctor.map (f ≫ g ≫ h)).toFunctor.obj (of a_1))
    ((prelaxfunctor.map₂ (Bicategory.associator f g h).hom).toNatTrans.app (of a_1))
    (((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).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 : (↑(prelaxfunctor.obj a) : Type u_1)
h :
  ∀ (a_1 : (↑a : Type u_1)),
    Eq (α :=
      (prelaxfunctor.map ((f ≫ g) ≫ h_1)).toFunctor.obj (of a_1) ⟶
        (prelaxfunctor.map (f ≫ g ≫ h_1)).toFunctor.obj (of a_1))
      ((prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom).toNatTrans.app (of a_1))
      (((Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
              Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
                (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
                  Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
                    (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h_1).toFunctor)).inv).toNatTrans.app
        (of a_1))
⊢ (prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom).toNatTrans.app X =
    ((Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
              (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
                Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
                  (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h_1).toFunctor)).inv).toNatTrans.app
      X
have h₁ : Eq (α := (prelaxfunctor.map ((f ≫ g) ≫ h_1)).toFunctor.obj star ⟶ (prelaxfunctor.map (f ≫ g ≫ h_1)).toFunctor.obj star)
  ((prelaxfunctor.map₂ (Bicategory.associator f g h_1).hom).toNatTrans.app star)
  (((Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h_1.toFunctor)).hom ≫
          Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h_1) ≫
            (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h_1)).hom ≫
              Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h_1.toFunctor)).inv ≫
                (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ 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
D : Type u_1
inst_1 : Category.{v_1, u_1} D
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (of Y)) =
    Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star) ≫
      (lift F M hM).map f
have star : Eq (α := G.obj star ⟶ (lift F M hM).obj (of Y))
  (CategoryStruct.comp (Y := G.obj (of Y)) (G.map PUnit.unit)
    (Iso.hom
      ((fun (X : WithInitial C) ↦
          (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
            | of x => h.app x
            | star => hG :
            G.obj X ≅ (lift F M hM).obj X))
        (of Y))))
  (CategoryStruct.comp (Y := (lift F M hM).obj star)
    (Iso.hom
      ((fun (X : WithInitial C) ↦
          (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
            | of x => h.app x
            | star => hG :
            G.obj X ≅ (lift F M hM).obj X))
        star))
    ((lift F M hM).map PUnit.unit))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ Eq (α := G.obj star ⟶ (lift F M hM).obj (of Y))
    (CategoryStruct.comp (Y := G.obj (of Y)) (G.map PUnit.unit)
      (Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          (of Y))))
    (CategoryStruct.comp (Y := (lift F M hM).obj star)
      (Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star))
      ((lift F M hM).map PUnit.unit))
have star : G.map PUnit.unit ≫ h.hom.app Y = hG.hom ≫ (lift F M hM).map PUnit.unit
Tactic: change G.map _ ≫ h.hom.app _ = hG.hom ≫ _
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ G.map PUnit.unit ≫ h.hom.app Y = hG.hom ≫ (lift F M hM).map PUnit.unit
have star : hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ h.hom.app Y
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ h.hom.app Y
have star : (lift F M hM).map PUnit.unit = (M Y ≫ h.symm.hom.app Y) ≫ h.hom.app Y
Tactic: erw [← Iso.eq_inv_comp, ← Category.assoc, hh]
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
f : Quiver.Hom.{v, u} (V := WithInitial C) star star
⊢ G.map f ≫
      Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star) =
    Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star) ≫
      (lift F M hM).map f
have star : Eq (α := G.obj star ⟶ (lift F M hM).obj star)
  (CategoryStruct.comp (Y := G.obj star) (G.map PUnit.unit)
    (Iso.hom
      ((fun (X : WithInitial C) ↦
          (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
            | of x => h.app x
            | star => hG :
            G.obj X ≅ (lift F M hM).obj X))
        star)))
  (CategoryStruct.comp (Y := (lift F M hM).obj star)
    (Iso.hom
      ((fun (X : WithInitial C) ↦
          (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
            | of x => h.app x
            | star => hG :
            G.obj X ≅ (lift F M hM).obj X))
        star))
    ((lift F M hM).map PUnit.unit))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
Z : D
F : Functor.{v, v_1, u, u_1} C D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : Functor.{v, v_1, u, u_1} (WithInitial C) D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh :
  ∀ (x : C),
    hG.symm.hom ≫ G.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) = M x ≫ h.symm.hom.app x
⊢ Eq (α := G.obj star ⟶ (lift F M hM).obj star)
    (CategoryStruct.comp (Y := G.obj star) (G.map PUnit.unit)
      (Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star)))
    (CategoryStruct.comp (Y := (lift F M hM).obj star)
      (Iso.hom
        ((fun (X : WithInitial C) ↦
            (match (motive := (X : WithInitial C) → G.obj X ≅ (lift F M hM).obj X) X with
              | of x => h.app x
              | star => hG :
              G.obj X ≅ (lift F M hM).obj X))
          star))
      ((lift F M hM).map PUnit.unit))
have star : G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z
Tactic: change G.map (𝟙 _) ≫ hG.hom = hG.hom ≫ 𝟙 _
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} (WithInitial C) D
x y : C
f : x ⟶ y
⊢ Functor.map (Functor.obj (Functor.const C) (F.obj star)) f ≫ F.map (Limits.IsInitial.to starInitial (of y)) =
    F.map (Limits.IsInitial.to starInitial (of x)) ≫ (Functor.obj (𝟭 (Functor.{v, v_1, u, u_1} C D)) (incl ⋙ F)).map f
have dsimp : 𝟙 (F.obj star) ≫ F.map (Limits.IsInitial.to starInitial (of y)) =
  F.map (Limits.IsInitial.to starInitial (of x)) ≫ F.map (Functor.map incl f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} (WithInitial C) D
x y : C
f : x ⟶ y
⊢ 𝟙 (F.obj star) ≫ F.map (Limits.IsInitial.to starInitial (of y)) =
    F.map (Limits.IsInitial.to starInitial (of x)) ≫ F.map (Functor.map incl f)
have rw : F.map (Limits.IsInitial.to starInitial (of y)) = F.map (Limits.IsInitial.to starInitial (of x) ≫ Functor.map incl f)
Tactic: rw [Category.id_comp, ← F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} (WithInitial C) D
x y : C
f : x ⟶ y
⊢ Eq (α := F.obj star ⟶ (incl ⋙ F).obj y)
    ((fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (of x))) x ≫ (incl ⋙ F).map f)
    ((fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (of x))) y)
have simp : F.map (Limits.IsInitial.to starInitial (of x)) ≫ F.map (Functor.map incl f) =
  F.map (Limits.IsInitial.to starInitial (of y))
Tactic: simp only [Functor.comp_obj, Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} (WithInitial C) D
x y : C
f : x ⟶ y
⊢ F.map (Limits.IsInitial.to starInitial (of x)) ≫ F.map (Functor.map incl f) =
    F.map (Limits.IsInitial.to starInitial (of y))
have rw : F.map (Limits.IsInitial.to starInitial (of x) ≫ Functor.map incl f) = F.map (Limits.IsInitial.to starInitial (of y))
Tactic: rw [← F.map_comp]