awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
Goal:
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
⊢ Eq (α := (fun (X : Type u) ↦ X) X → s.pt)
    (Function.comp (β := (fun (X : Type u) ↦ X) Y)
      (⇑(hom (FC := TypeCat.Fun) s.π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) s.pt)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
    (Function.comp (β := (fun (X : Type u) ↦ X) Y)
      (⇑(hom (FC := TypeCat.Fun) s.π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) s.pt)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
have h : ∀ (x : (fun (X : Type u) ↦ X) X),
  Eq (α := s.pt)
    (Function.comp (β := (fun (X : Type u) ↦ X) Y)
      (⇑(hom (FC := TypeCat.Fun) s.π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) s.pt)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x)
    (Function.comp (β := (fun (X : Type u) ↦ X) Y)
      (⇑(hom (FC := TypeCat.Fun) s.π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) s.pt)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
Goal:
X Y Z : Type u
f g : X ⟶ Y
x : Cofork f g
x_1 :
  (Cofork.ofπ
        (↾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))
        ⋯).pt ⟶
    x.pt
hm :
  (Cofork.ofπ
          (↾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))
          ⋯).π ≫
      x_1 =
    x.π
⊢ x_1 =
    (fun (s : Cofork f g) ↦
        ↾Function.Coequalizer.desc
            (⇑(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)
            (⇑(hom (FC := TypeCat.Fun) s.π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) s.pt) ⋯)
      x
have h : ∀
  (x_2 :
    (Cofork.ofπ
        (↾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))
        sorry).pt),
  (hom (FC := TypeCat.Fun) x_1).toFun x_2 =
    TypeCat.Fun.toFun
      (@hom _ types TypeCat.Fun _ _ _ _ _
        ((fun (s : Cofork f g) ↦
            ↾Function.Coequalizer.desc
                (⇑(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)
                (⇑(hom (FC := TypeCat.Fun) s.π) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) s.pt) sorry)
          x))
      x_2
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
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)
x : X
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) Y) U
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x :
        (fun (X : Type u) ↦ X) Y) ↔
    Membership.mem (α := (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) x :
        (fun (X : Type u) ↦ X) Y)
have change : Membership.mem (γ := 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) x ↔
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U) x
Tactic: change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
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)
x : X
⊢ Membership.mem (γ := 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) x ↔
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U) x
have rw : Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U) x ↔
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
    ((⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) ⁻¹' U) x
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (hypothesis)
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)
⊢ 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) =
    U
have 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)
Tactic: have lem : ∀ x y, Function.Coequalizer.Rel f g x y → (x ∈ U ↔ y ∈ U) := by
    rintro _ _ ⟨x⟩
    change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
    rw [H]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (hypothesis)
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)
⊢ 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) =
    U
have eqv : _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U
Tactic: have eqv : _root_.Equivalence fun x y => x ∈ U ↔ y ∈ U := by
    aesop (add safe constructors _root_.Equivalence)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
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
⊢ 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) =
    U
have h₁ : ∀ (x : (fun (X : Type u) ↦ X) Y),
  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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
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
⊢ 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
have 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
Tactic: rw [←
      show _ = π from
        h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
          WalkingParallelPair.one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (hypothesis)
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)
⊢ x ∈ U
have 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)
Tactic: have e'' :=
      (mono_iff_injective
            (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
        inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
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
have 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)
Tactic: refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact ?_))).mp hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
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'
⊢ (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
have 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
Tactic: rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
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
⊢ (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
have 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
Tactic: rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
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
⊢ (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
have 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
Tactic: rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]