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
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} (WithInitial C) D
x : C
⊢ Iso.hom (Iso.symm (Iso.refl (F.obj star))) ≫
      F.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) =
    (fun (x : C) ↦ F.map (Limits.IsInitial.to starInitial (of x))) x ≫
      NatTrans.app (Iso.hom (Iso.symm (Iso.refl (incl ⋙ F)))) x
have simp : F.map (Limits.IsInitial.to starInitial (Functor.obj.{v, v, u, u} incl x)) =
  F.map (Limits.IsInitial.to starInitial (of x))
Tactic: simp only [Iso.refl_symm, Iso.refl_hom, Category.id_comp, Functor.comp_obj,
            NatTrans.id_app, Category.comp_id]
-- 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
x : Functor.{v, v_1, u, u_1} (WithInitial C) D
⊢ mkCommaMorphism
      (Iso.hom
        (NatIso.ofComponents
          (fun (X : WithInitial C) ↦
            match (motive :=
              (X : WithInitial C) →
                x.obj X ≅
                  match (motive := WithInitial C → D) X with
                  | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                  | star => x.obj star)
              X with
            | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
            | star => Iso.refl (x.obj star))
          ⋯)) =
    𝟙 (mkCommaObject x)
have h₁ : CommaMorphism.left
    (mkCommaMorphism
      (Iso.hom
        (NatIso.ofComponents
          (fun (X : WithInitial C) ↦
            match (motive :=
              (X : WithInitial C) →
                x.obj X ≅
                  match (motive := WithInitial C → D) X with
                  | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                  | star => x.obj star)
              X with
            | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
            | star => Iso.refl (x.obj star))
          sorry))) =
  CommaMorphism.left (𝟙 (mkCommaObject x))
Tactic: ext
-- 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
x : Functor.{v, v_1, u, u_1} (WithInitial C) D
h₁ :
  CommaMorphism.left
      (mkCommaMorphism
        (Iso.hom
          (NatIso.ofComponents
            (fun (X : WithInitial C) ↦
              match (motive :=
                (X : WithInitial C) →
                  x.obj X ≅
                    match (motive := WithInitial C → D) X with
                    | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                    | star => x.obj star)
                X with
              | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
              | star => Iso.refl (x.obj star))
            ⋯))) =
    CommaMorphism.left (𝟙 (mkCommaObject x))
⊢ mkCommaMorphism
      (Iso.hom
        (NatIso.ofComponents
          (fun (X : WithInitial C) ↦
            match (motive :=
              (X : WithInitial C) →
                x.obj X ≅
                  match (motive := WithInitial C → D) X with
                  | of x_1 => x.obj (Functor.obj.{v, v, u, u} incl x_1)
                  | star => x.obj star)
              X with
            | of x_1 => Iso.app (Iso.refl (incl ⋙ x)) x_1
            | star => Iso.refl (x.obj star))
          ⋯)) =
    𝟙 (mkCommaObject x)
