awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 Y : C
f : X ⟶ Y
hf : monomorphisms C f
⊢ Mono f

Tactic:
have : Mono 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.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : monomorphisms C f
this : Mono f
mpr :
  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))
⊢ MorphismProperty.injective C (FC := FC) (CC := CC) f

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

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.forget, Function.Injective, DFunLike.coe
-- 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 Y : C
f : X ⟶ Y
hf : monomorphisms C f
this : Mono f
mpr :
  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)
⊢ 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:
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 : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
hf : monomorphisms C f
this : 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)

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)
inst_3 rw : 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)

Tactic:
rw [injective_eq_monomorphisms_iff]

Premises used: CategoryTheory.ConcreteCategory.injective_eq_monomorphisms_iff
-- 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))
⊢ Functor.PreservesMonomorphisms.{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)
inst_3 rw : 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)

Tactic:
rw [surjective_eq_epimorphisms_iff]

Premises used: CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms_iff
-- 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))
⊢ 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)
inst_3 : HasStrongEpiMonoFactorisations.{v, u} C
inst_4 : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
inst_5 : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
rw rw₁ : LE.le (α := MorphismProperty.{v, u} C) (epimorphisms C) (epimorphisms C)
⊢ LE.le (α := MorphismProperty.{v, u} C) (epimorphisms C) (MorphismProperty.surjective C (FC := FC) (CC := CC))

Tactic:
rw [surjective_eq_epimorphisms]

Premises used: CategoryTheory.ConcreteCategory.surjective_eq_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)
inst_3 : HasStrongEpiMonoFactorisations.{v, u} C
inst_4 : Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
inst_5 : Functor.PreservesEpimorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
rw rw₁ : LE.le (α := MorphismProperty.{v, u} C) (monomorphisms C) (monomorphisms C)
⊢ LE.le (α := MorphismProperty.{v, u} C) (monomorphisms C) (MorphismProperty.injective C (FC := FC) (CC := CC))

Tactic:
rw [injective_eq_monomorphisms]

Premises used: CategoryTheory.ConcreteCategory.injective_eq_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)
X Y : C
f : X ⟶ Y
inst_3 : Mono f
inst_4 : PreservesLimitsOfShape.{0, 0, v, w, u, w + 1} WalkingCospan (forget C (FC := FC) (CC := CC))
⊢ Function.Injective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)

Tactic:
(mono_iff_injective ((forget C).map f)).mp inferInstance

Premises used: CategoryTheory.mono_iff_injective, inferInstance, CategoryTheory.Functor.map, CategoryTheory.forget, Iff.mp
-- 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
inst_3 : PreservesLimitsOfShape.{0, 0, v, w, u, w + 1} WalkingCospan (forget C (FC := FC) (CC := CC))
⊢ Mono f ↔
    Function.Injective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)

Tactic:
((forget C).mono_map_iff_mono _).symm.trans (mono_iff_injective _)

Premises used: CategoryTheory.mono_iff_injective, CategoryTheory.forget, Iff.trans, CategoryTheory.Functor.mono_map_iff_mono, Iff.symm
-- 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
s : Function.Surjective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)
⊢ Epi f

Tactic:
(forget C).epi_of_epi_map ((epi_iff_surjective ((forget C).map f)).2 s)

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)
X Y : C
f : X ⟶ Y
inst_3 : Epi f
inst_4 : PreservesColimitsOfShape.{0, 0, v, w, u, w + 1} WalkingSpan (forget C (FC := FC) (CC := CC))
⊢ Function.Surjective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)

Tactic:
(epi_iff_surjective ((forget C).map f)).mp inferInstance

Premises used: CategoryTheory.epi_iff_surjective, inferInstance, CategoryTheory.Functor.map, CategoryTheory.forget, Iff.mp
-- 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
inst_3 : PreservesColimitsOfShape.{0, 0, v, w, u, w + 1} WalkingSpan (forget C (FC := FC) (CC := CC))
⊢ Epi f ↔
    Function.Surjective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)

Tactic:
((forget C).epi_map_iff_epi _).symm.trans (epi_iff_surjective _)

Premises used: CategoryTheory.epi_iff_surjective, CategoryTheory.Functor.epi_map_iff_epi, CategoryTheory.forget, Iff.trans, Iff.symm
-- 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
inst_3 : IsIso f
rw : IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
⊢ Function.Bijective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)

