awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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')
        (((e j').symm : (a : G.obj j') → F.obj j')
          ((ConcreteCategory.hom (FC := Fun) (G.map f) : (a : G.obj j) → 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')
        ((ConcreteCategory.hom (FC := Fun) (F.map f) : (a : F.obj j) → F.obj j')
          (((e j).symm : (a : G.obj j) → F.obj j) ((e j : (a : F.obj j) → G.obj j) y) : F.obj j)) :
      G.obj j')
⊢ 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')

Tactic:
dsimp
-- 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 (α := G.obj j')
    ((ConcreteCategory.hom (FC := Fun) (G.map f) : (a : G.obj j) → 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') ((ConcreteCategory.hom (FC := Fun) (F.map f) : (a : F.obj j) → F.obj j') y) :
      G.obj j')
⊢ Eq.{u_2 + 1} (α := G.obj j')
    ((e j' : (a : F.obj j') → G.obj j')
        (((e j').symm : (a : G.obj j') → F.obj j')
          ((ConcreteCategory.hom (FC := Fun) (G.map f) : (a : G.obj j) → 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')
        ((ConcreteCategory.hom (FC := Fun) (F.map f) : (a : F.obj j) → F.obj j')
          (((e j).symm : (a : G.obj j) → F.obj j) ((e j : (a : F.obj j) → G.obj j) y) : F.obj j)) :
      G.obj j')

Tactic:
simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_apply
-- 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
⊢ Eq (α := G.obj j')
    ((ConcreteCategory.hom (FC := Fun) (G.map f) : (a : G.obj j) → 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') ((ConcreteCategory.hom (FC := Fun) (F.map f) : (a : F.obj j) → F.obj j') y) :
      G.obj j')

Tactic:
(congr_fun (naturality f) y).symm

Premises used: congr_fun, Eq.symm
-- 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
⊢ Eq (α := G.obj j')
    ((ConcreteCategory.hom (FC := Fun) (G.map f) : (a : G.obj j) → 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') ((ConcreteCategory.hom (FC := Fun) (F.map f) : (a : F.obj j) → F.obj j') y) :
      G.obj j')

Tactic:
exact (congr_fun (naturality f) y).symm

Premises used: congr_fun, Eq.symm
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
⊢ uliftFunctor.{v, u}.Full

Tactic:
fullyFaithfulULiftFunctor.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.fullyFaithfulULiftFunctor
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
⊢ uliftFunctor.{v, u}.Faithful

Tactic:
fullyFaithfulULiftFunctor.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.fullyFaithfulULiftFunctor
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u
x y : X
⊢ x = y → homOfElement x = homOfElement y

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
mp : Mono (↾f) → Function.Injective f
mpr : Function.Injective f → Mono (↾f)
⊢ Mono (↾f) ↔ Function.Injective f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
h : f x = f x'
mp : ∀ (h : homOfElement (f x) = homOfElement (f x')), homOfElement x = homOfElement x'
⊢ x = x'

Tactic:
rw [← homOfElement_eq_iff] at h ⊢

Premises used: CategoryTheory.homOfElement_eq_iff
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
h : homOfElement (f x) = homOfElement (f x')
⊢ homOfElement x = homOfElement x'

Tactic:
(cancel_mono (ofHom f)).mp h

Premises used: TypeCat.ofHom, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
h : homOfElement (f x) = homOfElement (f x')
⊢ homOfElement x = homOfElement x'

Tactic:
exact (cancel_mono (ofHom f)).mp h

Premises used: TypeCat.ofHom, CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
⊢ Function.Injective f → Mono (↾f)

Tactic:
fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩

Premises used: CategoryTheory.Mono.mk, CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
mpr :
  ∀ (H : Function.Injective f) {Z : Type u} (g g' : Z ⟶ X) (h : g ≫ ↾f = g' ≫ ↾f) (x : Z),
    Eq.{u + 1} (α := Z → Y) ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Z) → X))
      ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Z) → X))
⊢ Function.Injective f → Mono (↾f)

Tactic:
refine fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Function.Injective f
Z : Type u
g g' : Z ⟶ X
h : g ≫ ↾f = g' ≫ ↾f
x : Z
mpr :
  ∀ (y : Z),
    Eq.{u + 1} (α := Y) ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Z) → X) y)
      ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Z) → X) y)
⊢ Eq.{u + 1} (α := Z → Y) ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Z) → X))
    ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Z) → X))

Tactic:
ext y
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Function.Injective f
Z : Type u
g g' : Z ⟶ X
h : g ≫ ↾f = g' ≫ ↾f
x y : Z
⊢ Eq.{u + 1} (α := Y) ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Z) → X) y)
    ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Z) → X) y)