have h₂ : ∀ (x_1 : C),
  NatTrans.app
      (CommaMorphism.right
        (mkCommaMorphism
          (Iso.hom
            (NatIso.ofComponents
              (fun (X : WithInitial C) ↦
                match (motive :=
                  (X : WithInitial C) →
                    x.obj X ≅
                      match (motive := WithInitial C → D) X with
                      | of x_2 => x.obj (Functor.obj.{v, v, u, u} incl x_2)
                      | star => x.obj star)
                  X with
                | of x_2 => Iso.app (Iso.refl (incl ⋙ x)) x_2
                | star => Iso.refl (x.obj star))
              sorry))))
      x_1 =
    (CommaMorphism.right (𝟙 (mkCommaObject x))).app x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.Cone (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
K : J ⥤ Under.{v₁, u₁} X
F : Functor.{v₁, v₂, u₁, u₂} C D
t_1 : Cocone K
t : Cocone (Functor.obj liftFromUnder K)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    K.obj x ⟶
      Functor.obj
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        x_1)
    (K.map f ≫ Under.homMk (t.ι.app (of x_1)) ⋯)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        x)
      (Under.homMk (t.ι.app (of x)) ⋯)
      (Functor.map
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        f))
have h : Eq (α :=
  (K.obj x).right ⟶
    Under.right (X := X)
      (Functor.obj
          (Functor.obj (Functor.const J)
            (Under.mk (Y :=
              Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
              (t.ι.app star)))
          x_1 :
        Under.{v₁, u₁} X))
  (Under.Hom.right (K.map f ≫ Under.homMk (t.ι.app (of x_1)) sorry))
  (Under.Hom.right
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        x)
      (Under.homMk (t.ι.app (of x)) sorry)
      (Functor.map
        (Functor.obj (Functor.const J)
          (Under.mk (Y :=
            Functor.obj.{w', v₁, w, u₁} (C := WithInitial J) (Functor.obj (Functor.const (WithInitial J)) t.pt) star)
            (t.ι.app star)))
        f)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : Option C
⊢ (fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => some a
          | star => none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => of a
            | none => star :
            WithTerminal C))
        a) =
    a
have none : Eq.{u + 1} (α := Option C)
  ((fun (x : WithTerminal C) ↦
      (match (motive := WithTerminal C → Option C) x with
        | of a => some a
        | star => none :
        Option C))
    ((fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => of a
          | none => star :
          WithTerminal C))
      none))
  none
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : Option C
none :
  Eq.{u + 1} (α := Option C)
    ((fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => of a
            | Option.none => star :
            WithTerminal C))
        Option.none))
    Option.none
⊢ (fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => of a
            | Option.none => star :
            WithTerminal C))
        a) =
    a
have some : ∀ (val : C),
  (fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | of a => some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => of a
            | Option.none => star :
            WithTerminal C))
        (some val)) =
    some val
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : WithTerminal C
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => of a
          | none => star :
          WithTerminal C))
      ((fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        a) =
    a
have of : ∀ (a : C),
  (fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => of a
          | none => star :
          WithTerminal C))
      ((fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        (of a)) =
    of a
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : WithTerminal C
of :
  ∀ (a : C),
    (fun (x : Option C) ↦
          (match (motive := Option C → WithTerminal C) x with
            | some a => WithTerminal.of a
            | none => star :
            WithTerminal C))
        ((fun (x : WithTerminal C) ↦
            (match (motive := WithTerminal C → Option C) x with
              | WithTerminal.of a => some a
              | star => none :
              Option C))
          (WithTerminal.of a)) =
      WithTerminal.of a
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithTerminal C) x with
          | some a => WithTerminal.of a
          | none => star :
          WithTerminal C))
      ((fun (x : WithTerminal C) ↦
          (match (motive := WithTerminal C → Option C) x with
            | WithTerminal.of a => some a
            | star => none :
            Option C))
        a) =
    a
have star : Eq.{u + 1} (α := WithTerminal C)
  ((fun (x : Option C) ↦
      (match (motive := Option C → WithTerminal C) x with
        | some a => WithTerminal.of a
        | none => star :
        WithTerminal C))
    ((fun (x : WithTerminal C) ↦
        (match (motive := WithTerminal C → Option C) x with
          | WithTerminal.of a => some a
          | star => none :
          Option C))
      star))
  star
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : Option C
⊢ (fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => some a
          | star => none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => of a
            | none => star :
            WithInitial C))
        a) =
    a
have none : Eq.{u + 1} (α := Option C)
  ((fun (x : WithInitial C) ↦
      (match (motive := WithInitial C → Option C) x with
        | of a => some a
        | star => none :
        Option C))
    ((fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => of a
          | none => star :
          WithInitial C))
      none))
  none
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : Option C
none :
  Eq.{u + 1} (α := Option C)
    ((fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => of a
            | Option.none => star :
            WithInitial C))
        Option.none))
    Option.none
⊢ (fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => of a
            | Option.none => star :
            WithInitial C))
        a) =
    a
