awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
X : FintypeCat
x : (uSwitch.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
    (((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
              (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
              _ _ _
              (uSwitch.map
                    (NatTrans.app
                      (Iso.hom
                        (NatIso.ofComponents
                          (fun (X : FintypeCat.{u}) ↦
                            Iso.symm
                              ((equivEquivIso :
                                  (a : (uSwitch.obj (uSwitch.obj X)).obj ≃ X.obj) → uSwitch.obj (uSwitch.obj X) ≅ X)
                                (Equiv.trans (uSwitch.obj X).uSwitchEquiv X.uSwitchEquiv)))
                          @uSwitchEquivalence._proof_2))
                      X) ≫
                  (NatIso.ofComponents
                          (fun (X : FintypeCat.{v}) ↦
                            (equivEquivIso :
                                (a : ((uSwitch ⋙ uSwitch).obj X).obj ≃ ((𝟭 FintypeCat).obj X).obj) →
                                  (uSwitch ⋙ uSwitch).obj X ≅ (𝟭 FintypeCat).obj X)
                              (Equiv.trans (uSwitch.obj X).uSwitchEquiv X.uSwitchEquiv))
                          @uSwitchEquivalence._proof_3).hom.app
                    (uSwitch.obj X) :
                uSwitch.obj X ⟶ uSwitch.obj X) :
            TypeCat.Fun (uSwitch.obj X).obj (uSwitch.obj X).obj) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (𝟙 (uSwitch.obj X) : uSwitch.obj X ⟶ uSwitch.obj X) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (uSwitch.obj X))

Tactic:
simp [← uSwitchEquiv_naturality]

Premises used: FintypeCat.uSwitchEquiv_naturality
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
⊢ uSwitch.IsEquivalence

Tactic:
uSwitchEquivalence.isEquivalence_functor

Premises used: FintypeCat.uSwitchEquivalence, FintypeCat.uSwitch, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.CategoryTheory.FintypeCat
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w, u, w + 1} C FintypeCat
X Y : C
σ : F ⟶ G
f : X ⟶ Y
x : (F.obj X).obj
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj Y))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (σ.app Y) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj Y))
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (F.map f) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y))
            x :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj Y)) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj Y))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (G.map f) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X)) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj Y))
        ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
                (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                  (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
                _ _ _ (σ.app X) :
              (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj X)) →
                (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X))
            x :
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj X)) :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (G.obj Y))

Tactic:
(σ.naturality_apply f) x

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v_1, u₁} C
D : Type u₂
inst_1 : Category.{v_2, u₂} D
F : Functor.{v_1, v_2, u₁, u₂} C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : D
h : F.obj Z ⟶ W
⊢ F.map (f ≫ g) ≫ h = F.map f ≫ F.map g ≫ h

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ obj.{v₁, v₁, u₁, u₁} (𝟭 C) X = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ map (𝟭 C) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
h : f = g
rw rw₁ : F.map g = F.map g
⊢ F.map f = F.map g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Functor.Basic
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
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f = G.map (F.map f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ F ⋙ 𝟭 D = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ 𝟭 C ⋙ F = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
P : Prop
inst_2 : Decidable P
f : P → (X ⟶ Y)
g : ¬P → (X ⟶ Y)
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map (if h : P then f h else g h)) (if h : P then F.map (f h) else F.map (g h))

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Functor.Basic
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
⊢ F.toPrefunctor ⋙q G.toPrefunctor = (F ⋙ G).toPrefunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.toPrefunctor, rfl
-- Module: Mathlib.CategoryTheory.Functor.Basic
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
h : F.toPrefunctor = G.toPrefunctor
obtain :
  ∀ (obj : C → D) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    (h :
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
        G.toPrefunctor),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } = G
⊢ F = G

