awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ obj (Pi.eval I s) c
c't : (s : α) → (c' : I s) × (c s ⟶ c') :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g))
⊢ Eq (α :=
    d ⟶
      Sigma.fst (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
    (f ≫
      Sigma.snd (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
    (g ≫
      Sigma.snd (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
have h₂ : f ≫ (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)).snd (β := fun (c' : I s) ↦ c s ⟶ c') =
  g ≫ (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)).snd (β := fun (c' : I s) ↦ c s ⟶ c')
Tactic: rw [Function.update_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
⊢ Final (Pi.eval I s)
have h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (d ⟶ obj (Pi.eval I s) c)
Tactic: classical
  apply Functor.final_of_exists_of_isFiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨coeq f g, coeqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using coeq_condition _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (d ⟶ obj (Pi.eval I s) c)
⊢ Final (Pi.eval I s)
have h₂ : ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ obj (Pi.eval I s) c),
  ∃ (c' : (i : α) → I i) (t : c ⟶ c'), s_1 ≫ map (Pi.eval I s) t = s' ≫ map (Pi.eval I s) t
Tactic: classical
  apply Functor.final_of_exists_of_isFiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨coeq f g, coeqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using coeq_condition _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
⊢ Initial (Pi.eval I s)
have h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (obj (Pi.eval I s) c ⟶ d)
Tactic: apply Functor.initial_of_exists_of_isCofiltered
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (obj (Pi.eval I s) c ⟶ d)
⊢ Initial (Pi.eval I s)
have h₂ : ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : obj (Pi.eval I s) c ⟶ d),
  ∃ (c' : (i : α) → I i) (t : c' ⟶ c), map (Pi.eval I s) t ≫ s_1 = map (Pi.eval I s) t ≫ s'
Tactic: apply Functor.initial_of_exists_of_isCofiltered
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : obj (Pi.eval I s) c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g))
⊢ ∃ (c' : (i : α) → I i) (t : c' ⟶ c), map (Pi.eval I s) t ≫ f = map (Pi.eval I s) t ≫ g
have h₂ : Eq (α := (obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c' ⟶ c t)) ⟶ d)
  ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ f)
  ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ g)
Tactic: refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : obj (Pi.eval I s) c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g))
⊢ Eq (α := (obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c' ⟶ c t)) ⟶ d)
    ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ f)
    ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ g)
have h₂ : Eq.{v₂ + 1} (α :=
  Sigma.fst (β := fun (c' : I s) ↦ c' ⟶ c s)
      (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
        (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
        (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ⟶
    d)
  (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s)
      (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
        (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
        (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ≫
    f)
  (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s)
      (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
        (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
        (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ≫
    g)
Tactic: dsimp only [Pi.eval_obj, Pi.eval_map, c't]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : obj (Pi.eval I s) c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g))
⊢ Eq.{v₂ + 1} (α :=
    Sigma.fst (β := fun (c' : I s) ↦ c' ⟶ c s)
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ⟶
      d)
    (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s)
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ≫
      f)
    (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s)
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ≫
      g)
have h₂ : Eq.{v₂ + 1} (α :=
  Sigma.fst (β := fun (c' : I s) ↦ c' ⟶ c s) (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g)) ⟶ d)
  (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s) (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g)) ≫ f)
  (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s) (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g)) ≫ g)
Tactic: rw [Function.update_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
⊢ Initial (Pi.eval I s)
have h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (obj (Pi.eval I s) c ⟶ d)
Tactic: classical
  apply Functor.initial_of_exists_of_isCofiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c' ⟶ c s)) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨eq f g, eqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using eq_condition _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (obj (Pi.eval I s) c ⟶ d)
⊢ Initial (Pi.eval I s)
have h₂ : ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : obj (Pi.eval I s) c ⟶ d),
  ∃ (c' : (i : α) → I i) (t : c' ⟶ c), map (Pi.eval I s) t ≫ s_1 = map (Pi.eval I s) t ≫ s'
Tactic: classical
  apply Functor.initial_of_exists_of_isCofiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c' ⟶ c s)) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨eq f g, eqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using eq_condition _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Preorder J₁
inst_1 : Preorder J₂
inst_2 : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
have rw : ((∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
      ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t) ↔
  ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
Tactic: rw [Functor.final_iff_of_isFiltered]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Preorder J₁
inst_1 : Preorder J₂
inst_2 : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
        ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t) ↔
    ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
have mp : ((∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
      ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t) →
  ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Preorder J₁
inst_1 : Preorder J₂
inst_2 : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
mp :
  ((∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
        ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t) →
    ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
⊢ ((∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
        ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t) ↔
    ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
have mpr : (∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁) →
  (∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
      ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Preorder J₁
inst_1 : Preorder J₂
inst_2 : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)
right :
  ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
    ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
⊢ ∃ (j₁ : J₁), j₂ ≤ f j₁
have mp : ∀ (j₁ : J₁) (φ : j₂ ⟶ hf.functor.obj j₁), ∃ (j₁ : J₁), j₂ ≤ f j₁
Tactic: obtain ⟨j₁, ⟨φ⟩⟩ := h j₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Preorder J₁
inst_1 : Preorder J₂
inst_2 : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
⊢ (∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
      ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t
have mpr : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Preorder J₁
inst_1 : Preorder J₂
inst_2 : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
mpr : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)
⊢ (∀ (d : J₂), ∃ (c : J₁), Nonempty.{u_2 + 1} (d ⟶ hf.functor.obj c)) ∧
    ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
      ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t
have mpr₁ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c),
  ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Preorder J₁
inst_1 : Preorder J₂
inst_2 : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁
j₂ : J₂
⊢ ∃ (c : J₁), Nonempty.{u_2 + 1} (j₂ ⟶ hf.functor.obj c)
have mpr : ∀ (j₁ : J₁) (h₁ : j₂ ≤ f j₁), ∃ (c : J₁), Nonempty.{u_2 + 1} (j₂ ⟶ hf.functor.obj c)
Tactic: obtain ⟨j₁, h₁⟩ := h j₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.FinallySmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
⊢ ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F : Functor.{w, w, u, u} D C₀),
    F.Final
have hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
Tactic: have hP (X : C₀) : ∃ (Y : C₀) (hY : P Y), Nonempty (X ⟶ Y) := by
      let f : StructuredArrow X (fromFinalModel.{w} C₀) := Classical.arbitrary _
      exact ⟨_, ObjectProperty.strictMap_obj _ _ (X := f.right) (by tauto), ⟨f.hom⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.FinallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
X : C₀
hX : P X
Y : C₀
hY : P Y
⊢ ∃ (Z : P.FullSubcategory) (x : ObjectProperty.FullSubcategory.mk (P := P) X hX ⟶ Z) (x :
    ObjectProperty.FullSubcategory.mk (P := P) Y hY ⟶ Z), True
have obtain : ∀ (Z : C₀) (hZ : P Z) (f : IsFiltered.max.{w, u} X Y ⟶ Z),
  ∃ (Z : P.FullSubcategory) (x : ObjectProperty.FullSubcategory.mk (P := P) X hX ⟶ Z) (x :
    ObjectProperty.FullSubcategory.mk (P := P) Y hY ⟶ Z), True
Tactic: obtain ⟨Z, hZ, ⟨f⟩⟩ := hP (max X Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.FinallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
X : C₀
hX : P X
Y : C₀
hY : P Y
f₁ f₂ : X ⟶ Y
⊢ ∃ (Z : P.FullSubcategory) (h : ObjectProperty.FullSubcategory.mk (P := P) Y hY ⟶ Z),
    Eq (α := ObjectProperty.FullSubcategory.mk (P := P) X hX ⟶ Z) ({ hom := f₁ } ≫ h) ({ hom := f₂ } ≫ h)
have obtain : ∀ (Z : C₀) (hZ : P Z) (g : coeq f₁ f₂ ⟶ Z),
  ∃ (Z : P.FullSubcategory) (h : ObjectProperty.FullSubcategory.mk (P := P) Y hY ⟶ Z),
    Eq (α := ObjectProperty.FullSubcategory.mk (P := P) X hX ⟶ Z) ({ hom := f₁ } ≫ h) ({ hom := f₂ } ≫ h)
Tactic: obtain ⟨Z, hZ, ⟨g⟩⟩ := hP (coeq f₁ f₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.FinallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
⊢ Nonempty.{u + 1} P.FullSubcategory
have obtain : ∀ (X : C₀) (hX : P X), Nonempty.{w + 1} (Classical.arbitrary C₀ ⟶ X) → Nonempty.{u + 1} P.FullSubcategory
Tactic: obtain ⟨X, hX, _⟩ := hP (Classical.arbitrary C₀)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.FinallySmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
⊢ ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F : Functor.{w, w, u, u} D C₀),
    F.Final
have this : IsFiltered.{w, u} P.FullSubcategory
Tactic: have : IsFiltered P.FullSubcategory :=
      { nonempty := by
          obtain ⟨X, hX, _⟩ := hP (Classical.arbitrary C₀)
          exact ⟨X, hX⟩
        cocone_objs := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩
          obtain ⟨Z, hZ, ⟨f⟩⟩ := hP (max X Y)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (leftToMax X Y ≫ f),
            ObjectProperty.homMk (rightToMax X Y ≫ f), by tauto⟩
        cocone_maps := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩ ⟨f₁ : X ⟶ Y⟩ ⟨f₂ : X ⟶ Y⟩
          obtain ⟨Z, hZ, ⟨g⟩⟩ := hP (coeq f₁ f₂)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.FinallySmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : FinallySmall.{w, v, u} C
C₀ : Type u
inst_4 : Category.{w, u} C₀
inst_5 : IsFiltered.{w, u} C₀
inst_6 : FinallySmall.{w, w, u} C₀
P : ObjectProperty.{w, u} C₀ := ObjectProperty.strictMap (C := FinalModel C₀) ⊤ (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)
this : IsFiltered.{w, u} P.FullSubcategory
G : Functor.{w, w, w, u} (FinalModel C₀) P.FullSubcategory :=
  { obj := fun (X : FinalModel C₀) ↦ ObjectProperty.FullSubcategory.mk (P := P) (Functor.obj (fromFinalModel C₀) X) ⋯,
    map := fun {X Y : FinalModel C₀} (f : X ⟶ Y) ↦ ObjectProperty.homMk (P := P) (Functor.map (fromFinalModel C₀) f),
    map_id := ⋯, map_comp := ⋯ }
⊢ ∃ (D : Type u) (_ : Small.{w, u} D) (x : Category.{w, u} D) (_ : IsFiltered.{w, u} D) (F : Functor.{w, w, u, u} D C₀),
    F.Final
have this₁ : (G ⋙ P.ι).Final
Tactic: have : (G ⋙ P.ι).Final := inferInstanceAs (fromFinalModel.{w} C₀).Final