awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
FD : D → D → Type u_2
CD : D → Type w
inst_2 : (X Y : D) → FunLike.{u_2 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_3 : ConcreteCategory.{w, v_1, u_1, u_2} D FD (CC := CD)
F G : Functor.{v, v_1, u, u_1} C D
φ : F ⟶ G
X Y : C
f : X ⟶ Y
x : ToType.{w, v_1, u_1, u_2} (FC := FD) (CC := CD) (F.obj X)
⊢ Eq (α := CD (G.obj Y))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app Y) : (a : CD (F.obj Y)) → CD (G.obj Y))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (F.map f) : (a : CD (F.obj X)) → CD (F.obj Y)) x : CD (F.obj Y)) :
      CD (G.obj Y))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (G.map f) : (a : CD (G.obj X)) → CD (G.obj Y))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) (φ.app X) : (a : CD (F.obj X)) → CD (G.obj X)) x : CD (G.obj X)) :
      CD (G.obj Y))

Tactic:
simp [← CategoryTheory.comp_apply]

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Bundled
Goal:
c : Type u → Type v
α : Type u
str : c α
⊢ (↑{ α := α, str := str : Bundled c } : Type u) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
inst_4 : Mono f
⊢ Mono.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
Functor.map_mono (forget C) f

Premises used: CategoryTheory.Functor.map_mono, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
inst_4 : Epi f
⊢ Epi.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
Functor.map_epi (forget C) f

Premises used: CategoryTheory.Functor.map_epi, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
X Y : C
f : X ⟶ Y
i : Function.Injective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)
⊢ Mono f

Tactic:
(forget C).mono_of_mono_map ((mono_iff_injective ((forget C).map f)).2 i)

Premises used: Iff.mpr, CategoryTheory.mono_iff_injective, CategoryTheory.Functor.map, CategoryTheory.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC_1 : C_1 → C_1 → Type u_1
CC_1 : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC_1 X Y) (CC_1 X) (CC_1 Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC_1 (CC := CC_1)
C : Type u
D : Type u'
inst_3 : Category.{v, u} C
inst_4 : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst_5 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w, v, u, u_2} C FC (CC := CC)
FD : D → D → Type u_3
CD : D → Type w
inst_7 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_8 : ConcreteCategory.{w, v', u', u_3} D FD (CC := CD)
inst_9 : HasForget₂.{w, v, u, u_2, v', u', u_3} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_10 simp : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
⊢ Functor.PreservesMonomorphisms.{v, w, u, w + 1}
    (Functor.comp.{v, v', w, u, u', w + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD))
      (forget D (FC := FD) (CC := CD)))

Tactic:
simp only [HasForget₂.forget_comp]

Premises used: CategoryTheory.HasForget₂.forget_comp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC_1 : C_1 → C_1 → Type u_1
CC_1 : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC_1 X Y) (CC_1 X) (CC_1 Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC_1 (CC := CC_1)
C : Type u
D : Type u'
inst_3 : Category.{v, u} C
inst_4 : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst_5 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w, v, u, u_2} C FC (CC := CC)
FD : D → D → Type u_3
CD : D → Type w
inst_7 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_8 : ConcreteCategory.{w, v', u', u_3} D FD (CC := CD)
inst_9 : HasForget₂.{w, v, u, u_2, v', u', u_3} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_10 : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
⊢ Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC_1 : C_1 → C_1 → Type u_1
CC_1 : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC_1 X Y) (CC_1 X) (CC_1 Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC_1 (CC := CC_1)
C : Type u
D : Type u'
inst_3 : Category.{v, u} C
inst_4 : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst_5 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w, v, u, u_2} C FC (CC := CC)
FD : D → D → Type u_3
CD : D → Type w
inst_7 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_8 : ConcreteCategory.{w, v', u', u_3} D FD (CC := CD)
inst_9 : HasForget₂.{w, v, u, u_2, v', u', u_3} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_10 simp : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
⊢ Functor.PreservesEpimorphisms.{v, w, u, w + 1}
    (Functor.comp.{v, v', w, u, u', w + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD))
      (forget D (FC := FD) (CC := CD)))

Tactic:
simp only [HasForget₂.forget_comp]

Premises used: CategoryTheory.HasForget₂.forget_comp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
FC_1 : C_1 → C_1 → Type u_1
CC_1 : C_1 → Type w
inst_1 : (X Y : C_1) → FunLike.{u_1 + 1, w + 1, w + 1} (FC_1 X Y) (CC_1 X) (CC_1 Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C_1 FC_1 (CC := CC_1)
C : Type u
D : Type u'
inst_3 : Category.{v, u} C
inst_4 : Category.{v', u'} D
FC : C → C → Type u_2
CC : C → Type w
inst_5 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w, v, u, u_2} C FC (CC := CC)
FD : D → D → Type u_3
CD : D → Type w
inst_7 : (X Y : D) → FunLike.{u_3 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_8 : ConcreteCategory.{w, v', u', u_3} D FD (CC := CD)
inst_9 : HasForget₂.{w, v, u, u_2, v', u', u_3} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_10 : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
⊢ Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
⊢ LE.le (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)

Tactic:
fun _ _ _ hf => (forget C).epi_of_epi_map ((epi_iff_surjective _).2 hf)

Premises used: Iff.mpr, CategoryTheory.epi_iff_surjective, CategoryTheory.Functor.map, CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
⊢ LE.le (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)

Tactic:
fun _ _ _ hf => (forget C).mono_of_mono_map ((mono_iff_injective _).2 hf)

Premises used: Iff.mpr, CategoryTheory.mono_iff_injective, CategoryTheory.Functor.map, CategoryTheory.forget, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
mp :
  Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C) →
    Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
