awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B
e_a :
  (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ =
    (ShiftedHom.opEquiv 1 :
        (a :
            ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
              (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
          ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
            (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
      T.mor₃
⊢ Eq (α :=
    ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
      (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
    ((ShiftedHom.opEquiv 1 :
          (a :
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
        ((Equiv.symm (ShiftedHom.opEquiv 1) :
              (a :
                  ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
                    (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1) →
                ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                  (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1)
            (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ :
          ShiftedHom (M := ℤ) (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)
            (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃) 1) :
      ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
        (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
    ((ShiftedHom.opEquiv 1 :
          (a :
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
        T.mor₃ :
      ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
        (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)

Tactic:
rw [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Triangulated.Yoneda
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B
⊢ (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ =
    (ShiftedHom.opEquiv 1 :
        (a :
            ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
              (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
          ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
            (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
      T.mor₃

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u_1
Y : Type u_2
x : Fun X Y
⊢ ∀ ⦃a₂ : Fun X Y⦄,
    Eq (α := (a : X) → Y) ((fun (f : Fun X Y) (x : X) ↦ f.toFun x) x) ((fun (f : Fun X Y) (x : X) ↦ f.toFun x) a₂) →
      x = a₂

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
x : X
⊢ ({ toFun := f : Fun X Y } : (a : X) → Y) x = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
⊢ (⇑{ toFun := f : Fun X Y } : (a : X) → Y) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
x : Fun X Y
⊢ (fun (f : X → Y) ↦ { toFun := f : Fun X Y }) ((fun (f : Fun X Y) ↦ ((⇑f : (a : X) → Y) : (a : X) → Y)) x) = x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
x : X → Y
⊢ (fun (f : Fun X Y) ↦ ((⇑f : (a : X) → Y) : (a : X) → Y)) ((fun (f : X → Y) ↦ { toFun := f : Fun X Y }) x) = x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ Eq (α := (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := Fun) f) : (a : X) → Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ Eq (α := (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := Fun) f) : (a : X) → Y)

Tactic:
with_reducible rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
x : X
⊢ Eq (α := (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
      (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
      (fun (X : Type u) ↦ X) Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
x : X
⊢ Eq (α := (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
      (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
      (fun (X : Type u) ↦ X) Y)

Tactic:
with_reducible rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u_1
Y : Type u_2
f : Fun X Y
⊢ Eq (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑f : (a : X) → Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u_1
Y : Type u_2
f : Fun X Y
⊢ Eq (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑f : (a : X) → Y)

Tactic:
with_reducible rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u_1
Y : Type u_2
f : Fun X Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u_1
Y : Type u_2
f : Fun X Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((f : (a : X) → Y) x : Y) ((f : (a : X) → Y) x : Y)

Tactic:
with_reducible rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : Fun X Y
x : X
⊢ f.toFun x = (f : (a : X) → Y) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u
⊢ ToType (FC := Fun) X = X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u
⊢ ToType (FC := Fun) X = X

Tactic:
with_reducible rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ ↾(⇑(ConcreteCategory.hom (FC := Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
⊢ Hom.hom (↾f) = { toFun := f }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ ↾(⇑(Hom.hom f) : (a : X) → Y) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
x : X
⊢ (ConcreteCategory.hom (FC := Fun) (↾f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ Eq (α := X → Y) ((homEquiv : (a : X ⟶ Y) → X → Y) f : X → Y)
    ((⇑(ConcreteCategory.hom (FC := Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) :
      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
⊢ (Equiv.symm homEquiv : (a : X → Y) → X ⟶ Y) f = ↾f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
x x' : X
h : x = x'
rw rw₁ :
  Eq (α := (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' :
      (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' :
      (fun (X : Type u) ↦ X) Y)
⊢ Eq (α := (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
      (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x' :
      (fun (X : Type u) ↦ X) Y)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u
⊢ Eq (α := (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X)
    (⇑(ConcreteCategory.hom (FC := Fun) (𝟙 X)) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : X) → Z) (⇑(ConcreteCategory.hom (FC := Fun) (f ≫ g)) : (a : X) → Z)
    (Function.comp (β := (fun (X : Type u) ↦ X) Y)
      (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      (⇑(ConcreteCategory.hom (FC := Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u
x : X
⊢ (ConcreteCategory.hom (FC := Fun) (𝟙 X) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
x : X
⊢ Eq (α := (fun (X : Type u) ↦ X) Z)
    ((ConcreteCategory.hom (FC := Fun) (f ≫ g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) x :
      (fun (X : Type u) ↦ X) Z)
    ((ConcreteCategory.hom (FC := Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
          (fun (X : Type u) ↦ X) Y) :
      (fun (X : Type u) ↦ X) Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f g : X ⟶ Y
h : f = g
x : X
⊢ Eq (α := (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
      (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
      (fun (X : Type u) ↦ X) Y)

Tactic:
ConcreteCategory.congr_hom h x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w, u, w + 1} J (Type w)
s : (↑F.sections : Type (max u w))
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (FC := Fun) (F.map f) :
        (a : (fun (X : Type w) ↦ X) (F.obj j)) → (fun (X : Type w) ↦ X) (F.obj j'))
      ((↑s : (j : J) → F.obj j) j) =
    (↑s : (j : J) → F.obj j) j'

Tactic:
s.property f

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w, u, w + 1} J (Type w)
x y : (↑F.sections : Type (max u w))
⊢ x = y ↔ ∀ (j : J), (↑x : (j : J) → F.obj j) j = (↑y : (j : J) → F.obj j) j

Tactic:
Subtype.ext_iff.trans funext_iff

Premises used: funext_iff, Subtype.ext_iff, Iff.trans
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
J : Type u
inst : Category.{v, u} J
F G : Functor.{v, w, u, w + 1} J (Type w)
φ : F ⟶ G
x : (↑F.sections : Type (max u w))
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.obj j'))
    ((ConcreteCategory.hom (FC := Fun) (G.map f) :
          (a : (fun (X : Type w) ↦ X) (G.obj j)) → (fun (X : Type w) ↦ X) (G.obj j'))
        ((fun (j : J) ↦
            ((ConcreteCategory.hom (FC := Fun) (φ.app j) :
                  (a : (fun (X : Type w) ↦ X) (F.obj j)) → (fun (X : Type w) ↦ X) (G.obj j))
                ((↑x : (j : J) → F.obj j) j) :
              (fun (X : Type w) ↦ X) (G.obj j)))
          j) :
      (fun (X : Type w) ↦ X) (G.obj j'))
    ((fun (j : J) ↦
          ((ConcreteCategory.hom (FC := Fun) (φ.app j) :
                (a : (fun (X : Type w) ↦ X) (F.obj j)) → (fun (X : Type w) ↦ X) (G.obj j))
              ((↑x : (j : J) → F.obj j) j) :
            (fun (X : Type w) ↦ X) (G.obj j)))
        j' :
      (fun (X : Type w) ↦ X) (G.obj j'))

Tactic:
simp [← NatTrans.naturality_apply, x.2 f]

Premises used: CategoryTheory.NatTrans.naturality_apply, Subtype.property
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
a : F.obj X
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj Z))
    ((ConcreteCategory.hom (FC := Fun) (F.map (f ≫ g)) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Z))
        a :
      (fun (X : Type w) ↦ X) (F.obj Z))
    ((ConcreteCategory.hom (FC := Fun) (F.map g) :
          (a : (fun (X : Type w) ↦ X) (F.obj Y)) → (fun (X : Type w) ↦ X) (F.obj Z))
        ((ConcreteCategory.hom (FC := Fun) (F.map f) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj Y))
            a :
          (fun (X : Type w) ↦ X) (F.obj Y)) :
      (fun (X : Type w) ↦ X) (F.obj Z))

Tactic:
F.map_comp_apply f g a

Premises used: CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : C
a : F.obj X
⊢ (ConcreteCategory.hom (FC := Fun) (F.map (𝟙 X)) :
        (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (F.obj X))
      a =
    a

Tactic:
F.map_id_apply X a

Premises used: CategoryTheory.Functor.map_id_apply
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F G H : Functor.{v, w, u, w + 1} C (Type w)
X : C
σ : F ⟶ G
τ : G ⟶ H
x : F.obj X
⊢ Eq (α := (fun (X : Type w) ↦ X) (H.obj X))
    ((ConcreteCategory.hom (FC := Fun) ((σ ≫ τ).app X) :
          (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (H.obj X))
        x :
      (fun (X : Type w) ↦ X) (H.obj X))
    ((ConcreteCategory.hom (FC := Fun) (τ.app X) :
          (a : (fun (X : Type w) ↦ X) (G.obj X)) → (fun (X : Type w) ↦ X) (H.obj X))
        ((ConcreteCategory.hom (FC := Fun) (σ.app X) :
              (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
            x :
          (fun (X : Type w) ↦ X) (G.obj X)) :
      (fun (X : Type w) ↦ X) (H.obj X))

Tactic:
σ.comp_app_apply τ X x

Premises used: CategoryTheory.NatTrans.comp_app_apply
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
σ : F ⟶ G
D : Type u'
𝒟 : Category.{u', u'} D
I J : Functor.{u', v, u', u} D C
ρ : I ⟶ J
W : D
x : (I ⋙ F).obj W
⊢ Eq (α := (fun (X : Type w) ↦ X) ((J ⋙ G).obj W))
    ((ConcreteCategory.hom (FC := Fun) ((ρ ◫ σ).app W) :
          (a : (fun (X : Type w) ↦ X) ((I ⋙ F).obj W)) → (fun (X : Type w) ↦ X) ((J ⋙ G).obj W))
        x :
      (fun (X : Type w) ↦ X) ((J ⋙ G).obj W))
    ((ConcreteCategory.hom (FC := Fun) (G.map (ρ.app W)) :
          (a : (fun (X : Type w) ↦ X) (G.obj (I.obj W))) → (fun (X : Type w) ↦ X) (G.obj (J.obj W)))
        ((ConcreteCategory.hom (FC := Fun) (σ.app (I.obj W)) :
              (a : (fun (X : Type w) ↦ X) (F.obj (I.obj W))) → (fun (X : Type w) ↦ X) (G.obj (I.obj W)))
            x :
          (fun (X : Type w) ↦ X) (G.obj (I.obj W))) :
      (fun (X : Type w) ↦ X) (G.obj (J.obj W)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
G : Functor.{v, u_2, u, u_2 + 1} C (Type u_2)
e : (j : C) → Equiv.{u_1 + 1, u_2 + 1} (F.obj j) (G.obj j)
naturality :
  ∀ {j j' : C} (f : j ⟶ j'),
    Eq (α := (fun (X : Type u_1) ↦ X) (F.obj j) → G.obj j')
      (Function.comp (β := F.obj j') (⇑(e j') : (a : F.obj j') → G.obj j')
        (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j')))
      (Function.comp (β := (fun (X : Type u_2) ↦ X) (G.obj j))
        (⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
          (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
        (⇑(e j) : (a : F.obj j) → G.obj j))
j j' : C
f : j ⟶ j'
h :
  ∀ (x : (fun (X : Type u_2) ↦ X) (G.obj j)),
    Eq (α := F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j').symm : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
          (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
        x)
      (Function.comp (β := (fun (X : Type u_1) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j'))
        (⇑(e j).symm : (a : G.obj j) → F.obj j) x)
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (G.obj j) → F.obj j')
    (Function.comp (β := G.obj j') (⇑(e j').symm : (a : G.obj j') → F.obj j')
      (⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
        (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j')))
    (Function.comp (β := (fun (X : Type u_1) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
        (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j'))
      (⇑(e j).symm : (a : G.obj j) → F.obj j))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
G : Functor.{v, u_2, u, u_2 + 1} C (Type u_2)
e : (j : C) → Equiv.{u_1 + 1, u_2 + 1} (F.obj j) (G.obj j)
naturality :
  ∀ {j j' : C} (f : j ⟶ j'),
    Eq (α := (fun (X : Type u_1) ↦ X) (F.obj j) → G.obj j')
      (Function.comp (β := F.obj j') (⇑(e j') : (a : F.obj j') → G.obj j')
        (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j')))
      (Function.comp (β := (fun (X : Type u_2) ↦ X) (G.obj j))
        (⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
          (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
        (⇑(e j) : (a : F.obj j) → G.obj j))
j j' : C
f : j ⟶ j'
x : (fun (X : Type u_2) ↦ X) (G.obj j)
h :
  ∀ (y : F.obj j),
    Eq (α := F.obj j')
      (Function.comp (α := (fun (X : Type u_2) ↦ X) (G.obj j)) (β := G.obj j')
        (⇑(e j').symm : (a : G.obj j') → F.obj j')
        ((⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
            (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j')) :
          (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
        ((e j : (a : F.obj j) → G.obj j) y : G.obj j))
      (Function.comp.{u_2 + 1, u_1 + 1, u_1 + 1} (α := G.obj j) (β := (fun (X : Type u_1) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j'))
        ((⇑(e j).symm : (a : G.obj j) → F.obj j) : (a : G.obj j) → F.obj j)
        ((e j : (a : F.obj j) → G.obj j) y : G.obj j))
⊢ Eq (α := F.obj j')
    (Function.comp (β := G.obj j') (⇑(e j').symm : (a : G.obj j') → F.obj j')
      (⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
        (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
      x)
    (Function.comp (β := (fun (X : Type u_1) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
        (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j'))
      (⇑(e j).symm : (a : G.obj j) → F.obj j) x)

Tactic:
obtain ⟨y, rfl⟩ := (e j).surjective x

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
G : Functor.{v, u_2, u, u_2 + 1} C (Type u_2)
e : (j : C) → Equiv.{u_1 + 1, u_2 + 1} (F.obj j) (G.obj j)
naturality :
  ∀ {j j' : C} (f : j ⟶ j'),
    Eq (α := (fun (X : Type u_1) ↦ X) (F.obj j) → G.obj j')
      (Function.comp (β := F.obj j') (⇑(e j') : (a : F.obj j') → G.obj j')
        (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j')))
      (Function.comp (β := (fun (X : Type u_2) ↦ X) (G.obj j))
        (⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
          (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
        (⇑(e j) : (a : F.obj j) → G.obj j))
j j' : C
f : j ⟶ j'
y : F.obj j
h :
  Eq.{u_2 + 1} (α := G.obj j')
    ((e j' : (a : F.obj j') → G.obj j')
        (Function.comp (α := (fun (X : Type u_2) ↦ X) (G.obj j)) (β := G.obj j')
          (⇑(e j').symm : (a : G.obj j') → F.obj j')
          ((⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
              (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j')) :
            (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
          ((e j : (a : F.obj j) → G.obj j) y : G.obj j)) :
      G.obj j')
    ((e j' : (a : F.obj j') → G.obj j')
        (Function.comp.{u_2 + 1, u_1 + 1, u_1 + 1} (α := G.obj j) (β := (fun (X : Type u_1) ↦ X) (F.obj j))
          (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
            (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j'))
          ((⇑(e j).symm : (a : G.obj j) → F.obj j) : (a : G.obj j) → F.obj j)
          ((e j : (a : F.obj j) → G.obj j) y : G.obj j)) :
      G.obj j')
⊢ Eq (α := F.obj j')
    (Function.comp (α := (fun (X : Type u_2) ↦ X) (G.obj j)) (β := G.obj j') (⇑(e j').symm : (a : G.obj j') → F.obj j')
      ((⇑(ConcreteCategory.hom (FC := Fun) (G.map f)) :
          (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j')) :
        (a : (fun (X : Type u_2) ↦ X) (G.obj j)) → (fun (X : Type u_2) ↦ X) (G.obj j'))
      ((e j : (a : F.obj j) → G.obj j) y : G.obj j))
    (Function.comp.{u_2 + 1, u_1 + 1, u_1 + 1} (α := G.obj j) (β := (fun (X : Type u_1) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := Fun) (F.map f)) :
        (a : (fun (X : Type u_1) ↦ X) (F.obj j)) → (fun (X : Type u_1) ↦ X) (F.obj j'))
      ((⇑(e j).symm : (a : G.obj j) → F.obj j) : (a : G.obj j) → F.obj j) ((e j : (a : F.obj j) → G.obj j) y : G.obj j))

Tactic:
apply (e j').injective

Premises used: Equiv.injective