awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : X ⟶ yp
hab :
  ∀ (j : C) (snd : (W : C) × (j ⟶ W)),
    CategoryStruct.comp (Y := ∏ᶜ fun (a : md) ↦ Y)
        (Pi.lift ((fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) f))
        (Pi.π (fun (a : md) ↦ Y) (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) j snd)) =
      f ≫ Pi.π (fun (a : md) ↦ Y) (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) j snd)
⊢ Pi.lift ((fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) f) = f

Tactic:
ext ⟨j⟩
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : X ⟶ yp
j : C
snd : (W : C) × (j ⟶ W)
⊢ CategoryStruct.comp (Y := ∏ᶜ fun (a : md) ↦ Y)
      (Pi.lift ((fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) f))
      (Pi.π (fun (a : md) ↦ Y) (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) j snd)) =
    f ≫ Pi.π (fun (a : md) ↦ Y) (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) j snd)

Tactic:
simp [yp]
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
apply : (X ⟶ yp) → md
apply₁ :
  Function.Injective (β := md) fun (f : X ⟶ yp) ↦
    Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) X (Sigma.mk (β := fun (W : C) ↦ X ⟶ W) yp f)
⊢ #(X ⟶ yp) ≤ α

Tactic:
apply Cardinal.mk_le_of_injective _

Premises used: Cardinal.mk_le_of_injective
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : X ⟶ yp
⊢ md

Tactic:
exact ⟨_, _, f⟩
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f g : X ⟶ yp
k :
  Eq.{u + 1} (α := md)
    ((fun (f : X ⟶ yp) ↦
        (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) X (Sigma.mk (β := fun (W : C) ↦ X ⟶ W) yp f) :
          (Z : C) × (W : C) × (Z ⟶ W)))
      f)
    ((fun (f : X ⟶ yp) ↦
        (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) X (Sigma.mk (β := fun (W : C) ↦ X ⟶ W) yp f) :
          (Z : C) × (W : C) × (Z ⟶ W)))
      g)
refl : f = f
⊢ f = g

Tactic:
cases k
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : X ⟶ yp
⊢ f = f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.SmallComplete
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
by_contra by_contra₁ by_contra₂ : ∀ (r_ne_s : ¬r = s), False
by_contra₃ by_contra₄ by_contra₅ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)), False
by_contra₆ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
by_contra₇ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
by_contra₈ : (r_ne_s : ¬r = s) → (z : 2 ≤ #(X ⟶ Y)) → Cardinal.{u}
by_contra₉ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    let yp : C := ∏ᶜ fun (x : md) ↦ Y;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
by_contra₁₀ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    let yp : C := ∏ᶜ fun (x : md) ↦ Y;
    #(X ⟶ yp) ≤ α
by_contra₁₁ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    let yp : C := ∏ᶜ fun (x : md) ↦ Y;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
by_contra₁₂ by_contra₁₃ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    let yp : C := ∏ᶜ fun (x : md) ↦ Y;
    #(X ⟶ yp) ≤ α
⊢ r = s

Tactic:
classical
      by_contra r_ne_s
      have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
      let md := Σ Z W : C, Z ⟶ W
      let α := #md
      apply not_le_of_gt (Cardinal.cantor α)
      let yp : C := ∏ᶜ fun _ : md => Y
      apply _root_.trans _ _
      · exact #(X ⟶ yp)
      · apply le_trans (Cardinal.power_le_power_right z)
        rw [Cardinal.power_def]
        apply le_of_eq
        rw [Cardinal.eq]
        refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
        · intro f
          ext k
          simp [yp]
        · intro f
          ext ⟨j⟩
          simp [yp]
      · apply Cardinal.mk_le_of_injective _
        · intro f
          exact ⟨_, _, f⟩
        · rintro f g k
          cases k
          rfl

Premises used: trans, Cardinal.eq, Cardinal.mk_le_of_injective, le_of_eq, Cardinal.power_def
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
h :
  ∀ (x : X),
    Eq (α :=
      Function.Coequalizer (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
        (⇑(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))
      (TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (f ≫
            ↾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)
      (TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (g ≫
            ↾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)
⊢ Eq (α :=
    X ⟶
      Function.Coequalizer (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
        (⇑(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))
    (f ≫
      ↾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))
    (g ≫
      ↾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:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
x : X
⊢ Eq (α :=
    Function.Coequalizer (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
      (⇑(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))
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (f ≫
          ↾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)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (g ≫
          ↾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)

Tactic:
Function.Coequalizer.condition f g x

Premises used: CategoryTheory.ConcreteCategory.hom, Function.Coequalizer.condition, Function.Coequalizer.mk, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
x : X
⊢ Eq (α :=
    Function.Coequalizer (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
      (⇑(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))
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (f ≫
          ↾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)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (g ≫
          ↾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)

Tactic:
exact Function.Coequalizer.condition f g x

Premises used: CategoryTheory.ConcreteCategory.hom, Function.Coequalizer.condition, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
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)
⊢ 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))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
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:
ConcreteCategory.congr_hom s.condition x

Premises used: CategoryTheory.Limits.Cofork.condition, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
s : Cofork f g
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:
exact ConcreteCategory.congr_hom s.condition x

Premises used: CategoryTheory.Limits.Cofork.condition, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
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.π
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))
          ⋯).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) ⋯)
            x))
        x_2
⊢ 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

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
x_1 : Cofork f g
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))
        ⋯).pt ⟶
    x_1.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_2 =
    x_1.π
x :
  (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
⊢ (hom (FC := TypeCat.Fun) x_2).toFun x =
    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) ⋯)
          x_1))
      x

Tactic:
Quot.inductionOn x (congr_hom hm)

Premises used: Quot.inductionOn
-- Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers
Goal:
X Y Z : Type u
f g : X ⟶ Y
x_1 : Cofork f g
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))
        ⋯).pt ⟶
    x_1.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_2 =
    x_1.π
x :
  (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
⊢ (hom (FC := TypeCat.Fun) x_2).toFun x =
    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) ⋯)
          x_1))
      x

Tactic:
exact Quot.inductionOn x (congr_hom hm)
-- 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)
x : X
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
⊢ 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)

Tactic:
change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U
-- 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)
x : X
rw 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
⊢ 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:
rw [H]
-- 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)
⊢ ∀ (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]
-- 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)
⊢ _root_.Equivalence fun (x y : Y) ↦ x ∈ U ↔ y ∈ U

Tactic:
aesop (add safe constructors _root_.Equivalence)

Premises used: Equivalence
-- 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)
⊢ _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)
-- 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
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
⊢ 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

Tactic:
ext