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 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β
have obtain : ∀ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s)
  (H :
    ∀ (i : Fin (Nat.succ 0).succ.succ),
      Eq (α := ![j₁, j₂, j₃] i ⟶ s)
        (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₁) f₁
              (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₁) f₂
                (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₁) f₃ fun (a : Fin 0) ↦ nomatch a))
              i ≫
            α :
          ![j₁, j₂, j₃] i ⟶ s)
        (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₂) g₁
              (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₂) g₂
                (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₂) g₃ fun (a : Fin 0) ↦ nomatch a))
              i ≫
            β :
          ![j₁, j₂, j₃] i ⟶ s)),
  ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β
Tactic: obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃] (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ nofun)))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ nofun)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ j₄ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
f₄ : j₄ ⟶ k₁
g₄ : j₄ ⟶ k₂
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β
have obtain : ∀ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s)
  (H :
    ∀ (i : Fin (Nat.succ 0).succ.succ.succ),
      Eq (α := ![j₁, j₂, j₃, j₄] i ⟶ s)
        (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₁) f₁
              (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₁) f₂
                (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₁) f₃
                  (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₁) f₄ fun (a : Fin 0) ↦
                    nomatch a)))
              i ≫
            α :
          ![j₁, j₂, j₃, j₄] i ⟶ s)
        (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₂) g₁
              (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₂) g₂
                (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₂) g₃
                  (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₂) g₄ fun (a : Fin 0) ↦
                    nomatch a)))
              i ≫
            β :
          ![j₁, j₂, j₃, j₄] i ⟶ s)),
  ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β
Tactic: obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃, j₄]
      (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ (Fin.cons f₄ nofun))))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ (Fin.cons g₄ nofun))))
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
have obtain : ∀ (l' : C) (k₁l : k₁ ⟶ l') (k₂l : k₂ ⟶ l') (hl : f₂ ≫ k₁l = f₃ ≫ k₂l),
  ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
Tactic: obtain ⟨l', k₁l, k₂l, hl⟩ := span f₂ f₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
have obtain : ∀ (s : C) (ls : l ⟶ s) (l's : l' ⟶ s) (hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's) (hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's),
  ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
Tactic: obtain ⟨s, ls, l's, hs₁, hs₂⟩ := bowtie g₁ (f₁ ≫ k₁l) g₂ (f₄ ≫ k₂l)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
have refine_1 : f₁ ≫ k₁l ≫ l's = g₁ ≫ ls
Tactic: refine ⟨s, k₁l ≫ l's, ls, k₂l ≫ l's, ?_, by simp only [← Category.assoc, hl], ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ l : C
f₁ : j₁ ⟶ k₁
f₂ : j₂ ⟶ k₁
f₃ : j₂ ⟶ k₂
f₄ : j₃ ⟶ k₂
g₁ : j₁ ⟶ l
g₂ : j₃ ⟶ l
l' : C
k₁l : k₁ ⟶ l'
k₂l : k₂ ⟶ l'
hl : f₂ ≫ k₁l = f₃ ≫ k₂l
s : C
ls : l ⟶ s
l's : l' ⟶ s
hs₁ : g₁ ≫ ls = (f₁ ≫ k₁l) ≫ l's
hs₂ : g₂ ≫ ls = (f₄ ≫ k₂l) ≫ l's
refine_1 : f₁ ≫ k₁l ≫ l's = g₁ ≫ ls
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : l ⟶ s) (γ : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = f₃ ≫ γ ∧ f₄ ≫ γ = g₂ ≫ β
have refine_2 : f₄ ≫ k₂l ≫ l's = g₂ ≫ ls
Tactic: refine ⟨s, k₁l ≫ l's, ls, k₂l ≫ l's, ?_, by simp only [← Category.assoc, hl], ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
have this : IsFiltered.{v, u} C
Tactic: have : IsFiltered C := { nonempty := ⟨i⟩ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
have intro : ∀ (val : Fintype I), ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
Tactic: cases nonempty_fintype I
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
val : Fintype I
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
have intro : ∀ (k : C) (fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (X ⟶ k))
  (hk :
    ∀ {X Y : C} (mX : X ∈ insert i (Finset.image j Finset.univ)) (mY : Y ∈ insert i (Finset.image j Finset.univ))
      {f_1 : X ⟶ Y},
      Membership.mem (γ :=
          Finset
            ((X : C) ×'
              (Y : C) ×'
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)))
          (Finset.image
            (fun (x : I) ↦
              PSigma.mk (β := fun (X : C) ↦
                (Y : C) ×'
                  (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                    (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
                i
                (PSigma.mk (β := fun (Y : C) ↦
                  (_ : i ∈ insert i (Finset.image j Finset.univ)) ×'
                    (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ Y))
                  (j x)
                  (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦
                    (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ j x)) sorry
                    (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦ i ⟶ j x) sorry (f x)))))
            Finset.univ)
          (PSigma.mk (β := fun (X : C) ↦
            (Y : C) ×'
              (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
            X
            (PSigma.mk (β := fun (Y : C) ↦
              (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
              Y
              (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j Finset.univ)) ↦
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)) mX
                (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j Finset.univ)) ↦ X ⟶ Y) mY f_1)))) →
        f_1 ≫ fk mY = fk mX),
  ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