have some : ∀ (val : C),
  (fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | of a => some a
          | star => Option.none :
          Option C))
      ((fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => of a
            | Option.none => star :
            WithInitial C))
        (some val)) =
    some val
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : WithInitial C
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => of a
          | none => star :
          WithInitial C))
      ((fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        a) =
    a
have of : ∀ (a : C),
  (fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => of a
          | none => star :
          WithInitial C))
      ((fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | of a => some a
            | star => none :
            Option C))
        (of a)) =
    of a
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.WithTerminal.FinCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
a : WithInitial C
of :
  ∀ (a : C),
    (fun (x : Option C) ↦
          (match (motive := Option C → WithInitial C) x with
            | some a => WithInitial.of a
            | none => star :
            WithInitial C))
        ((fun (x : WithInitial C) ↦
            (match (motive := WithInitial C → Option C) x with
              | WithInitial.of a => some a
              | star => none :
              Option C))
          (WithInitial.of a)) =
      WithInitial.of a
⊢ (fun (x : Option C) ↦
        (match (motive := Option C → WithInitial C) x with
          | some a => WithInitial.of a
          | none => star :
          WithInitial C))
      ((fun (x : WithInitial C) ↦
          (match (motive := WithInitial C → Option C) x with
            | WithInitial.of a => some a
            | star => none :
            Option C))
        a) =
    a
have star : Eq.{u + 1} (α := WithInitial C)
  ((fun (x : Option C) ↦
      (match (motive := Option C → WithInitial C) x with
        | some a => WithInitial.of a
        | none => star :
        WithInitial C))
    ((fun (x : WithInitial C) ↦
        (match (motive := WithInitial C → Option C) x with
          | WithInitial.of a => some a
          | star => none :
          Option C))
      star))
  star
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : C
f : Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (obj yoneda Z) (obj yoneda W)
⊢ map yoneda
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj Z).obj (op Z))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj W).obj (op Z)))
        (𝟙 (unop (op Z)))) =
    f
have w : ∀ (X : Cᵒᵖ) (x : obj (obj yoneda Z) X),
  TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app
          (map yoneda
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z)) :
                (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj Z).obj (op Z))) →
                  (fun (X : Type v₁) ↦ X) ((yoneda.obj W).obj (op Z)))
              (𝟙 (unop (op Z)))))
          X))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : C
f : Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (obj yoneda Z) (obj yoneda W)
X : Cᵒᵖ
x : obj (obj yoneda Z) X
⊢ TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app
          (map yoneda
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z)) :
                (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj Z).obj (op Z))) →
                  (fun (X : Type v₁) ↦ X) ((yoneda.obj W).obj (op Z)))
              (𝟙 (unop (op Z)))))
          X))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x
have this : Eq (α := obj (obj yoneda W) (op (unop X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
        (a : (yoneda.obj Z).obj (op (unop X))) → (yoneda.obj W).obj (op (unop X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj yoneda Z) (Quiver.Hom.op x)) :
            (a : (yoneda.obj Z).obj (op Z)) → (yoneda.obj Z).obj (op (unop X)))
          (𝟙 Z) :
        obj (obj yoneda Z) (op (unop X))) :
    obj (obj yoneda W) (op (unop X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj yoneda W) (Quiver.Hom.op x)) :
        (a : (yoneda.obj W).obj (op Z)) → (yoneda.obj W).obj (op (unop X)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Z)) :
            (a : (yoneda.obj Z).obj (op Z)) → (yoneda.obj W).obj (op Z))
          (𝟙 Z) :
        obj (obj yoneda W) (op Z)) :
    obj (obj yoneda W) (op (unop X)))
Tactic: have := f.naturality_apply x.op (𝟙 Z)
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : Quiver.Hom (V := C ⥤ Type v₁) (obj coyoneda Z) (obj coyoneda W)
⊢ map coyoneda
      (Quiver.Hom.op
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop Z)) :
            (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj Z).obj (unop Z))) →
              (fun (X : Type v₁) ↦ X) ((coyoneda.obj W).obj (unop Z)))
          (𝟙 (unop Z)))) =
    f
