awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C D E : Cat
F G : C ⟶ D
H : D ⟶ E
η : F ⟶ G
X : (↑C : Type u)
⊢ (η ▷ H).toNatTrans.app X = H.toFunctor.map (η.toNatTrans.app X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
⊢ toNatIso (λ_ F) = F.toFunctor.leftUnitor

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Functor.leftUnitor, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
⊢ (λ_ F).hom.toNatTrans = F.toFunctor.leftUnitor.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
⊢ (λ_ F).inv.toNatTrans = F.toFunctor.leftUnitor.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u_2)
⊢ (𝟙 B ≫ F).toFunctor.obj X = F.toFunctor.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u_2)
⊢ (λ_ F).hom.toNatTrans.app X = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u_2)
⊢ F.toFunctor.obj X = (𝟙 B ≫ F).toFunctor.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u_2)
⊢ (λ_ F).inv.toNatTrans.app X = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
simp : toNatIso (ρ_ F) = F.toFunctor.rightUnitor
⊢ toNatIso (ρ_ F) = eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ eqToIso ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
⊢ toNatIso (ρ_ F) = F.toFunctor.rightUnitor

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
⊢ (ρ_ F).hom.toNatTrans = F.toFunctor.rightUnitor.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
⊢ (ρ_ F).inv.toNatTrans = F.toFunctor.rightUnitor.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u)
⊢ (F ≫ 𝟙 C).toFunctor.obj X = F.toFunctor.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u)
⊢ (ρ_ F).hom.toNatTrans.app X = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u)
⊢ F.toFunctor.obj X = (F ≫ 𝟙 C).toFunctor.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C : Cat
F : B ⟶ C
X : (↑B : Type u)
⊢ (ρ_ F).inv.toNatTrans.app X = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
⊢ toNatIso (α_ F G H) = F.toFunctor.associator G.toFunctor H.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Functor.associator, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
⊢ (α_ F G H).hom.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
⊢ (α_ F G H).inv.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : (↑B : Type u_2)
⊢ ((F ≫ G) ≫ H).toFunctor.obj X = (F ≫ G ≫ H).toFunctor.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : (↑B : Type u_2)
⊢ (α_ F G H).hom.toNatTrans.app X = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : (↑B : Type u_2)
⊢ (F ≫ G ≫ H).toFunctor.obj X = ((F ≫ G) ≫ H).toFunctor.obj X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : (↑B : Type u_2)
⊢ (α_ F G H).inv.toNatTrans.app X = eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X : Cat
⊢ Hom.toFunctor (𝟙 X) = 𝟭 (↑X : Type v)

Tactic:
rfl

Premises used: CategoryTheory.Functor.id, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y Z : Cat
F : X ⟶ Y
G : Y ⟶ Z
⊢ (F ≫ G).toFunctor = F.toFunctor ⋙ G.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ (↑(of C) : Type u_1) = C

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
C : Cat
⊢ of (↑C : Type u) = C

Tactic:
rfl

Premises used: CategoryTheory.Cat.of, CategoryTheory.Cat, CategoryTheory.Bundled.of, rfl
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X : Type u
h :
  Cat.Hom.toFunctor
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X)))) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (Discrete X)))
⊢ toCatHom
      (Discrete.functor
        (Discrete.mk ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) :
            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X))) =
    𝟙 (Cat.of (Discrete X))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X : Type u
h :
  Eq (α := Discrete X ⥤ Discrete X)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X)))
    (𝟭 (Discrete X))
⊢ Cat.Hom.toFunctor
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X)))) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (Discrete X)))

Tactic:
simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.id_toFunctor]

Premises used: CategoryTheory.Cat.of_α, CategoryTheory.Cat.Hom.id_toFunctor, CategoryTheory.Functor.toCatHom_toFunctor
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X : Type u
h :
  ∀ (X_1 : Discrete X),
    obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) X_1 =
      obj (𝟭 (Discrete X)) X_1
h₁ :
  autoParam
    (∀ (X_1 Y : Discrete X) (f : X_1 ⟶ Y),
      Eq (α :=
        Quiver.Hom (V := Discrete X)
          (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) X_1)
          (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) Y))
        (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) f)
        (CategoryStruct.comp (Y := obj (𝟭 (Discrete X)) X_1) (eqToHom ⋯) (map (𝟭 (Discrete X)) f ≫ eqToHom ⋯)))
    ext._auto_1
⊢ Eq (α := Discrete X ⥤ Discrete X)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X)))
    (𝟭 (Discrete X))

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X : Type u
⊢ ∀ (X_1 : Discrete X),
    obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) X_1 =
      obj (𝟭 (Discrete X)) X_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X_1 : Type u
X Y : Discrete X_1
f : X ⟶ Y
h :
  ∀ (down : PLift (X.as = Y.as)),
    Eq (α :=
      Quiver.Hom (V := Discrete X_1)
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
          X)
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
          Y))
      (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
        { down := down })
      (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom ⋯)
        (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) Y) (map (𝟭 (Discrete X_1)) { down := down }) (eqToHom ⋯)))