Tactic: obtain ⟨k, fk, hk⟩ := sup_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨i, j x, by simp, by simp, f x⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
have intro : ∀ (val : Fintype I), ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
Tactic: classical
  cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := sup_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨i, j x, by simp, by simp, f x⟩)
  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
I : Type u_1
inst_2 : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered.{v, u} C
intro : ∀ (val : Fintype I), ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
⊢ ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
have intro₁ : ∀ (val : Fintype I) (k : C) (fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (X ⟶ k))
  (hk :
    ∀ {X Y : C} (mX : X ∈ insert i (Finset.image j Finset.univ)) (mY : Y ∈ insert i (Finset.image j Finset.univ))
      {f_1 : X ⟶ Y},
      Membership.mem (γ :=
          Finset
            ((X : C) ×'
              (Y : C) ×'
                (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                  (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)))
          (Finset.image
            (fun (x : I) ↦
              PSigma.mk (β := fun (X : C) ↦
                (Y : C) ×'
                  (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                    (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
                i
                (PSigma.mk (β := fun (Y : C) ↦
                  (_ : i ∈ insert i (Finset.image j Finset.univ)) ×'
                    (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ Y))
                  (j x)
                  (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j Finset.univ)) ↦
                    (_ : j x ∈ insert i (Finset.image j Finset.univ)) ×' (i ⟶ j x)) sorry
                    (PSigma.mk (β := fun (x_1 : j x ∈ insert i (Finset.image j Finset.univ)) ↦ i ⟶ j x) sorry (f x)))))
            Finset.univ)
          (PSigma.mk (β := fun (X : C) ↦
            (Y : C) ×'
              (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
            X
            (PSigma.mk (β := fun (Y : C) ↦
              (_ : X ∈ insert i (Finset.image j Finset.univ)) ×'
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y))
              Y
              (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j Finset.univ)) ↦
                (_ : Y ∈ insert i (Finset.image j Finset.univ)) ×' (X ⟶ Y)) mX
                (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j Finset.univ)) ↦ X ⟶ Y) mY f_1)))) →
        f_1 ≫ fk mY = fk mX),
  ∃ (k : C) (fik : i ⟶ k) (g : (x : I) → j x ⟶ k), ∀ (x : I), f x ≫ g x = fik
Tactic: classical
  cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := sup_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨i, j x, by simp, by simp, f x⟩)
  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : SemilatticeInf α
X Y : α
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g
have h : ULift.down.{u, 0} (𝟙 X ≫ f) = ULift.down.{u, 0} (𝟙 X ≫ g)
Tactic: apply ULift.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
X Y : α
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g
have h : ULift.down.{u, 0} (𝟙 X ≫ f) = ULift.down.{u, 0} (𝟙 X ≫ g)
Tactic: apply ULift.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ Eq (α := { as := PUnit.unit : Discrete PUnit.{u_1 + 1} } ⟶ Y)
    ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
        ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
      f)
    ({ down := { down := ⋯ : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
        ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
      g)
have h : Eq (α := PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = Y.as))
  (ULift.down.{u_1, 0}
    ({ down := { down := sorry : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
        ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
      f))
  (ULift.down.{u_1, 0}
    ({ down := { down := sorry : PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as) } :
        ULift.{u_1, 0} (PLift ({ as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as = X.as)) } ≫
      g))
Tactic: apply ULift.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
j : C
x x_1 : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
    ((fun (f : (i : C) ×' (i ⟶ j)) ↦
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
          Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) i ij))
    ((fun (f : (i : C) ×' (i ⟶ j)) ↦
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
          Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) l (li ≫ ij)))
have refine_1 : Superset (α := Set (F.obj j))
  (Set.range (ι := F.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ij)) : (a : F.obj i) → F.obj j))
  (Set.range (ι := F.obj l)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map li ≫ F.map ij)) : (a : F.obj l) → F.obj j))