have w : ∀ (X : C) (x : obj (obj coyoneda Z) X),
  TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app
          (map coyoneda
            (Quiver.Hom.op
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop Z)) :
                  (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj Z).obj (unop Z))) →
                    (fun (X : Type v₁) ↦ X) ((coyoneda.obj W).obj (unop Z)))
                (𝟙 (unop Z)))))
          X))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : Quiver.Hom (V := C ⥤ Type v₁) (obj coyoneda Z) (obj coyoneda W)
X : C
x : obj (obj coyoneda Z) X
⊢ TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (NatTrans.app
          (map coyoneda
            (Quiver.Hom.op
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop Z)) :
                  (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj Z).obj (unop Z))) →
                    (fun (X : Type v₁) ↦ X) ((coyoneda.obj W).obj (unop Z)))
                (𝟙 (unop Z)))))
          X))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x
have this : Eq (α := obj (obj coyoneda W) X)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : (coyoneda.obj Z).obj X) → (coyoneda.obj W).obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj coyoneda Z) x) :
            (a : (coyoneda.obj Z).obj (unop Z)) → (coyoneda.obj Z).obj X)
          (𝟙 (unop Z)) :
        obj (obj coyoneda Z) X) :
    obj (obj coyoneda W) X)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj coyoneda W) x) :
        (a : (coyoneda.obj W).obj (unop Z)) → (coyoneda.obj W).obj X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop Z)) :
            (a : (coyoneda.obj Z).obj (unop Z)) → (coyoneda.obj W).obj (unop Z))
          (𝟙 (unop Z)) :
        obj (obj coyoneda W) (unop Z)) :
    obj (obj coyoneda W) X)
Tactic: have := f.naturality_apply x (𝟙 (unop Z))
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F F' : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ Eq.{v + 1} (α := F'.obj (op X))
    (((Equiv.trans e.homEquiv (Iso.toEquiv (e'.app (op X))) : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F'.obj (op X))) :
          (a : X ⟶ Y) → F'.obj (op X))
        (f ≫ g) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) :
          (a : (fun (X : Type v) ↦ X) (F'.obj (op X'))) → (fun (X : Type v) ↦ X) (F'.obj (op X)))
        (((Equiv.trans e.homEquiv (Iso.toEquiv (e'.app (op X'))) : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F'.obj (op X'))) :
              (a : X' ⟶ Y) → F'.obj (op X'))
            g :
          F'.obj (op X')) :
      (fun (X : Type v) ↦ X) (F'.obj (op X)))
have dsimp : Eq (α := F'.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X)) : (a : F.obj (op X)) → F'.obj (op X))
      (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) :
        F.obj (op X)) :
    F'.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) : (a : F'.obj (op X')) → F'.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X')) : (a : F.obj (op X')) → F'.obj (op X'))
          (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
            F.obj (op X')) :
        F'.obj (op X')) :
    F'.obj (op X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F F' : Functor.{v₁, v, u₁, v + 1} Cᵒᵖ (Type v)
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ Eq (α := F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X)) : (a : F.obj (op X)) → F'.obj (op X))
        (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X ⟶ Y) (F.obj (op X))) : (a : X ⟶ Y) → F.obj (op X)) (f ≫ g) :
          F.obj (op X)) :
      F'.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) : (a : F'.obj (op X')) → F'.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X')) : (a : F.obj (op X')) → F'.obj (op X'))
            (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
              F.obj (op X')) :
          F'.obj (op X')) :
      F'.obj (op X))
have rw : Eq (α := F'.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X)) : (a : F.obj (op X)) → F'.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op X'))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
          (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
            F.obj (op X')) :
        (fun (X : Type v) ↦ X) (F.obj (op X))) :
    F'.obj (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f.op) : (a : F'.obj (op X')) → F'.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e'.hom.app (op X')) : (a : F.obj (op X')) → F'.obj (op X'))
          (((e.homEquiv : Equiv.{v₁ + 1, v + 1} (X' ⟶ Y) (F.obj (op X'))) : (a : X' ⟶ Y) → F.obj (op X')) g :
            F.obj (op X')) :
        F'.obj (op X')) :
    F'.obj (op X))
Tactic: rw [e.homEquiv_comp]