⊢ Eq (α :=
    Quiver.Hom (V := Discrete X_1)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1))) X)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
        Y))
    (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1))) f)
    (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom ⋯) (map (𝟭 (Discrete X_1)) f ≫ eqToHom ⋯))

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X_1 : Type u
X Y : Discrete X_1
down : PLift (X.as = Y.as)
h :
  Eq (α :=
    PLift
      (Eq (α := (fun (X : Type u) ↦ X) X_1)
        (Discrete.as
          (obj
            (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
            X))
        (Discrete.as
          (obj
            (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
            Y))))
    (ULift.down.{u, 0}
      (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
        { down := down }))
    (ULift.down.{u, 0}
      (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom ⋯)
        (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) Y) (map (𝟭 (Discrete X_1)) { down := down }) (eqToHom ⋯))))
⊢ Eq (α :=
    Quiver.Hom (V := Discrete X_1)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1))) X)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
        Y))
    (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
      { down := down })
    (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom ⋯)
      (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) Y) (map (𝟭 (Discrete X_1)) { down := down }) (eqToHom ⋯)))

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
h :
  Eq (α :=
    (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) X))) : Type u) ⥤
      (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) Z))) : Type u))
    (Cat.Hom.toFunctor
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (Discrete Y))
        (toCatHom
          (Discrete.functor
            (Discrete.mk ∘
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))))
        (toCatHom
          (Discrete.functor
            (Discrete.mk ∘
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z))))))
⊢ Eq (α := Cat.of (Discrete X) ⟶ Cat.of (Discrete Z))
    (toCatHom
      (Discrete.functor
        (Discrete.mk ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) :
            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z))))
    (CategoryStruct.comp (Y := Cat.of (Discrete Y))
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))))
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
h :
  Eq (α := Discrete X ⥤ Discrete Z)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
    (comp (D := Discrete Y)
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
⊢ Eq (α :=
    (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) X))) : Type u) ⥤
      (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) Z))) : Type u))
    (Cat.Hom.toFunctor
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (Discrete Y))
        (toCatHom
          (Discrete.functor
            (Discrete.mk ∘
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))))
        (toCatHom
          (Discrete.functor
            (Discrete.mk ∘
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z))))))

Tactic:
simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.comp_toFunctor]

Premises used: CategoryTheory.Cat.of_α, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Functor.toCatHom_toFunctor
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
h :
  autoParam
    (∀ (X_1 Y_1 : Discrete X) (f_1 : X_1 ⟶ Y_1),
      Eq (α :=
        Quiver.Hom (V := Discrete Z)
          (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
            X_1)
          (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
            Y_1))
        (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z))) f_1)
        (CategoryStruct.comp (Y :=
          obj
            (comp (D := Discrete Y)
              (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
              (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
            X_1)
          (eqToHom ⋯)
          (map
              (comp (D := Discrete Y)
                (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
                (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
              f_1 ≫
            eqToHom ⋯)))
    ext._auto_1
h₁ :
  ∀ (X_1 : Discrete X),
    Eq (α := Discrete Z)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z))) X_1)
      (obj
        (comp (D := Discrete Y)
          (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
          (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
        X_1)
⊢ Eq (α := Discrete X ⥤ Discrete Z)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
    (comp (D := Discrete Y)
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))

Tactic:
apply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
_X _Y : Type u
_f _g : _X ⟶ _Y
h : typeToCat.map _f = typeToCat.map _g
h₁ :
  ∀ (x : _X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) _f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) _g).toFun x
⊢ _f = _g

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
_X _Y : Type u
_f _g : _X ⟶ _Y
h : typeToCat.map _f = typeToCat.map _g
x : _X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) _f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) _g).toFun x

Tactic:
congrArg Discrete.as (Functor.congr_obj congr(($h).toFunctor) ⟨x⟩)

Premises used: congrArg, CategoryTheory.Functor.congr_obj, id, CategoryTheory.Discrete.mk, CategoryTheory.Discrete.as, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
_X _Y : Type u
_f _g : _X ⟶ _Y
h : typeToCat.map _f = typeToCat.map _g
x : _X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) _f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) _g).toFun x

Tactic:
exact congrArg Discrete.as (Functor.congr_obj congr(($h).toFunctor) ⟨x⟩)

Premises used: congrArg, CategoryTheory.Functor.congr_obj, id, CategoryTheory.Discrete.mk, CategoryTheory.Discrete.as, CategoryTheory.Cat.Hom.toFunctor
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
h : (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor = F.toFunctor
⊢ typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk)) = F

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (X_1 : (↑(typeToCat.obj X) : Type u)),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.obj X_1 = F.toFunctor.obj X_1
⊢ ∀ (X_1 : (↑(typeToCat.obj X) : Type u)),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.obj X_1 = F.toFunctor.obj X_1

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
h :
  ∀ (X_1 Y_1 : (↑(typeToCat.obj X) : Type u)) (f : X_1 ⟶ Y_1),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
      eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯
