awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Yoneda (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) B
⊢ Eq (α :=
    ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
      (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
    ((ShiftedHom.opEquiv 1 :
          (a :
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
        ((Equiv.symm (ShiftedHom.opEquiv 1) :
              (a :
                  ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
                    (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1) →
                ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                  (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1)
            (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ :
          ShiftedHom (M := ℤ) (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)
            (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃) 1) :
      ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
        (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
    ((ShiftedHom.opEquiv 1 :
          (a :
              ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
                (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
            ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
              (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
        T.mor₃ :
      ShiftedHom (M := ℤ) (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₃))
        (op (unop (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).obj₁)) 1)
have e_a : (Functor.obj (Equivalence.functor (triangleOpEquivalence C)) (op T)).mor₃ =
  (ShiftedHom.opEquiv 1 :
      (a :
          ShiftedHom (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)
            (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃) 1) →
        ShiftedHom (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₃))
          (op (unop ((triangleOpEquivalence C).functor.obj (op T)).obj₁)) 1)
    T.mor₃
Tactic: rw [Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X ⟶ Y
x x' : X
h : x = x'
⊢ Eq (α := (fun (X : Type u) ↦ X) Y)
    ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) 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) x' :
      (fun (X : Type u) ↦ X) Y)
have rw : Eq (α := (fun (X : Type u) ↦ X) Y)
  ((ConcreteCategory.hom (FC := Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) 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) x' :
    (fun (X : Type u) ↦ X) Y)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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'
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (G.obj j) → F.obj j')
    (Function.comp (β := 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')))
    (Function.comp (β := (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))
have h : ∀ (x : (fun (X : Type u_2) ↦ X) (G.obj j)),
  Eq (α := F.obj j')
    (Function.comp (β := 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'))
      x)
    (Function.comp (β := (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) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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'
x : (fun (X : Type u_2) ↦ X) (G.obj j)
⊢ Eq (α := F.obj j')
    (Function.comp (β := 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'))
      x)
    (Function.comp (β := (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) x)
have h : ∀ (y : F.obj j),
  Eq (α := F.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))
    (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))
Tactic: obtain ⟨y, rfl⟩ := (e j).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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 (α := F.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))
    (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))
have h : 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: apply (e j').injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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.{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')
have 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')
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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.{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')
have 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')
Tactic: simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X → Y
⊢ Mono (↾f) ↔ Function.Injective f
have mp : Mono (↾f) → Function.Injective f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X → Y
mp : Mono (↾f) → Function.Injective f
⊢ Mono (↾f) ↔ Function.Injective f
have mpr : Function.Injective f → Mono (↾f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
h : f x = f x'
⊢ x = x'
have mp : ∀ (h : homOfElement (f x) = homOfElement (f x')), homOfElement x = homOfElement x'
Tactic: rw [← homOfElement_eq_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X → Y
⊢ Function.Injective f → Mono (↾f)
have 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))
Tactic: refine fun H => ⟨fun g g' h => ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.comp_left ?_) x⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
⊢ 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))
have 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)
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X → Y
⊢ Epi (↾f) ↔ Function.Surjective f
have mp : Epi (↾f) → Function.Surjective f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X → Y
mp : Epi (↾f) → Function.Surjective f
⊢ Epi (↾f) ↔ Function.Surjective f
have mpr : Function.Surjective f → Epi (↾f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
have mp : ∀ (g₁ g₂ : Y → Prop) (hg : g₁ ∘ f = g₂ ∘ f), g₁ = g₂
Tactic: refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
⊢ g₁ = g₂
have 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₂)
Tactic: rw [← Equiv.ulift.{u}.symm.injective.comp_left.eq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
⊢ 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₂)
have 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)
Tactic: apply TypeCat.homEquiv.symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
⊢ 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)
have 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₂))
Tactic: apply H
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
⊢ 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₂))
have 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)
Tactic: apply ConcreteCategory.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X → Y
⊢ Function.Surjective f → Epi (↾f)
have 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))
Tactic: refine fun H => ⟨fun g g' h =>  ConcreteCategory.hom_ext _ _ fun x ↦
      congrFun (H.injective_comp_right ?_) x⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
⊢ 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))
have 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)
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
m : Type u → Type v
inst : _root_.Functor m
inst_1 : LawfulFunctor m
α : Type u
⊢ ↾_root_.Functor.map (⇑(Hom.hom (𝟙 α)) : (a : α) → α) = 𝟙 (m α)
have h : ∀ (X : m α),
  Fun.toFun (ConcreteCategory.hom (FC := Fun) (↾_root_.Functor.map (⇑(Hom.hom (𝟙 α)) : (a : α) → α))) X =
    (ConcreteCategory.hom (FC := Fun) (𝟙 (m α))).toFun X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
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
⊢ 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)))
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Basic (goal)
Goal:
X Y : Type u
f : X ⟶ Y
hf : Epi f
⊢ ↾Function.surjInv ⋯ ≫ f = 𝟙 Y
have h : ∀ (x : Y),
  (ConcreteCategory.hom (FC := Fun) (↾Function.surjInv sorry ≫ f)).toFun x =
    (ConcreteCategory.hom (FC := Fun) (𝟙 Y)).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Epimorphisms (goal)
Goal:
x x_1 x_2 x_3 : Type u
b : x ⟶ x_3
r : x_1 ⟶ x_3
t : x_2 ⟶ x_1
l : x_2 ⟶ x
sq : IsPullback t l r b
hr : epimorphisms (Type u) r
⊢ epimorphisms (Type u) l
have simp : ∀ (hr : Function.Surjective (α := x_1) (β := x_3) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : x_1) → x_3)),
  Function.Surjective (α := x_2) (β := x) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : x_2) → x)
Tactic: simp only [epimorphisms.iff, epi_iff_surjective] at hr ⊢
Cleared hypotheses: hr