Tactic:
ConcreteCategory.congr_hom h y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Function.Injective f
Z : Type u
g g' : Z ⟶ X
h : g ≫ ↾f = g' ≫ ↾f
x y : Z
⊢ Eq.{u + 1} (α := Y) ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Z) → X) y)
    ((fun (x : Z → X) ↦ f ∘ x) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Z) → X) y)

Tactic:
exact ConcreteCategory.congr_hom h y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ Mono f ↔
    Function.Injective (α := (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)

Tactic:
simp [← ofHom_mono_iff_injective]

Premises used: CategoryTheory.ofHom_mono_iff_injective
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
hf : Mono f
⊢ Function.Injective (α := (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)

Tactic:
(mono_iff_injective f).1 hf

Premises used: CategoryTheory.mono_iff_injective, Iff.mp
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
mp : Epi (↾f) → Function.Surjective f
mpr : Function.Surjective f → Epi (↾f)
⊢ Epi (↾f) ↔ Function.Surjective f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
⊢ Function.Surjective f

Tactic:
Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_

Premises used: Function.surjective_of_right_cancellable_Prop
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
mp : ∀ (g₁ g₂ : Y → Prop) (hg : g₁ ∘ f = g₂ ∘ f), g₁ = g₂
⊢ Function.Surjective f

Tactic:
refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_

Premises used: Function.surjective_of_right_cancellable_Prop
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
mp :
  Eq (α := Y → ULift.{u, 0} Prop) ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁)
    ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂)
⊢ g₁ = g₂

Tactic:
rw [← Equiv.ulift.{u}.symm.injective.comp_left.eq_iff]
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
mp :
  Eq (α := Y ⟶ ULift.{u, 0} Prop)
    ((Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁) :
      Y ⟶ ULift.{u, 0} Prop)
    ((Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂) :
      Y ⟶ ULift.{u, 0} Prop)
⊢ Eq (α := Y → ULift.{u, 0} Prop) ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁)
    ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂)

Tactic:
apply TypeCat.homEquiv.symm.injective

Premises used: TypeCat.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
mp :
  Eq (α := X ⟶ ULift.{u, 0} Prop)
    (↾f ≫
      (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁))
    (↾f ≫
      (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂))
⊢ Eq (α := Y ⟶ ULift.{u, 0} Prop)
    ((Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁) :
      Y ⟶ ULift.{u, 0} Prop)
    ((Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂) :
      Y ⟶ ULift.{u, 0} Prop)

Tactic:
apply H
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
mp :
  ∀ (x : X),
    Eq (α := ULift.{u, 0} Prop)
      ((ConcreteCategory.hom (FC := Fun)
              (↾f ≫
                (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
                  ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁)) :
            (a : X) → ULift.{u, 0} Prop)
          x :
        ULift.{u, 0} Prop)
      ((ConcreteCategory.hom (FC := Fun)
              (↾f ≫
                (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
                  ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂)) :
            (a : X) → ULift.{u, 0} Prop)
          x :
        ULift.{u, 0} Prop)
⊢ Eq (α := X ⟶ ULift.{u, 0} Prop)
    (↾f ≫
      (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁))
    (↾f ≫
      (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
        ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂))

