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₁} C
refine_1 : ∀ (hF : F.Final) (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj 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_2 : ∀ (hF : 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
Tactic: refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.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
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
hF : F.Final
d : D
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
have refine_1 : ∀ (f : StructuredArrow d F), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
Tactic: obtain ⟨f⟩ : Nonempty (StructuredArrow d F) := IsConnected.is_nonempty
-- 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₁} C
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
⊢ ∀ {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 : IsFilteredOrEmpty (AsSmall C)
Tactic: have : IsFilteredOrEmpty (AsSmall.{max u₁ v₁ u₂ v₂} C) := .of_equivalence 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
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
this : IsFilteredOrEmpty (AsSmall 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_2 : ∀ (c' : AsSmall C) (t : { down := c : ULift.{max (max u₁ v₁ u₂ v₂) v₁, u₁} C } ⟶ c')
  (ht :
    Eq (α := obj AsSmall.up d ⟶ (s₁.inverse ⋙ F ⋙ s₂.functor).obj c')
      (map AsSmall.up s ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t)
      (map AsSmall.up s' ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t)),
  ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
Tactic: obtain ⟨c', t, ht⟩ := Functor.Final.exists_coeq_of_locally_small (s₁.inverse ⋙ F ⋙ s₂.functor)
      (AsSmall.up.map s) (AsSmall.up.map 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 : IsCofilteredOrEmpty.{v₁, u₁} C
⊢ F.Initial ↔
    (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
have refine : ∀ (hF : F.Initial),
  (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
Tactic: refine ⟨fun hF => ?_, fun h => initial_of_exists_of_isCofiltered F h.1 h.2⟩
-- 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 : IsCofilteredOrEmpty.{v₁, u₁} C
hF : F.Initial
⊢ (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
have h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
Tactic: obtain ⟨h₁, h₂⟩ := F.op.final_iff_of_isFiltered.mp inferInstance
-- 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 : IsCofilteredOrEmpty.{v₁, u₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
⊢ (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
have h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
Tactic: obtain ⟨h₁, h₂⟩ := F.op.final_iff_of_isFiltered.mp inferInstance
-- 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
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
⊢ (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
have refine_1 : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
Tactic: refine ⟨?_, ?_⟩
-- 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
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
refine_1 : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
have refine_2 : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
Tactic: refine ⟨?_, ?_⟩
-- 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
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
have refine_1 : ∀ (c : Cᵒᵖ) (t : op d ⟶ F.op.obj c), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
Tactic: obtain ⟨c, ⟨t⟩⟩ := h₁ (op 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₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
c : C
s s' : F.obj c ⟶ d
⊢ ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
have refine_2 : ∀ (c' : Cᵒᵖ) (t : op c ⟶ c') (ht : Eq (α := op d ⟶ F.op.obj c') (s.op ≫ F.op.map t) (s'.op ≫ F.op.map t)),
  ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
Tactic: obtain ⟨c', t, ht⟩ := h₂ (Quiver.Hom.op s) (Quiver.Hom.op 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
⊢ F.Final ↔ ∀ (d : D), IsFiltered (StructuredArrow d F)
have refine : F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)
Tactic: refine ⟨?_, fun h => final_of_isFiltered_structuredArrow 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 : IsFilteredOrEmpty.{v₁, u₁} C
⊢ F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)
have rw : ((∀ (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) →
  ∀ (d : D), IsFiltered (StructuredArrow d F)
Tactic: rw [final_iff_of_isFiltered]
-- 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
⊢ F.Initial ↔ ∀ (d : D), IsCofiltered (CostructuredArrow F d)
have refine : F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)
Tactic: refine ⟨?_, fun h => initial_of_isCofiltered_costructuredArrow 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₁} C
⊢ F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)
have rw : ((∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') →
  ∀ (d : D), IsCofiltered (CostructuredArrow F d)
Tactic: rw [initial_iff_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
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
X : C × C
⊢ ∀ (Y : C), IsFiltered (StructuredArrow (C := Under.{v₁, u₁} X.1) Y (Under.forget X.1))
have rw : Final (C := Under.{v₁, u₁} X.1) (Under.forget X.1)
Tactic: rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]
-- 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₁} C
X : C × C
⊢ IsFiltered (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag C))
have this : ∀ (Y : C), IsFiltered (StructuredArrow (C := Under.{v₁, u₁} X.1) Y (Under.forget X.1))
Tactic: haveI : ∀ Y, IsFiltered (StructuredArrow Y (Under.forget X.1)) := by
    rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]
    infer_instance
-- 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
X : C × C
⊢ ∀ (Y : C), IsCofiltered (CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) Y)
have rw : Initial (C := Over.{v₁, u₁} X.1) (Over.forget X.1)
Tactic: rw [← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)]
-- 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 : IsCofilteredOrEmpty.{v₁, u₁} C
X : C × C
⊢ IsCofiltered (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag C) X)
have this : ∀ (Y : C), IsCofiltered (CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) Y)
Tactic: haveI : ∀ Y, IsCofiltered (CostructuredArrow (Over.forget X.1) Y) := by
    rw [← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
⊢ F.Final
have refine_1 : ∀ (x : Discrete PUnit.{u_1 + 1}), ∃ (c : C), Nonempty.{u_1 + 1} (x ⟶ F.obj c)
Tactic: refine final_of_exists_of_isFiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
refine_1 : ∀ (x : Discrete PUnit.{u_1 + 1}), ∃ (c : C), Nonempty.{u_1 + 1} (x ⟶ F.obj c)
⊢ F.Final
have refine_2 : ∀ {x : Discrete PUnit.{u_1 + 1}} {c : C} (x_1 x_2 : x ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), x_1 ≫ F.map t = x_2 ≫ F.map t
Tactic: refine final_of_exists_of_isFiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
⊢ ∃ (c : C), Nonempty.{u_1 + 1} (x ⟶ F.obj c)
have h : Nonempty.{u_1 + 1} (x ⟶ F.obj (Classical.choice sorry))
Tactic: use Classical.choice IsFiltered.nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : x ⟶ F.obj c
⊢ ∃ (c' : C) (t : c ⟶ c'), x_1 ≫ F.map t = x_2 ≫ F.map t
have h : ∃ (t : c ⟶ c), x_1 ≫ F.map t = x_2 ≫ F.map t
Tactic: use c
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : x ⟶ F.obj c
⊢ ∃ (t : c ⟶ c), x_1 ≫ F.map t = x_2 ≫ F.map t
have h : x_1 ≫ F.map (𝟙 c) = x_2 ≫ F.map (𝟙 c)
Tactic: use 𝟙 c
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
⊢ F.Initial
have refine_1 : ∀ (x : Discrete PUnit.{u_1 + 1}), ∃ (c : C), Nonempty.{u_1 + 1} (F.obj c ⟶ x)
Tactic: refine initial_of_exists_of_isCofiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
refine_1 : ∀ (x : Discrete PUnit.{u_1 + 1}), ∃ (c : C), Nonempty.{u_1 + 1} (F.obj c ⟶ x)
⊢ F.Initial
have refine_2 : ∀ {x : Discrete PUnit.{u_1 + 1}} {c : C} (x_1 x_2 : F.obj c ⟶ x), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2
Tactic: refine initial_of_exists_of_isCofiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
⊢ ∃ (c : C), Nonempty.{u_1 + 1} (F.obj c ⟶ x)
have h : Nonempty.{u_1 + 1} (F.obj (Classical.choice sorry) ⟶ x)
Tactic: use Classical.choice IsCofiltered.nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : F.obj c ⟶ x
⊢ ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2
have h : ∃ (t : c ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2
Tactic: use c
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : F.obj c ⟶ x
⊢ ∃ (t : c ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2
have h : F.map (𝟙 c) ≫ x_1 = F.map (𝟙 c) ≫ x_2
Tactic: use 𝟙 c
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
Y : D
⊢ (proj Y T).Final
have refine : ∀ (X : C), IsConnected (StructuredArrow X (proj Y T))
Tactic: refine ⟨fun X => ?_⟩
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
Y : D
X : C
⊢ IsConnected (StructuredArrow X (proj Y T))
have rw : IsConnected (StructuredArrow Y (Under.forget X ⋙ T))
Tactic: rw [isConnected_iff_of_equivalence (ofStructuredArrowProjEquivalence T Y X)]
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
Y : D
⊢ (proj T Y).Initial
have refine : ∀ (X : C), IsConnected (CostructuredArrow (proj T Y) X)
Tactic: refine ⟨fun X => ?_⟩
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
Y : D
X : C
⊢ IsConnected (CostructuredArrow (proj T Y) X)
have rw : IsConnected (CostructuredArrow (Over.forget X ⋙ T) Y)
Tactic: rw [isConnected_iff_of_equivalence (ofCostructuredArrowProjEquivalence T Y X)]
-- 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₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Final
T' : Functor.{v₁, v₃, u₁, u₃} C E
d : D
e : E
u : e ⟶ S.obj d
α : T ⋙ S ⟶ T'
inst_6 : IsIso α
⊢ Final (C := StructuredArrow d T) (D := StructuredArrow e T') (map₂ (F := 𝟭 C) u α)
have this : IsFiltered (StructuredArrow e (T ⋙ S))
Tactic: haveI : IsFiltered (StructuredArrow e (T ⋙ S)) :=
    (T ⋙ S).final_iff_isFiltered_structuredArrow.mp inferInstance e
-- 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₁} C
S S' : D
f : S ⟶ S'
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
⊢ Final (C := StructuredArrow S' T) (map f)
have this : IsIso (𝟙 T)
Tactic: haveI := NatIso.isIso_of_isIso_app (𝟙 T)
-- 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₁} C
S S' : D
f : S ⟶ S'
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
this : IsIso (𝟙 T)
⊢ Final (C := StructuredArrow S' T) (map f)
have this₁ : Final (C := StructuredArrow S' T) (D := StructuredArrow S T) (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T))
Tactic: have : (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T)).Final := by
    apply StructuredArrow.final_map₂_id (S := 𝟭 D) (T := T) (T' := T) f (𝟙 T)
-- 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₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Initial
d : D
e : E
u : S.obj d ⟶ e
⊢ Initial (C := CostructuredArrow T d) (D := CostructuredArrow (T ⋙ S) e) (map₂ (F := 𝟭 C) (𝟙 (T ⋙ S)) u)
have this : IsCofiltered (CostructuredArrow (T ⋙ S) e)
Tactic: have := (T ⋙ S).initial_iff_isCofiltered_costructuredArrow.mp inferInstance e
-- 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: apply Functor.final_of_exists_of_isFiltered
-- 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: apply Functor.final_of_exists_of_isFiltered
-- 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))
⊢ ∃ (c' : (i : α) → I i) (t : c ⟶ c'), f ≫ map (Pi.eval I s) t = g ≫ map (Pi.eval I s) t
have h₂ : Eq (α := d ⟶ obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c t ⟶ c'))
  (f ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))
  (g ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))
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 : α), 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 ⟶ obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c t ⟶ c'))
    (f ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))
    (g ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))
have h₂ : 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))
Tactic: dsimp only [Pi.eval_obj, Pi.eval_map, c't]