⊢ (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor = F.toFunctor

Tactic:
refine Functor.ext (by cat_disch) ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Category.Cat
Goal:
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : (↑(typeToCat.obj X) : Type u)
f : x ⟶ y
h :
  ULift.down.{u, 0} ((typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f) =
    ULift.down.{u, 0} (eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯)
⊢ (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
    eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- Module: Mathlib.CategoryTheory.Category.Factorisation
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
d : Factorisation f_1
f : Factorisation.initial ⟶ d
h : f.h = d.initialHom.h
⊢ f = d.initialHom

Tactic:
apply Factorisation.Hom.ext

Premises used: CategoryTheory.Factorisation.Hom.ext
-- Module: Mathlib.CategoryTheory.Category.Factorisation
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
d : Factorisation f_1
f : Factorisation.initial ⟶ d
⊢ f.h = d.initialHom.h

Tactic:
simp [← f.ι_h]

Premises used: CategoryTheory.Factorisation.Hom.ι_h
-- Module: Mathlib.CategoryTheory.Category.Factorisation
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
d : Factorisation f_1
f : d ⟶ Factorisation.terminal
h : f.h = d.terminalHom.h
⊢ f = d.terminalHom

Tactic:
apply Factorisation.Hom.ext

Premises used: CategoryTheory.Factorisation.Hom.ext
-- Module: Mathlib.CategoryTheory.Category.Factorisation
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
d : Factorisation f_1
f : d ⟶ Factorisation.terminal
⊢ f.h = d.terminalHom.h

Tactic:
simp [← f.h_π]

Premises used: CategoryTheory.Factorisation.Hom.h_π
-- Module: Mathlib.CategoryTheory.Category.Factorisation
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
d : Factorisation f
⊢ HasInitial (Factorisation f)

Tactic:
Limits.hasInitial_of_unique Factorisation.initial

Premises used: CategoryTheory.Limits.hasInitial_of_unique, CategoryTheory.Factorisation.initial
-- Module: Mathlib.CategoryTheory.Category.Factorisation
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
d : Factorisation f
⊢ HasTerminal (Factorisation f)

Tactic:
Limits.hasTerminal_of_unique Factorisation.terminal

Premises used: CategoryTheory.Limits.hasTerminal_of_unique, CategoryTheory.Factorisation.terminal
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
α β : KleisliCat m
f g : α ⟶ β
h : ∀ (x : α), f x = g x
⊢ f = g

Tactic:
funext h

Premises used: funext
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
refine_1 : ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f
refine_2 : ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f
refine_3 : ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
⊢ Category.{max u v, u + 1} (KleisliCat m)

Tactic:
refine { id_comp := ?_, comp_id := ?_, assoc := ?_ }
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
refine_1 : ∀ (x : X), (𝟙 X ≫ f) x = f x
⊢ 𝟙 X ≫ f = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
refine_2 : ∀ (x : X), (f ≫ 𝟙 Y) x = f x
⊢ f ≫ 𝟙 Y = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
W X Y Z : KleisliCat m
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
refine_3 : ∀ (x : W), ((f ≫ g) ≫ h) x = (f ≫ g ≫ h) x
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
x : X
⊢ (𝟙 X ≫ f) x = f x

Tactic:
simp +unfoldPartialApp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, Bind.kleisliRight
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
x : X
⊢ (f ≫ 𝟙 Y) x = f x

Tactic:
simp +unfoldPartialApp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, Bind.kleisliRight
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
W X Y Z : KleisliCat m
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
x : W
⊢ ((f ≫ g) ≫ h) x = (f ≫ g ≫ h) x

Tactic:
simp +unfoldPartialApp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, Bind.kleisliRight
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u_1 → Type u_2
inst : Monad m
α : KleisliCat m
⊢ Eq (α := α ⟶ α) (𝟙 α) pure

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.KleisliCat
Goal:
m : Type u_1 → Type u_2
inst : Monad m
α β γ : KleisliCat m
xs : α ⟶ β
ys : β ⟶ γ
a : α
⊢ (xs ≫ ys) a = xs a >>= ys

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Pairwise
Goal:
ι : Type v
α : Type u
U : ι → α
inst : CompleteLattice α
s : Cocone (diagram U)
h : ∀ b ∈ Set.range U, b ≤ s.pt
⊢ Cocone.pt (cocone U) ≤ s.pt

Tactic:
apply sSup_le

Premises used: sSup_le
-- Module: Mathlib.CategoryTheory.Category.Pairwise
Goal:
ι : Type v
α : Type u
U : ι → α
inst : CompleteLattice α
s : Cocone (diagram U)
j : ι
⊢ U j ≤ s.pt

Tactic:
(s.ι.app (single j)).le

Premises used: Quiver.Hom.le, CategoryTheory.Pairwise.single, CategoryTheory.Pairwise.diagramObj, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Category.Pairwise
Goal:
ι : Type v
α : Type u
U : ι → α
inst : CompleteLattice α
s : Cocone (diagram U)
j : ι
⊢ U j ≤ s.pt

Tactic:
exact (s.ι.app (single j)).le

Premises used: Quiver.Hom.le, CategoryTheory.Pairwise.single, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app