awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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
⊢ 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))
have 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)
Tactic: rw [← epi_iff_surjective]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
⊢ 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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))
⊢ 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))
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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)
⊢ Functor.PreservesMonomorphisms.{v, w, u, w + 1} (forget C (FC := FC) (CC := CC))
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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
⊢ 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)
have 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))
Tactic: rw [mono_iff_injective]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (hypothesis)
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
⊢ 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))
have hf₁ : MorphismProperty.injective C (FC := FC) (CC := CC) f
Tactic: rw [← h] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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))
⊢ Eq (α := MorphismProperty.{v, u} C) (MorphismProperty.injective C (FC := FC) (CC := CC)) (monomorphisms C)
have mpr : LE.le (α := MorphismProperty.{v, u} C) (monomorphisms C) (MorphismProperty.injective C (FC := FC) (CC := CC))
Tactic: apply le_antisymm (injective_le_monomorphisms C)
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (hypothesis)
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
⊢ MorphismProperty.injective C (FC := FC) (CC := CC) f
have this : Mono f
Tactic: have : Mono f := hf
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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
⊢ MorphismProperty.injective C (FC := FC) (CC := CC) f
have 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))
Tactic: change Function.Injective ((forget C).map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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
⊢ 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))
have 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)
Tactic: rw [← mono_iff_injective]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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))
⊢ LE.le (α := MorphismProperty.{v, u} C) (epimorphisms C) (MorphismProperty.surjective C (FC := FC) (CC := CC))
have rw : LE.le (α := MorphismProperty.{v, u} C) (epimorphisms C) (epimorphisms C)
Tactic: rw [surjective_eq_epimorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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))
⊢ LE.le (α := MorphismProperty.{v, u} C) (monomorphisms C) (MorphismProperty.injective C (FC := FC) (CC := CC))
have rw : LE.le (α := MorphismProperty.{v, u} C) (monomorphisms C) (monomorphisms C)
Tactic: rw [injective_eq_monomorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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
⊢ Function.Bijective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)
have rw : IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
Tactic: rw [bijective_iff_isIso_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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 ↔
    Function.Bijective.{w + 1, w + 1} (α := CC X) (β := CC Y) (⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y)
have rw : IsIso f ↔ IsIso.{w, w + 1} (X := CC X) (Y := CC Y) (↾(⇑(hom (FC := FC) (CC := CC) f) : (a : CC X) → CC Y))
Tactic: rw [bijective_iff_isIso_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (goal)
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))
have 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
Tactic: refine ⟨fun _ ↦ inferInstance, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.EpiMono (hypothesis)
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 f
have 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)
Tactic: have : IsIso ((forget C).map f) := h
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Forget (goal)
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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x :
  ToType.{w, v_2, u_3, u_4} (FC := FD) (CC := CD)
    (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
⊢ Eq (α := CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) (f ≫ g)) :
          (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Z))
        x :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
          (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
              (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
            x :
          CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
have rw : Eq (α := CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f ≫
            Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
        (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Z))
      x :
    CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
  ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
        (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
            (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
          x :
        CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
    CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
Tactic: rw [Functor.map_comp, CategoryTheory.comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Forget (goal)
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_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))
have 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))
Tactic: change (CategoryTheory.forget₂ _ D) ⋙ (CategoryTheory.forget₂ D E ⋙ CategoryTheory.forget E) = _
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.Forget (goal)
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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x :
  ToType.{w, v_2, u_3, u_4} (FC := FD) (CC := CD)
    (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
⊢ Eq (α := CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((hom (FC := FD) (CC := CD) (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) (f ≫ g)) :
          (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Z))
        x :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
    ((hom (FC := FD) (CC := CD) (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
          (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
        ((hom (FC := FD) (CC := CD) (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
              (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
            x :
          CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
      CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
have rw : Eq (α := CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
  ((hom (FC := FD) (CC := CD)
          (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f ≫
            Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
        (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Z))
      x :
    CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
  ((hom (FC := FD) (CC := CD) (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) g) :
        (a : CD ((forget₂ C D).obj Y)) → CD ((forget₂ C D).obj Z))
      ((hom (FC := FD) (CC := CD) (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f) :
            (a : CD ((forget₂ C D).obj X)) → CD ((forget₂ C D).obj Y))
          x :
        CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Y)) :
    CD (Functor.obj.{v_1, v_2, u_1, u_3} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) Z))
Tactic: rw [Functor.map_comp, CategoryTheory.comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso (hypothesis)
Goal:
C : Type (u + 1)
inst : Category.{v_1, u + 1} C
FC : C → C → Type u
CC : C → Type u
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u, v_1, u + 1, u} C FC (CC := CC)
D : Type (u + 1)
inst_3 : Category.{v_2, u + 1} D
FD : D → D → Type u
CD : D → Type u
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{u, v_2, u + 1, u} D FD (CC := CD)
inst_6 : HasForget₂.{u, v_1, u + 1, u, v_2, u + 1, u} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_7 : Functor.ReflectsIsomorphisms.{v_1, u + 1, u, u + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
i :
  IsIso.{v_2, u + 1} (X :=
    Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f)
⊢ IsIso f
have i' : IsIso (X :=
  Functor.obj.{v_2, u, u + 1, u + 1} (forget D (FC := FD) (CC := CD))
    (Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X))
  (Functor.map (forget D (FC := FD) (CC := CD))
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f))
Tactic: haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
-- Lean 4 proof step from Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso (goal)
Goal:
C : Type (u + 1)
inst : Category.{v_1, u + 1} C
FC : C → C → Type u
CC : C → Type u
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u, v_1, u + 1, u} C FC (CC := CC)
D : Type (u + 1)
inst_3 : Category.{v_2, u + 1} D
FD : D → D → Type u
CD : D → Type u
inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst_5 : ConcreteCategory.{u, v_2, u + 1, u} D FD (CC := CD)
inst_6 : HasForget₂.{u, v_1, u + 1, u, v_2, u + 1, u} C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)
inst_7 : Functor.ReflectsIsomorphisms.{v_1, u + 1, u, u + 1} (forget C (FC := FC) (CC := CC))
X Y : C
f : X ⟶ Y
i :
  IsIso.{v_2, u + 1} (X :=
    Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X)
    (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f)
i' :
  IsIso (X :=
    Functor.obj.{v_2, u, u + 1, u + 1} (forget D (FC := FD) (CC := CD))
      (Functor.obj.{v_1, v_2, u + 1, u + 1} (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) X))
    (Functor.map (forget D (FC := FD) (CC := CD))
      (Functor.map (forget₂ C (FC := FC) (CC := CC) D (FD := FD) (CD := CD)) f))
⊢ IsIso (X := Functor.obj.{v_1, u, u + 1, u + 1} (forget C (FC := FC) (CC := CC)) X)
    (Functor.map (forget C (FC := FC) (CC := CC)) f)
have rwa : IsIso (X :=
  Functor.obj.{v_1, u, u + 1, u + 1}
    (Functor.comp.{v_1, v_2, u, u + 1, u + 1, u + 1} (@HasForget₂.forget₂ _ _ FC CC _ inst_2 _ _ FD CD _ inst_5 _)
      (forget D (FC := FD) (CC := CD)))
    X)
  (Functor.map
    (Functor.comp.{v_1, v_2, u, u + 1, u + 1, u + 1} (@HasForget₂.forget₂ _ _ FC CC _ inst_2 _ _ FD CD _ inst_5 _)
      (forget D (FC := FD) (CC := CD)))
    f)
Tactic: rwa [← @HasForget₂.forget_comp C _ _ _ _ _ D _ _ _ _ _]