awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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 E
inst_3 : F.Faithful
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ Faithful.div F G obj h_obj @map @h_map ⋙ G = F
have obtain : ∀ (F_obj : C → E) (map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)) (map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X))
  (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g)
  [{ obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful]
  (h_obj :
    ∀ (X : C),
      G.obj (obj X) =
        { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X)
  (h_map :
    ∀ {X Y : C} {f : X ⟶ Y},
      G.map (map f) ≍
        { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f),
  Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E } G
        obj h_obj @map @h_map ⋙
      G =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }
Tactic: obtain ⟨F_obj, _, _, _⟩ := F
Cleared hypotheses: F, inst_3, h_obj, h_map
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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 : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.Faithful
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_4 :
  { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
h_obj :
  ∀ (X : C),
    G.obj (obj X) =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    G.map (map f) ≍
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f
⊢ Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E } G
        obj h_obj @map @h_map ⋙
      G =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }
have obtain : ∀ (G_obj : D → E) (map_2 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)) (map_id_1 : ∀ (X : D), map_2 (𝟙 X) = 𝟙 (G_obj X))
  (map_comp_1 : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g)
  [inst_5 :
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
        Functor.{v₂, v₃, u₂, u₃} D E }.Faithful]
  (h_obj :
    ∀ (X : C),
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
          (obj X) =
        { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X)
  (h_map :
    ∀ {X Y : C} {f : X ⟶ Y},
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.map
          (map f) ≍
        { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f),
  Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E } obj
        h_obj @map @h_map ⋙
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E } =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }
Tactic: obtain ⟨G_obj, _, _, _⟩ := G
Cleared hypotheses: G, inst_3, h_obj, h_map
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_3 :
  { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
G_obj : D → E
map_2 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 : ∀ (X : D), map_2 (𝟙 X) = 𝟙 (G_obj X)
map_comp_1 : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g
inst_4 :
  { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        (obj X) =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.map
        (map f) ≍
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f
⊢ Faithful.div { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E } obj
        h_obj @map @h_map ⋙
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E } =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }
have unfold : {
    obj := fun (X : C) ↦
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        ({ obj := obj, map := @map, map_id := sorry, map_comp := sorry : Functor.{v₁, v₂, u₁, u₂} C D }.obj X),
    map := fun {X Y : C} (f : X ⟶ Y) ↦
      { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 }.map
        ({ obj := obj, map := @map, map_id := sorry, map_comp := sorry }.map f),
    map_id := sorry, map_comp := sorry } =
  { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
Tactic: unfold Faithful.div Functor.comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (hypothesis)
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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_3 :
  { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
G_obj : D → E
map_2 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 : ∀ (X : D), map_2 (𝟙 X) = 𝟙 (G_obj X)
map_comp_1 : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g
inst_4 :
  { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        (obj X) =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.map
        (map f) ≍
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f
⊢ {
      obj := fun (X : C) ↦
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.obj X),
      map := fun {X Y : C} (f : X ⟶ Y) ↦
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 }.map
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ }.map f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
have this : F_obj = G_obj ∘ obj
Tactic: have : F_obj = G_obj ∘ obj := (funext h_obj).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map_1 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id : ∀ (X : D), map_1 (𝟙 X) = 𝟙 (G_obj X)
map_comp : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_3 :
  { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.Faithful
map_2 : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id_1 : ∀ (X : C), map_2 (𝟙 X) = 𝟙 ((G_obj ∘ obj) X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g
inst_4 :
  { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
      Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        (obj X) =
      { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
            Functor.{v₁, v₃, u₁, u₃} C E }.obj
        X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.map
        (map f) ≍
      { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
            Functor.{v₁, v₃, u₁, u₃} C E }.map
        f
⊢ {
      obj := fun (X : C) ↦
        { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.obj
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.obj X),
      map := fun {X Y : C} (f : X ⟶ Y) ↦
        { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }.map
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ }.map f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₁, v₃, u₁, u₃} C E }
have e_map : (fun {X Y : C} (f : X ⟶ Y) ↦
    { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }.map
      ({ obj := obj, map := @map, map_id := sorry, map_comp := sorry }.map f)) =
  @map_2
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (hypothesis)
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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map_1 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id : ∀ (X : D), map_1 (𝟙 X) = 𝟙 (G_obj X)
map_comp : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_3 :
  { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.Faithful
map_2 : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id_1 : ∀ (X : C), map_2 (𝟙 X) = 𝟙 ((G_obj ∘ obj) X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g
inst_4 :
  { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
      Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        (obj X) =
      { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
            Functor.{v₁, v₃, u₁, u₃} C E }.obj
        X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.map
        (map f) ≍
      { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
            Functor.{v₁, v₃, u₁, u₃} C E }.map
        f
⊢ (fun {X Y : C} (f : X ⟶ Y) ↦
      { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }.map
        ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ }.map f)) =
    @map_2
have h_map₁ : ∀ {X Y : C} {f : X ⟶ Y}, map_1 (map f) = map_2 f
Tactic: simp only [Function.comp_apply, heq_eq_eq] at h_map
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map_1 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id : ∀ (X : D), map_1 (𝟙 X) = 𝟙 (G_obj X)
map_comp : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_3 :
  { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.Faithful
map_2 : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id_1 : ∀ (X : C), map_2 (𝟙 X) = 𝟙 ((G_obj ∘ obj) X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g
inst_4 :
  { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
      Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        (obj X) =
      { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
            Functor.{v₁, v₃, u₁, u₃} C E }.obj
        X
h_map_1 :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.map
        (map f) ≍
      { obj := G_obj ∘ obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
            Functor.{v₁, v₃, u₁, u₃} C E }.map
        f
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map_1 (map f) = map_2 f
⊢ (fun {X Y : C} (f : X ⟶ Y) ↦
      { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp }.map
        ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ }.map f)) =
    @map_2
have e_map : ∀ (x x_1 : C) (x_2 : x ⟶ x_1),
  { obj := G_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₂, v₃, u₂, u₃} D E }.map
      ({ obj := obj, map := @map, map_id := sorry, map_comp := sorry : Functor.{v₁, v₂, u₁, u₂} C D }.map x_2) =
    map_2 x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (hypothesis)
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 : Functor.{v₂, v₃, u₂, u₃} D E
H : Functor.{v₁, v₃, u₁, u₃} C E
inst_3 : H.Full
inst_4 : G.Faithful
h : F ⋙ G ≅ H
⊢ F.Full
have this : (F ⋙ G).Full
Tactic: have := Full.of_iso h.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 G_1 : Functor.{v, v', u, u'} C D
F G A : Functor.{v, w, u, w + 1} C (Type w)
a : F.HomObj G A
X Y : C
f : X ⟶ Y
⊢ (tensorObj (𝒞 := category) F A).map f ≫
      (fun (X : C) ↦
          (↾fun (x : (tensorObj (𝒞 := category) F A).obj X) ↦
              match (motive := (tensorObj (𝒞 := category) F A).obj X → G.obj X) x with
              | (x, y) =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X y) :
                    (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                  x :
            (tensorObj (𝒞 := category) F A).obj X ⟶ G.obj X))
        Y =
    (fun (X : C) ↦
          (↾fun (x : (tensorObj (𝒞 := category) F A).obj X) ↦
              match (motive := (tensorObj (𝒞 := category) F A).obj X → G.obj X) x with
              | (x, y) =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X y) :
                    (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                  x :
            (tensorObj (𝒞 := category) F A).obj X ⟶ G.obj X))
        X ≫
      G.map f
have h : ∀ (x : F.obj X) (y : A.obj X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((tensorObj (𝒞 := category) F A).map f ≫
          (fun (X : C) ↦
              (↾fun (x : (tensorObj (𝒞 := category) F A).obj X) ↦
                  match (motive := (tensorObj (𝒞 := category) F A).obj X → G.obj X) x with
                  | (x, y) =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X y) :
                        (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                      x :
                (tensorObj (𝒞 := category) F A).obj X ⟶ G.obj X))
            Y))
      (x, y) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : C) ↦
              (↾fun (x : (tensorObj (𝒞 := category) F A).obj X) ↦
                  match (motive := (tensorObj (𝒞 := category) F A).obj X → G.obj X) x with
                  | (x, y) =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X y) :
                        (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                      x :
                (tensorObj (𝒞 := category) F A).obj X ⟶ G.obj X))
            X ≫
          G.map f))
      (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 G_1 : Functor.{v, v', u, u'} C D
F G A : Functor.{v, w, u, w + 1} C (Type w)
a : tensorObj (𝒞 := category) F A ⟶ G
c d : C
φ : c ⟶ d
y : A.obj c
⊢ F.map φ ≫
      (fun (X : C) (y : A.obj X) ↦
          (↾fun (x : F.obj X) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) :
                  (a : (fun (X : Type w) ↦ X) ((F ⊗ A).obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                (x, y) :
            F.obj X ⟶ G.obj X))
        d
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) :
            (a : (fun (X : Type w) ↦ X) (A.obj c)) → (fun (X : Type w) ↦ X) (A.obj d))
          y) =
    (fun (X : C) (y : A.obj X) ↦
          (↾fun (x : F.obj X) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) :
                  (a : (fun (X : Type w) ↦ X) ((F ⊗ A).obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                (x, y) :
            F.obj X ⟶ G.obj X))
        c y ≫
      G.map φ
have h : ∀ (x : F.obj c),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (F.map φ ≫
          (fun (X : C) (y : A.obj X) ↦
              (↾fun (x : F.obj X) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) :
                      (a : (fun (X : Type w) ↦ X) ((F ⊗ A).obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                    (x, y) :
                F.obj X ⟶ G.obj X))
            d
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) :
                (a : (fun (X : Type w) ↦ X) (A.obj c)) → (fun (X : Type w) ↦ X) (A.obj d))
              y)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : C) (y : A.obj X) ↦
              (↾fun (x : F.obj X) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) :
                      (a : (fun (X : Type w) ↦ X) ((F ⊗ A).obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                    (x, y) :
                F.obj X ⟶ G.obj X))
            c y ≫
          G.map φ))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A : Functor.{v, w, u, w + 1} C (Type w)
f g : F.HomObj G A
h : f = g
X : C
a : A.obj X
⊢ f.app X a = g.app X a
have subst : f.app X a = f.app X a
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A A' : Functor.{v, w, u, w + 1} C (Type w)
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
⊢ F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ') :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ')) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A'.map φ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A'.obj Δ'))
              a :
            (fun (X : Type w) ↦ X) (A'.obj Δ'))) =
    x.app Δ
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
          a) ≫
      G.map φ
have rw : F.map φ ≫
    x.app Δ'
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ') :
          (a : (fun (X : Type w) ↦ X) (A'.obj Δ')) → (fun (X : Type w) ↦ X) (A.obj Δ'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A'.map φ) :
              (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A'.obj Δ'))
            a :
          (fun (X : Type w) ↦ X) (A'.obj Δ'))) =
  F.map φ ≫
    x.app Δ'
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) :
          (a : (fun (X : Type w) ↦ X) (A.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
              (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
            a :
          (fun (X : Type w) ↦ X) (A.obj Δ)))
Tactic: rw [← x.naturality φ (f.app Δ a), f.naturality_apply φ a]