mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ PUnit.{u + 1} ≅ colim.obj (⊤_ C ⥤ Type u)

pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ ⊤_ Type u ≅ PUnit.{u + 1}

Tactic:
·

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ PUnit.{u + 1} ≅ colim.obj (⊤_ C ⥤ Type u)
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ ⊤_ Type u ≅ PUnit.{u + 1}

Tactic:
·

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ ⊤_ Type u ≅ PUnit.{u + 1}
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{?u.66 + 1}) colim
⊢ colimit (⊤_ C ⥤ Type u) ≅ PUnit.{u + 1}

pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{?u.66 + 1}) colim
⊢ Types.constPUnitFunctor C ≅ ⊤_ C ⥤ Type u

Tactic:
·

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{?u.66 + 1}) colim
⊢ colimit (⊤_ C ⥤ Type u) ≅ PUnit.{u + 1}
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) colim
⊢ Types.constPUnitFunctor C ≅ ⊤_ C ⥤ Type u

Tactic:
·

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape (Discrete PEmpty.{1}) colim
⊢ Types.constPUnitFunctor C ≅ ⊤_ C ⥤ Type u
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
⊢ ∃ Z x x, True

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ ∃ Z h, η ≫ h = μ ≫ h

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
⊢ ∃ Z x x, True
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ f ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))

pp: case refine_1.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))

Tactic:
·

Goal state after:
case refine_1.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ f ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))

Tactic:
·

Goal state after:
case refine_1.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ ∃ Z h, η ≫ h = μ ≫ h

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ ∃ Z h, η ≫ h = μ ≫ h
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∃ c, Nonempty (op d ⟶ F.op.obj c)

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ {c : Cᵒᵖ} (s s' : op d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t

Tactic:
·

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∃ c, Nonempty (op d ⟶ F.op.obj c)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ {c : Cᵒᵖ} (s s' : op d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ {c : Cᵒᵖ} (s s' : op d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
⊢ F.Final

Tactic:
have := IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
⊢ F.Final
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
⊢ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (x✝ ⟶ F.obj c)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ c' t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (x✝ ⟶ F.obj c)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ c' t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ c' t, x✝¹ ≫ F.map t = x✝ ≫ F.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (F.obj c ⟶ x✝)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ c' t, F.map t ≫ x✝¹ = F.map t ≫ x✝

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (F.obj c ⟶ x✝)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ c' t, F.map t ≫ x✝¹ = F.map t ≫ x✝

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ c' t, F.map t ≫ x✝¹ = F.map t ≫ x✝
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Functor.diag J ⋙ externalProduct F₁ F₂ ≅ F₁ ⊗ F₂

pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)) ≅ c₁.tensor c₂

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Functor.diag J ⋙ externalProduct F₁ F₂ ≅ F₁ ⊗ F₂
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ (Cocone.precompose
          (NatIso.ofComponents (fun x ↦ Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x)) ⋯).inv).obj
      (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)) ≅
    c₁.tensor c₂

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ (Cocone.precompose
          (NatIso.ofComponents (fun x ↦ Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x)) ⋯).inv).obj
      (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)) ≅
    c₁.tensor c₂
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ (d : I s), ∃ c, Nonempty (d ⟶ (Pi.eval I s).obj c)

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ (Pi.eval I s).obj c),
    ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t

Tactic:
·

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ (d : I s), ∃ c, Nonempty (d ⟶ (Pi.eval I s).obj c)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ (Pi.eval I s).obj c),
    ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ (Pi.eval I s).obj c),
    ∃ c' t, s_1 ≫ (Pi.eval I s).map t = s' ≫ (Pi.eval I s).map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ (d : I s), ∃ c, Nonempty ((Pi.eval I s).obj c ⟶ d)

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : (Pi.eval I s).obj c ⟶ d),
    ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'

Tactic:
·

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ (d : I s), ∃ c, Nonempty ((Pi.eval I s).obj c ⟶ d)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : (Pi.eval I s).obj c ⟶ d),
    ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : (Pi.eval I s).obj c ⟶ d),
    ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) →
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

pp: case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ (∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁) →
    (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
·

Goal state after:
case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t) →
    ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
⊢ ∃ j₁, j₂ ≤ f j₁

Tactic:
obtain ⟨j₁, ⟨φ⟩⟩ := h j₂

Goal state after:
case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t
j₂ : J₂
j₁ : J₁
φ : j₂ ⟶ hf.functor.obj j₁
⊢ ∃ j₁, j₂ ≤ f j₁
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ (∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁) →
    (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t

Tactic:
·

Goal state after:
case mpr
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ (∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁) →
    (∀ (d : J₂), ∃ c, Nonempty (d ⟶ hf.functor.obj c)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : d ⟶ hf.functor.obj c), ∃ c' t, s ≫ hf.functor.map t = s' ≫ hf.functor.map t