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
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
⊢ ∃ (Z : C) (h : c' ⟶ Z), f ≫ h = g ≫ h
have obtain : ∀ (c₀ : C) (f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀), ∃ (Z : C) (h : c' ⟶ Z), f ≫ h = g ≫ h
Tactic: obtain ⟨c₀, ⟨f₀⟩⟩ := h (IsFiltered.coeq (F.map f) (F.map g))
-- 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
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ ∃ (Z : C) (h : c' ⟶ Z), f ≫ h = g ≫ h
have refine : F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) =
  F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))
Tactic: refine ⟨_, F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀), F.map_injective ?_⟩
-- 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
inst_2 : IsCofilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ IsCofilteredOrEmpty.{v₁, u₁} C
have suffices : IsFilteredOrEmpty.{v₁, u₁} Cᵒᵖ
Tactic: suffices IsFilteredOrEmpty Cᵒᵖ from isCofilteredOrEmpty_of_isFilteredOrEmpty_op _
-- 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
inst_2 : IsCofilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ IsFilteredOrEmpty.{v₁, u₁} Cᵒᵖ
have refine : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
Tactic: refine IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)
-- 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
inst_2 : IsCofilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
d : Dᵒᵖ
⊢ ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
have obtain : ∀ (c : C) (f : F.obj c ⟶ unop d), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
Tactic: obtain ⟨c, ⟨f⟩⟩ := h d.unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (hypothesis)
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
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
⊢ Nonempty C
have this : Nonempty D
Tactic: have : Nonempty D := IsFiltered.nonempty
-- 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
inst_2 : IsFiltered.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : Nonempty D
⊢ Nonempty C
have obtain : ∀ (c : C), Nonempty C
Tactic: obtain ⟨c, -⟩ := h (Classical.arbitrary D)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (hypothesis)
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
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ Nonempty C
have this : Nonempty D
Tactic: have : Nonempty D := IsCofiltered.nonempty
-- 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
inst_2 : IsCofiltered.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
this : Nonempty D
⊢ Nonempty C
have obtain : ∀ (c : C), Nonempty C
Tactic: obtain ⟨c, -⟩ := h (Classical.arbitrary D)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (hypothesis)
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 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
⊢ F.Final
have this : IsFilteredOrEmpty.{v₁, u₁} C
Tactic: have := IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h
-- 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
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
⊢ F.Final
have refine : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
Tactic: refine Functor.final_of_exists_of_isFiltered F h (fun {d c} s s' => ?_)
-- 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
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
d : D
c : C
s s' : d ⟶ F.obj c
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
have obtain : ∀ (c₀ : C) (f : IsFiltered.coeq s s' ⟶ F.obj c₀), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
Tactic: obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.coeq s s')
-- 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
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
have refine : s ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f)) = s' ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f))
Tactic: refine ⟨c₀, F.preimage (IsFiltered.coeqHom s s' ≫ f), ?_⟩
-- 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
inst_2 : IsCofilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ F.Initial
have suffices : F.op.Final
Tactic: suffices Final F.op from initial_of_final_op _
-- 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
inst_2 : IsCofilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ F.op.Final
have refine : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
Tactic: refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)
-- 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
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
⊢ ∃ (c' : Under.{v₁, u₁} c) (t : x ⟶ c'), s ≫ Functor.map (forget c) t = s' ≫ Functor.map (forget c) t
have h : ∃ (t : x ⟶ mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')),
  s ≫ Functor.map (forget c) t = s' ≫ Functor.map (forget c) t
Tactic: use mk (x.hom ≫ IsFiltered.coeqHom s s')
-- 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
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
⊢ ∃ (t : x ⟶ mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')),
    s ≫ Functor.map (forget c) t = s' ≫ Functor.map (forget c) t
have h : Eq (α := x_1 ⟶ obj (forget c) (mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')))
  (s ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') sorry))
  (s' ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') sorry))
Tactic: use homMk (IsFiltered.coeqHom s s') (by simp)
-- 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
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
⊢ Eq (α := x_1 ⟶ obj (forget c) (mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')))
    (s ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') ⋯))
    (s' ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') ⋯))
have h : Eq (α := x_1 ⟶ IsFiltered.coeq s s') (s ≫ IsFiltered.coeqHom s s') (s' ≫ IsFiltered.coeqHom s s')
Tactic: simp only [forget_obj, mk_right, forget_map, homMk_right]
-- 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
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
⊢ Eq (α := x_1 ⟶ IsFiltered.coeq s s') (s ≫ IsFiltered.coeqHom s s') (s' ≫ IsFiltered.coeqHom s s')
have h : Eq (α := x_1 ⟶ IsFiltered.coeq s s') (s' ≫ IsFiltered.coeqHom s s') (s' ≫ IsFiltered.coeqHom s s')
Tactic: rw [IsFiltered.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
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
⊢ ∃ (c' : Over.{v₁, u₁} c) (t : c' ⟶ x), Functor.map (forget c) t ≫ s = Functor.map (forget c) t ≫ s'
have h : ∃ (t : mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom) ⟶ x),
  Functor.map (forget c) t ≫ s = Functor.map (forget c) t ≫ s'
Tactic: use mk (IsCofiltered.eqHom s s' ≫ x.hom)
-- 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
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
⊢ ∃ (t : mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom) ⟶ x),
    Functor.map (forget c) t ≫ s = Functor.map (forget c) t ≫ s'
have h : Eq (α := obj (forget c) (mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom)) ⟶ x_1)
  (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') sorry) ≫ s)
  (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') sorry) ≫ s')
Tactic: use homMk (IsCofiltered.eqHom s s') (by simp)
-- 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
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
⊢ Eq (α := obj (forget c) (mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom)) ⟶ x_1)
    (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') ⋯) ≫ s)
    (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') ⋯) ≫ s')
have h : Eq (α := IsCofiltered.eq s s' ⟶ x_1) (IsCofiltered.eqHom s s' ≫ s) (IsCofiltered.eqHom s s' ≫ s')
Tactic: simp only [forget_obj, mk_left, forget_map, homMk_left]
-- 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
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
⊢ Eq (α := IsCofiltered.eq s s' ⟶ x_1) (IsCofiltered.eqHom s s' ≫ s) (IsCofiltered.eqHom s s' ≫ s')
have h : Eq (α := IsCofiltered.eq s s' ⟶ x_1) (IsCofiltered.eqHom s s' ≫ s') (IsCofiltered.eqHom s s' ≫ s')
Tactic: rw [IsCofiltered.eq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
have a : Eq (α := PUnit.{v₁ + 1})
  (((colimitCompCoyonedaIso F d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v₁ + 1})
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
            (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
              (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
          s :
        (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))) :
    PUnit.{v₁ + 1})
  (((colimitCompCoyonedaIso F d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v₁ + 1})
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
            (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
              (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
          s' :
        (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))) :
    PUnit.{v₁ + 1})
Tactic: apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (hypothesis)
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
have this : Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
        (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
          (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
      s :
    (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
        (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
          (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
      s' :
    (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
Tactic: have : colimit.ι (F ⋙ coyoneda.obj (op d)) c s = colimit.ι (F ⋙ coyoneda.obj (op d)) c s' := by
    apply (Final.colimitCompCoyonedaIso F d).toEquiv.injective
    subsingleton
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
have obtain : ∀ (c' : C) (t₁ t₂ : c ⟶ c')
  (h :
    Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
            (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
              (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
          s :
        (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
            (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
              (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
          s' :
        (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))),
  ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
Tactic: obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h :
  Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s' :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
have refine : Eq (α := d ⟶ F.obj (IsFiltered.coeq t₁ t₂)) (s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
  (s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
Tactic: refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h :
  Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s' :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
| s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂)
have rw : s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂)
Tactic: rw [IsFiltered.coeq_condition t₁ t₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type v₁
inst : Category.{v₁, v₁} C
D : Type u₂
inst_1 : Category.{v₁, u₂} D
F : C ⥤ D
inst_2 : IsFilteredOrEmpty C
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  Eq (α := (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) c) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
        s' :
      (fun (X : Type v₁) ↦ X) (colimit (F ⋙ obj coyoneda (op d))))
c' : C
t₁ t₂ : c ⟶ c'
h :
  Eq (α := (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₁) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map t₂) :
          (a : (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c)) →
            (fun (X : Type v₁) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj c'))
        s' :
      (fun (X : Type v₁) ↦ X) ((F ⋙ obj coyoneda (op d)).obj c'))
⊢ Eq (α := d ⟶ F.obj (IsFiltered.coeq t₁ t₂)) (s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
    (s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
have conv_rhs : Eq (α := d ⟶ F.obj (IsFiltered.coeq t₁ t₂)) (s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂))
  (s' ≫ F.map (t₂ ≫ IsFiltered.coeqHom t₁ t₂))
Tactic: conv_rhs => rw [IsFiltered.coeq_condition t₁ 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
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
⊢ F.Final ↔
    (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
have refine_1 : ∀ (hF : F.Final) (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
Tactic: refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