mpr :
  Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) →
    Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C) ↔
    Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
mp :
  ∀ {X Y : C} (f : X ⟶ Y) [Epi f],
    Epi (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
      (Functor.map (forget C (FC := FC) (CC := CC)) f)
⊢ Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
mp :
  Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))
⊢ Epi (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)

Tactic:
rw [epi_iff_surjective]

Premises used: CategoryTheory.epi_iff_surjective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
⊢ MorphismProperty.surjective C (FC := FC) (CC := CC) f

Tactic:
rw [← h] at hf
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
X Y : C
f : X ⟶ Y
hf : MorphismProperty.surjective C (FC := FC) (CC := CC) f
⊢ Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))

Tactic:
hf

Premises used: CategoryTheory.MorphismProperty.surjective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)
X Y : C
f : X ⟶ Y
hf : MorphismProperty.surjective C (FC := FC) (CC := CC) f
⊢ Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))

Tactic:
exact hf
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
mpr : LE.le (α := MorphismProperty.{v, u} C) (epimorphisms C) (MorphismProperty.surjective C (FC := FC) (CC := CC))
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.surjective C (FC := FC) (CC := CC)) (epimorphisms C)

Tactic:
apply le_antisymm (surjective_le_epimorphisms C)

Premises used: le_antisymm, CategoryTheory.ConcreteCategory.surjective_le_epimorphisms
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X : C
mpr : ∀ ⦃Y : C⦄ (f : X ⟶ Y), epimorphisms C f → MorphismProperty.surjective C (FC := FC) (CC := CC) f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), epimorphisms C f → MorphismProperty.surjective C (FC := FC) (CC := CC) f

Tactic:
_
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
⊢ Epi f

Tactic:
have : Epi f := hf
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
this : Epi f
mpr :
  Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))
⊢ MorphismProperty.surjective C (FC := FC) (CC := CC) f

Tactic:
change Function.Surjective ((forget C).map f)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.forget, DFunLike.coe, Function.Surjective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
this : Epi f
mpr :
  Epi (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)
⊢ Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))

Tactic:
rw [← epi_iff_surjective]

Premises used: CategoryTheory.epi_iff_surjective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : epimorphisms C f
this : Epi f
⊢ Epi (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
mp :
  Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C) →
    Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
mpr :
  Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) →
    Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C) ↔
    Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)
mp :
  ∀ {X Y : C} (f : X ⟶ Y) [Mono f],
    Mono (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
      (Functor.map (forget C (FC := FC) (CC := CC)) f)
⊢ Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)
X Y : C
f : X ⟶ Y
hf : monomorphisms C f
mp :
  Function.Injective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))
⊢ Mono (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)

Tactic:
rw [mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)
X Y : C
f : X ⟶ Y
hf : monomorphisms C f
⊢ MorphismProperty.injective C (FC := FC) (CC := CC) f

Tactic:
rw [← h] at hf
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)
X Y : C
f : X ⟶ Y
hf : MorphismProperty.injective C (FC := FC) (CC := CC) f
⊢ Function.Injective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))

Tactic:
hf

Premises used: CategoryTheory.MorphismProperty.injective
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)
X Y : C
f : X ⟶ Y
hf : MorphismProperty.injective C (FC := FC) (CC := CC) f
⊢ Function.Injective (α := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X))
    (β := (fun (X : Type w) ↦ X) (Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) Y))
    (⇑(hom (FC := TypeCat.Fun) (Functor.map (forget C (FC := FC) (CC := CC)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget C).obj X)) → (fun (X : Type w) ↦ X) ((forget C).obj Y))

Tactic:
exact hf
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
mpr : LE.le (α := MorphismProperty.{v, u} C) (monomorphisms C) (MorphismProperty.injective C (FC := FC) (CC := CC))
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)

Tactic:
apply le_antisymm (injective_le_monomorphisms C)

Premises used: le_antisymm, CategoryTheory.ConcreteCategory.injective_le_monomorphisms
-- Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
h : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X : C
mpr : ∀ ⦃Y : C⦄ (f : X ⟶ Y), monomorphisms C f → MorphismProperty.injective C (FC := FC) (CC := CC) f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), monomorphisms C f → MorphismProperty.injective C (FC := FC) (CC := CC) f

Tactic:
_