Tactic:
apply ConcreteCategory.hom_ext

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
x : X
⊢ Eq (α := ULift.{u, 0} Prop)
    ((ConcreteCategory.hom (FC := Fun)
            (↾f ≫
              (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
                ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₁)) :
          (a : X) → ULift.{u, 0} Prop)
        x :
      ULift.{u, 0} Prop)
    ((ConcreteCategory.hom (FC := Fun)
            (↾f ≫
              (Equiv.symm homEquiv : (a : Y → ULift.{u, 0} Prop) → Y ⟶ ULift.{u, 0} Prop)
                ((⇑(Equiv.symm Equiv.ulift) : (a : Prop) → ULift.{u, 0} Prop) ∘ g₂)) :
          (a : X) → ULift.{u, 0} Prop)
        x :
      ULift.{u, 0} Prop)

Tactic:
simp [dsimp% congrFun hg x]

Premises used: congrFun
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
⊢ Function.Surjective f → Epi (↾f)

Tactic:
fun H => ⟨fun g g' h =>  ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.injective_comp_right ?_) x⟩

Premises used: CategoryTheory.Epi.mk, CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
mpr :
  ∀ (H : Function.Surjective f) {Z : Type u} (g g' : Y ⟶ Z) (h : ↾f ≫ g = ↾f ≫ g') (x : Y),
    Eq.{u + 1} (α := X → Z) ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Y) → Z))
      ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Y) → Z))
⊢ Function.Surjective f → Epi (↾f)

Tactic:
refine fun H => ⟨fun g g' h =>  ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.injective_comp_right ?_) x⟩
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Function.Surjective f
Z : Type u
g g' : Y ⟶ Z
h : ↾f ≫ g = ↾f ≫ g'
x : Y
mpr :
  ∀ (y : X),
    Eq.{u + 1} (α := Z) ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Y) → Z) y)
      ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Y) → Z) y)
⊢ Eq.{u + 1} (α := X → Z) ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Y) → Z))
    ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Y) → Z))

Tactic:
ext y
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Function.Surjective f
Z : Type u
g g' : Y ⟶ Z
h : ↾f ≫ g = ↾f ≫ g'
x : Y
y : X
⊢ Eq.{u + 1} (α := Z) ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Y) → Z) y)
    ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Y) → Z) y)

