awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
⊢ F_obj = G_obj ∘ obj

Tactic:
have : F_obj = G_obj ∘ obj := (funext h_obj).symm
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
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 := ⋯, map_comp := ⋯ }.map f)) =
    @map_2
⊢ {
      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 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
⊢ ∀ {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

Premises used: heq_eq_eq, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
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 := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.map x_2) =
      map_2 x_2
⊢ (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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
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 := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.map x_2) =
    map_2 x_2

Tactic:
h_map
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
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 := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.map x_2) =
    map_2 x_2

Tactic:
exact h_map
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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).Faithful

Tactic:
(Faithful.div_comp F G _ h_obj _ @h_map).faithful_of_comp

Premises used: Eq.faithful_of_comp, CategoryTheory.Functor.Faithful.div_comp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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 F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : G.Full
X Y : C
f : (F ⋙ G).obj X ⟶ (F ⋙ G).obj Y
⊢ (F ⋙ G).map (F.preimage (G.preimage f)) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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 ⋙ G).Full

Tactic:
have := Full.of_iso h.symm
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
this : (F ⋙ G).Full
⊢ F.Full

Tactic:
Full.of_comp_faithful F G

Premises used: CategoryTheory.Functor.Full.of_comp_faithful
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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
this : (F ⋙ G).Full
⊢ F.Full

Tactic:
exact Full.of_comp_faithful F G

Premises used: CategoryTheory.Functor.Full.of_comp_faithful
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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_1 F' : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : H.Full
inst_4 : H.Faithful
comp_iso : F ⋙ H ≅ G ⋙ H
X Y : C
f : X ⟶ Y
⊢ H.map (F.map f ≫ Iso.hom ((fun (X : C) ↦ H.preimageIso (comp_iso.app X)) Y)) =
    H.map (Iso.hom ((fun (X : C) ↦ H.preimageIso (comp_iso.app X)) X) ≫ G.map f)

Tactic:
simpa using comp_iso.hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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 : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : H.Full
inst_4 : H.Faithful
comp_iso : F ⋙ H ≅ G ⋙ H
X : C
⊢ (fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)

Tactic:
rfl

Premises used: CategoryTheory.Functor.preimage, Classical.choose, rfl
-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
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 : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : H.Full
inst_4 : H.Faithful
comp_iso : F ⋙ H ≅ G ⋙ H
X : C
⊢ (fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)

Tactic:
rfl

Premises used: CategoryTheory.Functor.preimage, Classical.choose, rfl
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
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
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)
⊢ (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

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
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
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:
simpa using ConcreteCategory.congr_hom (a.naturality f y) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.HomObj.naturality
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
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
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
⊢ 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 φ

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
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
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:
simpa using (a.naturality_apply φ) (x, y)

Premises used: CategoryTheory.NatTrans.naturality_apply, Prod.mk
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
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)
x : F.HomObj G A
⊢ (fun (a : tensorObj (𝒞 := category) F A ⟶ G) ↦
        ({
            app := 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),
            naturality := ⋯ } :
          F.HomObj G A))
      ((fun (a : F.HomObj G A) ↦
          ({
              app := 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,
              naturality := ⋯ } :
            NatTrans (tensorObj (𝒞 := category) F A) G))
        x) =
    x

Tactic:
aesop