Tactic: simp_rw [F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
j : C
x x_1 : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
l : C
li : l ⟶ i
lk : l ⟶ k
e : li ≫ ij = lk ≫ kj
⊢ (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
    ((fun (f : (i : C) ×' (i ⟶ j)) ↦
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
          Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) k kj))
    ((fun (f : (i : C) ×' (i ⟶ j)) ↦
        (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
              (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
          Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) l (lk ≫ kj)))
have refine_2 : Superset (α := Set (F.obj j))
  (Set.range (ι := F.obj k) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map kj)) : (a : F.obj k) → F.obj j))
  (Set.range (ι := F.obj l)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map lk ≫ F.map kj)) : (a : F.obj l) → F.obj j))
Tactic: simp_rw [F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
⊢ ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
have obtain : ∀ (t : C) (k₁t : t ⟶ k₁) (k₂t : t ⟶ k₂) (ht : k₁t ≫ f₁ = k₂t ≫ g₁),
  ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
Tactic: obtain ⟨t, k₁t, k₂t, ht⟩ := cospan f₁ g₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
⊢ ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
have obtain : ∀ (s : C) (ts : s ⟶ t) (hs : ts ≫ k₁t ≫ f₂ = ts ≫ k₂t ≫ g₂),
  ∃ (s : C) (α : s ⟶ k₁) (β : s ⟶ k₂), α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
Tactic: obtain ⟨s, ts, hs⟩ := IsCofilteredOrEmpty.cone_maps (k₁t ≫ f₂) (k₂t ≫ g₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v, v₁, u, u₁} C D
R : Functor.{v₁, v, u₁, u} D C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        f :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        g :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
have rw : Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
  (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
          Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
        (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
      (eqHom (R.map f) (R.map g) ≫ R.map f) :
    L.obj (eq (R.map f) (R.map g)) ⟶ Y)
  (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
            Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
          (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
        (eqHom (R.map f) (R.map g)) ≫
      g :
    L.obj (eq (R.map f) (R.map g)) ⟶ Y)
Tactic: rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v, v₁, u, u₁} C D
R : Functor.{v₁, v, u₁, u} D C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
rw :
  Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
            Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
          (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
        (eqHom (R.map f) (R.map g) ≫ R.map f) :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        g :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
⊢ Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        f :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
    (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) X) :
              Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj X) (L.obj (eq (R.map f) (R.map g)) ⟶ X)) :
            (a : eq (R.map f) (R.map g) ⟶ R.obj X) → L.obj (eq (R.map f) (R.map g)) ⟶ X)
          (eqHom (R.map f) (R.map g)) ≫
        g :
      L.obj (eq (R.map f) (R.map g)) ⟶ Y)
have rw₁ : Eq.{v₁ + 1} (α := L.obj (eq (R.map f) (R.map g)) ⟶ Y)
  (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
          Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
        (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
      (eqHom (R.map f) (R.map g) ≫ R.map f) :
    L.obj (eq (R.map f) (R.map g)) ⟶ Y)
  (((Equiv.symm (h.homEquiv (eq (R.map f) (R.map g)) Y) :
          Equiv.{v + 1, v₁ + 1} (eq (R.map f) (R.map g) ⟶ R.obj Y) (L.obj (eq (R.map f) (R.map g)) ⟶ Y)) :
        (a : eq (R.map f) (R.map g) ⟶ R.obj Y) → L.obj (eq (R.map f) (R.map g)) ⟶ Y)
      (eqHom (R.map f) (R.map g) ≫ R.map g) :
    L.obj (eq (R.map f) (R.map g)) ⟶ Y)
Tactic: rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]
-- 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'
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)
have insert : ∀ (S' : C) (w' : ∀ {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: obtain ⟨S', w'⟩ := h
Cleared hypotheses: 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
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {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)
have h : ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (min.{v, u} X S' ⟶ X_1)
Tactic: use min X S'