Tactic:
obtain ⟨obj, map, _, _⟩ := F

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    G.toPrefunctor
obtain :
  ∀ (obj' : C → D) (map' : {X Y : C} → (X ⟶ Y) → (obj' X ⟶ obj' Y)) (map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj' X))
    (map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g)
    (h :
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
        { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
      { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } = G

Tactic:
obtain ⟨obj', map', _, _⟩ := G
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj' : C → D
map' : {X Y : C} → (X ⟶ Y) → (obj' X ⟶ obj' Y)
map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj' X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor
⊢ obj = obj'

Tactic:
congr_arg Prefunctor.obj h

Premises used: congr_arg, Prefunctor.obj
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj' : C → D
map' : {X Y : C} → (X ⟶ Y) → (obj' X ⟶ obj' Y)
map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj' X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor
obtain :
  ∀ (map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id_2 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X))
    (map_comp_2 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g)
    (h :
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
        { obj := obj, map := @map', map_id := map_id_2, map_comp := @map_comp_2 }.toPrefunctor),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
      { obj := obj, map := @map', map_id := map_id_2, map_comp := @map_comp_2 }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
obtain rfl : obj = obj' := congr_arg Prefunctor.obj h

Premises used: congr_arg, rfl, Prefunctor.obj
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    { obj := obj, map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor
⊢ @map = @map'

Tactic:
simpa [Functor.toPrefunctor] using h

Premises used: CategoryTheory.Functor.toPrefunctor
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    { obj := obj, map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor
obtain :
  ∀ (map_id_2 : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
    (map_comp_2 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    (h :
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
        { obj := obj, map := @map, map_id := map_id_2, map_comp := @map_comp_2 }.toPrefunctor),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
      { obj := obj, map := @map, map_id := map_id_2, map_comp := @map_comp_2 }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj, map := @map', map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
obtain rfl : @map = @map' := by simpa [Functor.toPrefunctor] using h

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map_id_1 : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    { obj := obj, map := @map, map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj, map := @map, map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α β : F ⟶ G
w : α.app = β.app
⊢ α = β

Tactic:
NatTrans.ext w

Premises used: CategoryTheory.NatTrans.ext
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : G ⟶ H
⊢ vcomp α β = α ≫ β

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : G ⟶ H
X : C
⊢ (α ≫ β).app X = α.app X ≫ β.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α β : F ⟶ G
h : α = β
X : C
rw rw₁ : β.app X = β.app X
⊢ α.app X = β.app X

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ app (𝟙 F) X = 𝟙 (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Category
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 : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
T : F ⟶ G
X : C
Y Z : D
f : Y ⟶ Z
⊢ (F.obj X).map f ≫ (T.app X).app Z = (T.app X).app Y ≫ (G.obj X).map f

Tactic:
(T.app X).naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.Category
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 : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
T : F ⟶ G
Z : D
X Y : C
f : X ⟶ Y
⊢ (F.map f).app Z ≫ (T.app Y).app Z = (T.app X).app Z ≫ (G.map f).app Z

Tactic:
congr_fun (congr_arg app (T.naturality f)) Z

Premises used: congr_arg, CategoryTheory.NatTrans.naturality, congr_fun, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.Category
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
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F G : C ⥤ D ⥤ Functor.{v₃, v₄, u₃, u₄} E E'
α : F ⟶ G
X₁ Y₁ : C
f : X₁ ⟶ Y₁
X₂ : D
X₃ : E
⊢ ((F.map f).app X₂).app X₃ ≫ ((α.app Y₁).app X₂).app X₃ = ((α.app X₁).app X₂).app X₃ ≫ ((G.map f).app X₂).app X₃

Tactic:
congr_app (NatTrans.naturality_app α X₂ f) X₃

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.NatTrans.naturality_app
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst_2 : IsIso (α.app X)
inst_3 : IsIso (α.app Y)
rw : F.map f ≫ α.app Y = α.app X ≫ G.map f
⊢ inv (α.app X) ≫ F.map f = G.map f ≫ inv (α.app Y)

Tactic:
rw [IsIso.inv_comp_eq, ← Category.assoc, IsIso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.IsIso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst_2 : IsIso (α.app X)
inst_3 : IsIso (α.app Y)
⊢ F.map f ≫ α.app Y = α.app X ≫ G.map f

Tactic:
α.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst_2 : IsIso (α.app X)
inst_3 : IsIso (α.app Y)
⊢ F.map f ≫ α.app Y = α.app X ≫ G.map f

Tactic:
exact α.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α : F ⟶ G
inst_2 : ∀ (X : C), Epi (α.app X)
Z : Functor.{v₁, v₂, u₁, u₂} C D
g h : G ⟶ Z
eq : α ≫ g = α ≫ h
w : ∀ (X : C), g.app X = h.app X
⊢ g = h

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α : F ⟶ G
inst_2 : ∀ (X : C), Epi (α.app X)
Z : Functor.{v₁, v₂, u₁, u₂} C D
g h : G ⟶ Z
eq : α ≫ g = α ≫ h
X : C
w : α.app X ≫ g.app X = α.app X ≫ h.app X
w₁ : (α ≫ g).app X = α.app X ≫ h.app X
w₂ : (α ≫ h).app X = α.app X ≫ h.app X
w₃ w₄ : α.app X ≫ h.app X = α.app X ≫ h.app X
⊢ g.app X = h.app X

Tactic:
rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]

Premises used: CategoryTheory.NatTrans.comp_app, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α β : Quiver.Hom (V := Functor.{v₁, v₁, u₁, u₁} C C) (𝟭 C) (𝟭 C)
w : ∀ (X : C), (α ≫ β).app X = (β ≫ α).app X
⊢ α ≫ β = β ≫ α

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α β : Quiver.Hom (V := Functor.{v₁, v₁, u₁, u₁} C C) (𝟭 C) (𝟭 C)
X : C
⊢ (α ≫ β).app X = (β ≫ α).app X

Tactic:
(α.naturality (β.app X)).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α β : Quiver.Hom (V := Functor.{v₁, v₁, u₁, u₁} C C) (𝟭 C) (𝟭 C)
X : C
⊢ (α ≫ β).app X = (β ≫ α).app X

Tactic:
exact (α.naturality (β.app X)).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.Category
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 I : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ F
β : I ⟶ H
w :
  ∀ (x : C),
    { app := fun (X : C) ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ : NatTrans (G ⋙ I) (F ⋙ H) }.app x =
      (mk' (fun (X : C) ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯).app x
⊢ { app := fun (X : C) ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ : NatTrans (G ⋙ I) (F ⋙ H) } =
    mk' (fun (X : C) ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Functor.Category
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 I : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ F
β : I ⟶ H
x : C
⊢ { app := fun (X : C) ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ : NatTrans (G ⋙ I) (F ⋙ H) }.app x =
    (mk' (fun (X : C) ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯).app x

Tactic:
β.naturality' (α.app x)

Premises used: CategoryTheory.NatTrans.naturality', CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.Category
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 I : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ F
β : I ⟶ H
x : C
⊢ { app := fun (X : C) ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ : NatTrans (G ⋙ I) (F ⋙ H) }.app x =
    (mk' (fun (X : C) ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯).app x

Tactic:
exact β.naturality' (α.app x)

Premises used: CategoryTheory.NatTrans.naturality', CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.Category
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
α : F ⟶ G
X : C
⊢ (α ◫ 𝟙 H).app X = H.map (α.app X)

Tactic:
simp