Tactic:
rw [bijective_iff_isIso_ofHom]

Premises used: CategoryTheory.bijective_iff_isIso_ofHom
-- 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
inst_3 : IsIso f
⊢ IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

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)
inst_3 : Functor.ReflectsIsomorphisms.{v, u, w, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
rw : IsIso f ↔ IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
⊢ IsIso f ↔
    Function.Bijective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)

Tactic:
rw [bijective_iff_isIso_ofHom]

Premises used: CategoryTheory.bijective_iff_isIso_ofHom
-- 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.ReflectsIsomorphisms.{v, u, w, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
⟨fun _ ↦ inferInstance, fun h ↦ ?_⟩

Premises used: inferInstance, Iff.intro
-- 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.ReflectsIsomorphisms.{v, u, w, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
refine :
  ∀ (h : IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))), IsIso f
⊢ IsIso f ↔ IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
refine ⟨fun _ ↦ inferInstance, fun h ↦ ?_⟩
-- 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.ReflectsIsomorphisms.{v, u, w, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
h : IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
⊢ IsIso (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:
have : IsIso ((forget C).map f) := h
-- 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.ReflectsIsomorphisms.{v, u, w, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
h : IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
this :
  IsIso (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)
⊢ IsIso f

Tactic:
isIso_of_reflects_iso f (forget C)

Premises used: CategoryTheory.isIso_of_reflects_iso, 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.ReflectsIsomorphisms.{v, u, w, w + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
h : IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
this :
  IsIso (X := Functor.obj.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)
⊢ IsIso f

Tactic:
exact isIso_of_reflects_iso f (forget C)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj.{v_1, w, u_1, w + 1} (forget C (FC := FC) (CC := CC)) X ⟶
      Functor.obj.{v_1, w, u_1, w + 1} (forget C (FC := FC) (CC := CC)) Y)
    (Functor.map (forget C (FC := FC) (CC := CC)) f) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
X : C
⊢ Functor.obj.{v_1, w, u_1, w + 1} (forget C (FC := FC) (CC := CC)) X =
    ToType.{w, v_1, u_1, u_2} (FC := FC) (CC := CC) X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h : f = g
x : ToType.{w, v_1, u_1, u_2} (FC := FC) (CC := CC) X
⊢ Eq (α := CC Y) ((ConcreteCategory.hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)

Tactic:
congrFun (congrArg (fun k : X ⟶ Y => (k : ToType X → ToType Y)) h) x

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, congrFun, DFunLike.coe
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
X Y : C
f : X ⟶ Y
x x' : ToType.{w, v_1, u_1, u_2} (FC := FC) (CC := CC) X
h : x = x'
⊢ Eq (α := CC Y) ((ConcreteCategory.hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x' : CC Y)

Tactic:
congrArg (f : ToType X → ToType Y) h

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
D : Type u_3
inst_3 : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_4 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v_2, u_3, u_4} D FD (CC := CD)
inst_6 : HasForget₂.{w, v_1, u_1, u_2, v_2, u_3, u_4} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
⊢ Functor.Faithful.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD))

Tactic:
HasForget₂.forget_comp.faithful_of_comp

Premises used: CategoryTheory.HasForget₂.forget_comp, Eq.faithful_of_comp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
D : Type u_3
inst_3 : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_4 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v_2, u_3, u_4} D FD (CC := CD)
obj : C → D
h_obj :
  ∀ (X : C),
    Functor.obj.{v_2, w, u_3, w + 1} (forget D (FC := FD) (CC := CD)) (obj X) =
      Functor.obj.{v_1, w, u_1, w + 1} (forget C (FC := FC) (CC := CC)) X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq (α :=
      Functor.obj.{v_2, w, u_3, w + 1} (forget D (FC := FD) (CC := CD)) (obj X) ⟶
        Functor.obj.{v_2, w, u_3, w + 1} (forget D (FC := FD) (CC := CD)) (obj Y))
      (Functor.map (forget D (FC := FD) (CC := CD)) (map f)) (β :=
      Functor.obj.{v_1, w, u_1, w + 1} (forget C (FC := FC) (CC := CC)) X ⟶
        Functor.obj.{v_1, w, u_1, w + 1} (forget C (FC := FC) (CC := CC)) Y)
      (Functor.map (forget C (FC := FC) (CC := CC)) f)
⊢ Functor.Faithful.div (forget C (FC := FC) (CC := CC)) (forget D (FC := FD) (CC := CD)) obj h_obj @map @h_map ⋙
      forget D (FC := FD) (CC := CD) =
    forget C (FC := FC) (CC := CC)

Tactic:
apply Functor.Faithful.div_comp

Premises used: CategoryTheory.Functor.Faithful.div_comp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
D : Type u_3
inst_3 : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_4 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v_2, u_3, u_4} D FD (CC := CD)
E : Type u_5
inst_6 : Category.{v_3, u_5} E
FE : E → E → Type u_6
CE : E → Type w
inst_7 : (X Y : E) → FunLike.{u_6 + 1, w + 1, w + 1} (FE X Y) (CE X) (CE Y)
inst_8 : ConcreteCategory.{w, v_3, u_5, u_6} E FE (CC := CE)
inst_9 : HasForget₂.{w, v_1, u_1, u_2, v_2, u_3, u_4} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_10 : HasForget₂.{w, v_2, u_3, u_4, v_3, u_5, u_6} D (FC := FD) (CC := CD) E (FD := FE) (CD := CE)
change :
  Eq (α := Functor.{v_1, w, u_1, w + 1} C (Type w))
    (Functor.comp.{v_1, v_2, w, u_1, u_3, w + 1}
      (CategoryTheory.forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD))
      (Functor.comp.{v_2, v_3, w, u_3, u_5, w + 1}
        (CategoryTheory.forget₂ D (FC := FD) (CC := CD) E (FD := FE) (CD := CE)) (forget E (FC := FE) (CC := CE))))
    (forget C (FC := FC) (CC := CC))