Tactic:
ConcreteCategory.congr_hom h y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
H : Function.Surjective f
Z : Type u
g g' : Y ⟶ Z
h : ↾f ≫ g = ↾f ≫ g'
x : Y
y : X
⊢ Eq.{u + 1} (α := Z) ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g) : (a : Y) → Z) y)
    ((fun (g : Y → Z) ↦ g ∘ f) (⇑(ConcreteCategory.hom (FC := Fun) g') : (a : Y) → Z) y)

Tactic:
exact ConcreteCategory.congr_hom h y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ Epi f ↔
    Function.Surjective (α := (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)

Tactic:
simp [← ofHom_epi_iff_surjective]

Premises used: CategoryTheory.ofHom_epi_iff_surjective
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
hf : Epi f
⊢ Function.Surjective (α := (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)

Tactic:
(epi_iff_surjective f).1 hf

Premises used: CategoryTheory.epi_iff_surjective, Iff.mp
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
m : Type u → Type v
inst : _root_.Functor m
inst_1 : LawfulFunctor m
α : Type u
h :
  ∀ (X : m α),
    Fun.toFun (ConcreteCategory.hom (FC := Fun) (↾_root_.Functor.map (⇑(Hom.hom (𝟙 α)) : (a : α) → α))) X =
      (ConcreteCategory.hom (FC := Fun) (𝟙 (m α))).toFun X
⊢ ↾_root_.Functor.map (⇑(Hom.hom (𝟙 α)) : (a : α) → α) = 𝟙 (m α)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
m : Type u → Type v
inst : _root_.Functor m
inst_1 : LawfulFunctor m
α : Type u
X : m α
⊢ Fun.toFun (ConcreteCategory.hom (FC := Fun) (↾_root_.Functor.map (⇑(Hom.hom (𝟙 α)) : (a : α) → α))) X =
    (ConcreteCategory.hom (FC := Fun) (𝟙 (m α))).toFun X

Tactic:
apply id_map

Premises used: LawfulFunctor.id_map
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
m : Type u → Type v
inst : _root_.Functor m
inst_1 : LawfulFunctor m
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : m X),
    Eq (α := m Z)
      (Fun.toFun (ConcreteCategory.hom (FC := Fun) (↾_root_.Functor.map (⇑(Hom.hom (f ≫ g)) : (a : X) → Z))) x)
      (Fun.toFun
        (ConcreteCategory.hom (FC := Fun)
          (CategoryStruct.comp (Y := m Y) (↾_root_.Functor.map (⇑(Hom.hom f) : (a : X) → Y))
            (↾_root_.Functor.map (⇑(Hom.hom g) : (a : Y) → Z))))
        x)
⊢ Eq.{v + 1} (α := m X ⟶ m Z) (↾_root_.Functor.map (⇑(Hom.hom (f ≫ g)) : (a : X) → Z))
    (CategoryStruct.comp (Y := m Y) (↾_root_.Functor.map (⇑(Hom.hom f) : (a : X) → Y))
      (↾_root_.Functor.map (⇑(Hom.hom g) : (a : Y) → Z)))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
m : Type u → Type v
inst : _root_.Functor m
inst_1 : LawfulFunctor m
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
x : m X
⊢ Eq (α := m Z)
    (Fun.toFun (ConcreteCategory.hom (FC := Fun) (↾_root_.Functor.map (⇑(Hom.hom (f ≫ g)) : (a : X) → Z))) x)
    (Fun.toFun
      (ConcreteCategory.hom (FC := Fun)
        (CategoryStruct.comp (Y := m Y) (↾_root_.Functor.map (⇑(Hom.hom f) : (a : X) → Y))
          (↾_root_.Functor.map (⇑(Hom.hom g) : (a : Y) → Z))))
      x)

Tactic:
comp_map (f := m) f.hom g.hom x

Premises used: TypeCat.Hom.hom, DFunLike.coe, LawfulFunctor.comp_map
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
m : Type u → Type v
inst : _root_.Functor m
inst_1 : LawfulFunctor m
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
x : m X
⊢ Eq (α := m Z)
    (Fun.toFun (ConcreteCategory.hom (FC := Fun) (↾_root_.Functor.map (⇑(Hom.hom (f ≫ g)) : (a : X) → Z))) x)
    (Fun.toFun
      (ConcreteCategory.hom (FC := Fun)
        (CategoryStruct.comp (Y := m Y) (↾_root_.Functor.map (⇑(Hom.hom f) : (a : X) → Y))
          (↾_root_.Functor.map (⇑(Hom.hom g) : (a : Y) → Z))))
      x)

Tactic:
exact comp_map (f := m) f.hom g.hom x

Premises used: TypeCat.Hom.hom, DFunLike.coe, LawfulFunctor.comp_map
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
i : X ≅ Y
x : X
⊢ (ConcreteCategory.hom (FC := Fun) i.inv : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) X)
      ((ConcreteCategory.hom (FC := Fun) i.hom : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
        (fun (X : Type u) ↦ X) Y) =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
i : X ≅ Y
y : Y
⊢ (ConcreteCategory.hom (FC := Fun) i.hom : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
      ((ConcreteCategory.hom (FC := Fun) i.inv : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) X) y :
        (fun (X : Type u) ↦ X) X) =
    y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
i : X ≅ Y
⊢ Eq (α := (a : X) → Y) (⇑i.toEquiv : (a : X) → Y)
    (⇑(ConcreteCategory.hom (FC := Fun) i.hom) : (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
i : X ≅ Y
⊢ (⇑i.toEquiv.symm : (a : Y) → X) = (ConcreteCategory.hom (FC := Fun) i.inv).toFun

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X : Type u
⊢ toEquiv (refl X) = Equiv.refl X

Tactic:
rfl

Premises used: CategoryTheory.Iso.toEquiv, Equiv.refl, rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y Z : Type u
f : X ≅ Y
g : Y ≅ Z
⊢ (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv

Tactic:
rfl

Premises used: CategoryTheory.Iso.toEquiv, Equiv.trans, rfl