awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
⊢ Nonempty.{v + 1} (min.{v, u} X S' ⟶ Y)
have h : ∀ (nm : Y ∉ O') (mY : Y ∈ insert Y O'), Nonempty.{v + 1} (min.{v, u} Y S' ⟶ Y)
Tactic: obtain rfl | h := eq_or_ne Y X
Cleared hypotheses: X, nm, mY
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S' ⟶ X)
Y : C
mY : Y ∈ insert X O'
h : ∀ (nm : Y ∉ O') (mY : Y ∈ insert Y O'), Nonempty.{v + 1} (min.{v, u} Y S' ⟶ Y)
⊢ Nonempty.{v + 1} (min.{v, u} X S' ⟶ Y)
have h₁ : ∀ (h : Y ≠ X), Nonempty.{v + 1} (min.{v, u} X S' ⟶ Y)
Tactic: obtain rfl | h := eq_or_ne Y X
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)
have empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (S ⟶ X)
Tactic: induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (S ⟶ X)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)
have insert : ∀ (X : C) (O' : Finset C) (nm : X ∉ O') (h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S ⟶ X)),
  ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (S ⟶ X_1)
Tactic: induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)
have empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (S ⟶ X)
Tactic: classical
  induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (S ⟶ X)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)
have insert : ∀ (X : C) (O' : Finset C) (nm : X ∉ O') (h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (S ⟶ X)),
  ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (S ⟶ X_1)
Tactic: classical
  induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use min X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨minToLeft _ _⟩
    · exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      Membership.mem (γ := Finset ((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)))) →
        T mX ≫ f = T mY
have empty : ∀ (S : C) (f : ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (S ⟶ X)),
  ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      Membership.mem (γ := Finset ((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)))) →
        T mX ≫ f = T mY
Tactic: obtain ⟨S, f⟩ := inf_objs_exists O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofiltered.{v, u} C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
h' : (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)
H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
nmf : h' ∉ H'
h'' :
  ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {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
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {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))) ∈
          insert h' H' →
        T mX ≫ f = T mY
have insert : ∀ (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)),
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
              (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
                (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
          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' →
        T mX_1 ≫ f_1 = T mY_1
Tactic: obtain ⟨X, Y, mX, mY, f⟩ := h'
Cleared hypotheses: h', nmf
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (S ⟶ X)),
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
              (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
                (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
          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' →
        T mX_1 ≫ f_1 = T mY_1
have insert : ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
  PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
        (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
          (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
            (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
      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_1)
      ((fun {X_2 : C} (mZ : X_2 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_2)) mX_1 ≫ f_1)
      ((fun {X_2 : C} (mZ : X_2 ∈ O) ↦ (eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ : eq (T' mX ≫ f) (T' mY) ⟶ X_2)) mY_1)
Tactic: refine ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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'
⊢ 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')
have 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')
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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'
⊢ 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')
have 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')
Tactic: by_cases h : X = X' ∧ Y = Y'
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: by_cases h : X = X' ∧ Y = Y'
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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'
⊢ 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')
have 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')
Tactic: rcases h with ⟨rfl, rfl⟩
Cleared hypotheses: X', Y', mX', mY', f', mf', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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')
⊢ 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')
have 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'
Tactic: rw [@w' _ _ mX' mY' f' _]