awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    Insert.insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
insert :
  Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y') (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
    ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')
⊢ Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y')
    ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mX' ≫ f')
    ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
pos :
  ∀ (h : X = X' ∧ Y = Y'),
    Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y') (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
      ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')
neg :
  ∀ (h : ¬(X = X' ∧ Y = Y')),
    Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y') (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
      ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')
⊢ Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y') (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
    ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')

Tactic:
by_cases h : X = X' ∧ Y = Y'
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
h : X = X' ∧ Y = Y'
pos :
  ∀ (mX' : X ∈ O) (mY' : Y ∈ O) {f' : X ⟶ Y}
    (mf' :
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX'
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY' f'))) ∈
        insert
          (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
              (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
          H'),
    Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y) (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
      ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')
⊢ Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y') (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
    ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')

Tactic:
rcases h with ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
mX' : X ∈ O
mY' : Y ∈ O
f' : X ⟶ Y
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX'
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY' f'))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
⊢ Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y) (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
    ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')

Tactic:
grind [eq_condition]

Premises used: CategoryTheory.IsCofiltered.eq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
h : ¬(X = X' ∧ Y = Y')
rw :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    H'
⊢ Eq (α := eq (T' mX ≫ f) (T' mY) ⟶ Y') (eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f')
    ((fun {X_1 : C} (mZ : X_1 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_1)) mY')

Tactic:
rw [@w' _ _ mX' mY' f' _]
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
h : ¬(X = X' ∧ Y = Y')
apply :
  Ne (α := (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
    (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))))
    (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
⊢ PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    H'

Tactic:
apply Finset.mem_of_mem_insert_of_ne mf'

Premises used: Finset.mem_of_mem_insert_of_ne
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
h : ¬(X = X' ∧ Y = Y')
contrapose :
  ∀
    (h :
      Eq (α := (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
        (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
            (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
              (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))))
        (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))),
    X = X' ∧ Y = Y'
⊢ Ne (α := (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
    (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))))
    (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))

Tactic:
contrapose h
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
h :
  Eq (α := (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
    (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X'
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X' ∈ O) ×' (_ : Y ∈ O) ×' (X' ⟶ Y)) Y'
        (PSigma.mk (β := fun (x : X' ∈ O) ↦ (_ : Y' ∈ O) ×' (X' ⟶ Y')) mX'
          (PSigma.mk (β := fun (x : Y' ∈ O) ↦ X' ⟶ Y') mY' f'))))
    (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
obtain :
  ∀
    (mf' :
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        insert
          (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
              (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
          H'),
    X = X ∧ Y = Y
⊢ X = X' ∧ Y = Y'

Tactic:
obtain ⟨rfl, h⟩ := h

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∉
    H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' :
  ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
    PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
        H' →
      T' mX ≫ f = T' mY
mf' :
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
      (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
        (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
          (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))) ∈
    insert
      (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
          (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
            (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f))))
      H'
left : X = X
right : Y = Y
left₁ : X = X
right₁ : Y = Y
left₂ : X = X
right₂ : Y = Y
left₃ : X = X
right₃ : Y = Y
⊢ X = X ∧ Y = Y

Tactic:
trivial