⊢ Eq (α := Functor.{v_1, w, u_1, w + 1} C (Type w))
    (Functor.comp.{v_1, v_3, w, u_1, u_5, w + 1}
      (Functor.comp.{v_1, v_2, v_3, u_1, u_3, u_5}
        (CategoryTheory.forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD))
        (CategoryTheory.forget₂ D (FC := FD) (CC := CD) E (FD := FE) (CD := CE)))
      (forget E (FC := FE) (CC := CE)))
    (forget C (FC := FC) (CC := CC))

Tactic:
change (CategoryTheory.forget₂ _ D) ⋙ (CategoryTheory.forget₂ D E ⋙ CategoryTheory.forget E) = _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.forget₂, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
D : Type u_3
inst_3 : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_4 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v_2, u_3, u_4} D FD (CC := CD)
E : Type u_5
inst_6 : Category.{v_3, u_5} E
FE : E → E → Type u_6
CE : E → Type w
inst_7 : (X Y : E) → FunLike.{u_6 + 1, w + 1, w + 1} (FE X Y) (CE X) (CE Y)
inst_8 : ConcreteCategory.{w, v_3, u_5, u_6} E FE (CC := CE)
inst_9 : HasForget₂.{w, v_1, u_1, u_2, v_2, u_3, u_4} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_10 : HasForget₂.{w, v_2, u_3, u_4, v_3, u_5, u_6} D (FC := FD) (CC := CD) E (FD := FE) (CD := CE)
⊢ Eq (α := Functor.{v_1, w, u_1, w + 1} C (Type w))
    (Functor.comp.{v_1, v_2, w, u_1, u_3, w + 1}
      (CategoryTheory.forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD))
      (Functor.comp.{v_2, v_3, w, u_3, u_5, w + 1}
        (CategoryTheory.forget₂ D (FC := FD) (CC := CD) E (FD := FE) (CD := CE)) (forget E (FC := FE) (CC := CE))))
    (forget C (FC := FC) (CC := CC))

Tactic:
simp only [HasForget₂.forget_comp]

Premises used: CategoryTheory.HasForget₂.forget_comp
-- Module: Mathlib.CategoryTheory.ConcreteCategory.Forget
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_2 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v_1, u_1, u_2} C FC (CC := CC)
D : Type u_3
inst_3 : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst_4 : (X Y : D) → FunLike.{u_4 + 1, w + 1, w + 1} (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{w, v_2, u_3, u_4} D FD (CC := CD)
X Y : C
f : X ⟶ Y
inst_6 : IsIso f
⊢ IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(ConcreteCategory.hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))

Tactic:
((forget C).mapIso (asIso f)).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.forget, CategoryTheory.Functor.mapIso, CategoryTheory.asIso