awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
h₁ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) '' U))
      x →
    x ∈ U
h₂ :
  x ∈ U →
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) '' U))
      x
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) '' U))
      x ↔
    x ∈ U

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
h₁ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun)
              ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
                (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)) :
          (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((⇑(hom (FC := TypeCat.Fun)
                ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
                  (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)) :
            (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) ''
          U))
      x →
    x ∈ U
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) '' U))
      x →
    x ∈ U

Tactic:
rw [←
      show _ = π from
        h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
          WalkingParallelPair.one]

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.Types.coequalizerColimit
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
y : Y
hy : y ∈ U
e' :
  Eq (α := Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            y :
          (coequalizerColimit f g).cocone.pt) :
      Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            x :
          (coequalizerColimit f g).cocone.pt) :
      Z)
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) (β :=
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    (⇑(hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv) :
      (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)

Tactic:
have e'' :=
      (mono_iff_injective
            (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
        inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
y : Y
hy : y ∈ U
e' :
  Eq (α := Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            y :
          (coequalizerColimit f g).cocone.pt) :
      Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            x :
          (coequalizerColimit f g).cocone.pt) :
      Z)
e'' :
  Function.Injective (α := (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) (β :=
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    (⇑(hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv) :
      (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
⊢ x ∈ U

Tactic:
(eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact ?_))).mp hy

Premises used: Set.Mem, Relation.EqvGen.mono, Iff.mp, Quot.eqvGen_exact, Equivalence.eqvGen_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
y : Y
hy : y ∈ U
e' :
  Eq (α := Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            y :
          (coequalizerColimit f g).cocone.pt) :
      Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            x :
          (coequalizerColimit f g).cocone.pt) :
      Z)
e'' :
  Function.Injective (α := (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) (β :=
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    (⇑(hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv) :
      (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
h₁ :
  Eq (α :=
    Quot (α := Y)
      (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)))
    (Quot.mk
      (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
      y)
    (Quot.mk
      (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
      x)
⊢ x ∈ U

Tactic:
refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact ?_))).mp hy

Premises used: Relation.EqvGen.mono, Iff.mp, Quot.eqvGen_exact, Equivalence.eqvGen_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
y : Y
hy : y ∈ U
e' :
  Eq (α := Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            y :
          (coequalizerColimit f g).cocone.pt) :
      Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            x :
          (coequalizerColimit f g).cocone.pt) :
      Z)
e'' :
  Function.Injective (α := (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) (β :=
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    (⇑(hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv) :
      (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
⊢ Eq (α := Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            y :
          (coequalizerColimit f g).cocone.pt) :
      Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            x :
          (coequalizerColimit f g).cocone.pt) :
      Z)

Tactic:
e'
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
y : Y
hy : y ∈ U
e' :
  Eq (α := Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            y :
          (coequalizerColimit f g).cocone.pt) :
      Z)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (coequalizerColimit f g).cocone.pt) → Z)
        ((hom (FC := TypeCat.Fun) (Cofork.π (coequalizerColimit f g).cocone) :
              (a : Y) → (coequalizerColimit f g).cocone.pt)
            x :
          (coequalizerColimit f g).cocone.pt) :
      Z)
e'' :
  Function.Injective (α := (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) (β :=
    (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    (⇑(hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv) :
      (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
        (Quot.mk
          (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
            (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
            (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
          y) :
      (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
    ((hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv :
          (a : (fun (X : Type u) ↦ X) (coequalizerColimit f g).cocone.pt) → (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)
        (Quot.mk
          (Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
            (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
            (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
          x) :
      (fun (X : Type u) ↦ X) (Cofork.ofπ π e).pt)

Tactic:
convert! e'
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
⊢ x ∈ U →
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) '' U))
      x

Tactic:
fun hx => ⟨_, hx, rfl⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U)
lem :
  ∀ (x y : (fun (X : Type u) ↦ X) Y),
    Function.Coequalizer.Rel (α := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x y →
      (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
x : (fun (X : Type u) ↦ X) Y
⊢ x ∈ U →
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((⇑(hom (FC := TypeCat.Fun) π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) '' U))
      x

Tactic:
exact fun hx => ⟨_, hx, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y : Type u
f g : X ⟶ Y
⊢ coequalizer.π f g ≫ (coequalizerIso f g).hom =
    ↾Function.Coequalizer.mk (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)

Tactic:
colimit.isoColimitCocone_ι_hom (coequalizerColimit f g) WalkingParallelPair.one

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, Function.Coequalizer, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom, CategoryTheory.Limits.Types.coequalizerColimit
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y : Type u
f g : X ⟶ Y
⊢ ↾Function.Coequalizer.mk (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
          (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ≫
      (coequalizerIso f g).inv =
    coequalizer.π f g

Tactic:
rfl

Premises used: Function.Coequalizer.desc, TypeCat.Fun.comp, CategoryTheory.Limits.colimit, rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
j j' : J
f : j ⟶ j'
x : F.obj j
⊢ c.ι j'
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        x) =
    c.ι j x

Tactic:
congr_fun (c.ι_naturality f) x

Premises used: congr_fun, CategoryTheory.Functor.CoconeTypes.ι_naturality
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
app : (j : J) → G.obj j → F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    app j' ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')) =
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j')) ∘
        app j
j j' : J
f : j ⟶ j'
rw :
  c.ι j' ∘
      app j' ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')) =
    c.ι j ∘ app j
rw₁ :
  c.ι j' ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j')) ∘
        app j =
    c.ι j ∘ app j
rw₂ :
  (c.ι j' ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))) ∘
      app j =
    c.ι j ∘ app j
rw₃ rw₄ : c.ι j ∘ app j = c.ι j ∘ app j
⊢ (c.ι j' ∘ app j') ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
        (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')) =
    c.ι j ∘ app j

Tactic:
rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]

Premises used: CategoryTheory.Functor.CoconeTypes.ι_naturality, Function.comp_assoc
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
j j' : J
x : F.obj j
y : F.obj j'
⊢ F.ιColimitType j x = F.ιColimitType j' y ↔
    Relation.EqvGen F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)
      (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' y)

Tactic:
Quot.eq

Premises used: CategoryTheory.Functor.ColimitType, CategoryTheory.Functor.ιColimitType, Quot.eq