awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Final
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))
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)
⊢ 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:
rw [Function.update_self]

Premises used: Function.update_self
-- Module: Mathlib.CategoryTheory.Filtered.Final
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) (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:
simpa using eq_condition _ _

Premises used: CategoryTheory.IsCofiltered.eq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Final
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)
h₂ 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'
⊢ Initial (Pi.eval I 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 _ _

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered, CategoryTheory.Pi.eval_obj, CategoryTheory.IsCofiltered.eq_condition, Function.update_self, CategoryTheory.Pi.eval_map
-- Module: Mathlib.CategoryTheory.Filtered.Final
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
inst_2 : IsFiltered.{v₂, u₂} D
⊢ Final (Prod.fst C D)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Filtered.Final
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
inst_2 : IsFiltered.{v₁, u₁} C
⊢ Final (Prod.snd C D)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Filtered.Final
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
inst_2 : IsCofiltered.{v₂, u₂} D
⊢ Initial (Prod.fst C D)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Filtered.Final
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
inst_2 : IsCofiltered.{v₁, u₁} C
⊢ Initial (Prod.snd C D)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Filtered.Final
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
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₁
⊢ hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ (j₁ : J₁), j₂ ≤ f j₁

Tactic:
rw [Functor.final_iff_of_isFiltered]

Premises used: CategoryTheory.Functor.final_iff_of_isFiltered
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₁
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
⊢ ((∀ (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
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₂
mp : ∀ (j₁ : J₁) (φ : j₂ ⟶ hf.functor.obj j₁), ∃ (j₁ : J₁), j₂ ≤ f j₁
⊢ ∃ (j₁ : J₁), j₂ ≤ f j₁

Tactic:
obtain ⟨j₁, ⟨φ⟩⟩ := h j₂
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₂ ⟶ hf.functor.obj j₁
⊢ ∃ (j₁ : J₁), j₂ ≤ f j₁

Tactic:
⟨j₁, leOfHom φ⟩

Premises used: Exists.intro, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₂ ⟶ hf.functor.obj j₁
⊢ ∃ (j₁ : J₁), j₂ ≤ f j₁

Tactic:
exact ⟨j₁, leOfHom φ⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
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)
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
⊢ (∀ (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
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₂
mpr : ∀ (j₁ : J₁) (h₁ : j₂ ≤ f j₁), ∃ (c : J₁), Nonempty.{u_2 + 1} (j₂ ⟶ hf.functor.obj c)
⊢ ∃ (c : J₁), Nonempty.{u_2 + 1} (j₂ ⟶ hf.functor.obj c)

Tactic:
obtain ⟨j₁, h₁⟩ := h j₂
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₂
j₁ : J₁
h₁ : j₂ ≤ f j₁
⊢ ∃ (c : J₁), Nonempty.{u_2 + 1} (j₂ ⟶ hf.functor.obj c)

Tactic:
⟨j₁, ⟨homOfLE h₁⟩⟩

Premises used: Nonempty.intro, CategoryTheory.homOfLE, Exists.intro
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₂
j₁ : J₁
h₁ : j₂ ≤ f j₁
⊢ ∃ (c : J₁), Nonempty.{u_2 + 1} (j₂ ⟶ hf.functor.obj c)

Tactic:
exact ⟨j₁, ⟨homOfLE h₁⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₁
mpr : ∀ (s s' : d ⟶ hf.functor.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t
⊢ ∀ (s s' : d ⟶ hf.functor.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
_
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₁
s : d ⟶ hf.functor.obj c
mpr : ∀ (s' : d ⟶ hf.functor.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t
⊢ ∀ (s' : d ⟶ hf.functor.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
_
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₁
s s' : d ⟶ hf.functor.obj c
⊢ ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
⟨c, 𝟙 _, rfl⟩

Premises used: CategoryTheory.CategoryStruct.id, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Filtered.Final
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₁
s s' : d ⟶ hf.functor.obj c
⊢ ∃ (c' : J₁) (t : c ⟶ c'), s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
exact ⟨c, 𝟙 _, rfl⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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₀)
X : C₀
f : StructuredArrow (C := FinalModel C₀) X (fromFinalModel C₀) :=
  Classical.arbitrary (StructuredArrow (C := FinalModel C₀) X (fromFinalModel C₀))
⊢ ⊤ f.right

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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₀)
X : C₀
f : StructuredArrow (C := FinalModel C₀) X (fromFinalModel C₀) :=
  Classical.arbitrary (StructuredArrow (C := FinalModel C₀) X (fromFinalModel C₀))
⊢ ∃ (Y : C₀) (_ : P Y), Nonempty.{w + 1} (X ⟶ Y)

Tactic:
exact ⟨_, ObjectProperty.strictMap_obj _ _ (X := f.right) (by tauto), ⟨f.hom⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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₀)
⊢ ∀ (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⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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
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
⊢ ∃ (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)

Premises used: CategoryTheory.IsFiltered.max
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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 : C₀
hZ : P Z
f : IsFiltered.max.{w, u} X Y ⟶ Z
⊢ True

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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 : 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:
exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (leftToMax X Y ≫ f),
            ObjectProperty.homMk (rightToMax X Y ≫ f), by tauto⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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
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)
⊢ ∃ (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₂)

Premises used: CategoryTheory.IsFiltered.coeq
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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 : 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:
⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.IsFiltered.coeqHom, CategoryTheory.IsFiltered.coeq_condition_assoc, CategoryTheory.ObjectProperty.hom_ext, CategoryTheory.ObjectProperty.homMk, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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 : 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:
exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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)
obtain : ∀ (X : C₀) (hX : P X), Nonempty.{w + 1} (Classical.arbitrary C₀ ⟶ X) → Nonempty.{u + 1} P.FullSubcategory
⊢ Nonempty.{u + 1} P.FullSubcategory

Tactic:
obtain ⟨X, hX, _⟩ := hP (Classical.arbitrary C₀)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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
h : Nonempty.{w + 1} (Classical.arbitrary C₀ ⟶ X)
⊢ Nonempty.{u + 1} P.FullSubcategory

Tactic:
⟨X, hX⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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
h : Nonempty.{w + 1} (Classical.arbitrary C₀ ⟶ X)
⊢ Nonempty.{u + 1} P.FullSubcategory

Tactic:
exact ⟨X, hX⟩
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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)
⊢ 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 _ _ _) ⟩ }
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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
X : FinalModel C₀
⊢ P (Functor.obj (fromFinalModel C₀) X)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Filtered.FinallySmall
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 := ⋯ }
⊢ (G ⋙ P.ι).Final

Tactic:
have : (G ⋙ P.ι).Final := inferInstanceAs (fromFinalModel.{w} C₀).Final