mathlib-initiative/mathlib-tactics huggingface dataset:
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 C
h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ F.Final

Tactic:
by

Goal state after:
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✝ : IsCofilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ F.Initial

Tactic:
by

Goal state after:
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)
c c' : C
⊢ ∃ Z x x, True

Tactic:
by

Goal state after:
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)
c c' : C
f g : c ⟶ c'
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
by

Goal state after:
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✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ IsCofilteredOrEmpty C

Tactic:
by

Goal state after:
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✝² : IsFiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
⊢ Nonempty C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} J₁
inst✝³ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝² : Category.{v_3, u_3} C₁
inst✝¹ : Category.{v_4, u_4} C₂
inst✝ : Category.{v_5, u_5} C
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
⊢ ∀ ⦃X Y : J₁ × J₂⦄ (f : X ⟶ Y),
    ((uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).map f ≫
        match Y with
        | (j₁, j₂) =>
          (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫ (G.obj (((const J₁).obj c₁.pt).obj j₁)).map (c₂.ι.app j₂)) =
      (match X with
        | (j₁, j₂) =>
          (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫ (G.obj (((const J₁).obj c₁.pt).obj j₁)).map (c₂.ι.app j₂)) ≫
        ((const (J₁ × J₂)).obj ((G.obj c₁.pt).obj c₂.pt)).map f

Tactic:
by

Goal state after:
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✝² : IsCofiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ Nonempty C

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Products.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ (associativity C D E).functor.IsEquivalence

Tactic:
by

Goal state after:
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✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ F.Initial

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Products.Associator

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ (associativity C D E).inverse.IsEquivalence

Tactic:
by

Goal state after:
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 C
c x✝ : C
x : Under c
s s' : x✝ ⟶ (forget c).obj x
⊢ x.hom ≫ IsFiltered.coeqHom s s' = (mk (x.hom ≫ IsFiltered.coeqHom s s')).hom

Tactic:
by

Goal state after:
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 C
c x✝ : C
x : Under c
s s' : x✝ ⟶ (forget c).obj x
⊢ ∃ c' t, s ≫ (forget c).map t = s' ≫ (forget c).map t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
K : Type u₁
inst✝² : Category.{v₁, u₁} K
inst✝¹ : LocallySmall.{w, v, u} J
inst✝ : InitiallySmall J
X : J
⊢ InitiallySmall (Over X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
⊢ ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ FinallySmall J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
⊢ FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
⊢ ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} J₁
inst✝³ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝² : Category.{v_3, u_3} C₁
inst✝¹ : Category.{v_4, u_4} C₂
inst✝ : Category.{v_5, u_5} C
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cone K₁
c₂ : Cone K₂
⊢ ∀ ⦃X Y : J₁ × J₂⦄ (f : X ⟶ Y),
    (((const (J₁ × J₂)).obj ((G.obj c₁.pt).obj c₂.pt)).map f ≫
        match Y with
        | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) =
      (match X with
        | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
        (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).map f

Tactic:
by

Goal state after:
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✝ : IsCofilteredOrEmpty C
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ IsCofiltered.eqHom s s' ≫ x.hom = (mk (IsCofiltered.eqHom s s' ≫ x.hom)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ InitiallySmall J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
P : ObjectProperty J
inst✝ : ObjectProperty.EssentiallySmall.{v, v, u} P
hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)
Q : ObjectProperty J
H : ObjectProperty.Small.{v, v, u} Q
hQ : P ≤ Q.isoClosure
⊢ Small.{v, u}
    (have this := Q;
    ↑this)

Tactic:
by

Goal state after:
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
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ IsCofiltered.eqHom s s' ≫ s = IsCofiltered.eqHom s s' ≫ s'

Tactic:
rw [IsCofiltered.eq_condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv =
    (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2)

Tactic:
by

Goal state after:
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✝ : IsCofilteredOrEmpty C
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ ∃ c' t, (forget c).map t ≫ s = (forget c).map t ≫ s'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s =
    (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
P : ObjectProperty J
inst✝ : ObjectProperty.EssentiallySmall.{v, v, u} P
hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)
⊢ InitiallySmall J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsCofilteredOrEmpty J
⊢ InitiallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫
      (G.obj c₁.pt).map (c₂.ι.app j.2) ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom =
    c₃.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
X : C₀
f : StructuredArrow X (fromFinalModel C₀) := Classical.arbitrary (StructuredArrow X (fromFinalModel C₀))
⊢ ⊤ f.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
X : C₀
⊢ ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
X : C₀
hX : P X
Y : C₀
hY : P Y
Z : C₀
hZ : P Z
f : IsFiltered.max X Y ⟶ Z
⊢ True

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ ∀ (X Y : P.FullSubcategory), ∃ Z x x, True

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ ∀ ⦃X Y : P.FullSubcategory⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ Nonempty P.FullSubcategory

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this : IsFiltered P.FullSubcategory
X : FinalModel C₀
⊢ P ((fromFinalModel C₀).obj X)

Tactic:
by

Goal state after:
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 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' : AsSmall C
t : { down := c } ⟶ c'
ht : AsSmall.up.map s ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t = AsSmall.up.map s' ≫ (s₁.inverse ⋙ F ⋙ s₂.functor).map t
⊢ s₂.functor.map (s ≫ F.map (AsSmall.down.map t)) = s₂.functor.map (s' ≫ F.map (AsSmall.down.map t))

Tactic:
by

Goal state after:
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 C
⊢ F.Final ↔
    (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this✝ : IsFiltered P.FullSubcategory
G : FinalModel C₀ ⥤ P.FullSubcategory :=
  { obj := fun X ↦ { obj := (fromFinalModel C₀).obj X, property := ⋯ },
    map := fun {X Y} f ↦ ObjectProperty.homMk ((fromFinalModel C₀).map f), map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
⊢ Function.Surjective G.obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
⊢ ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : IsFiltered C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : FinallySmall C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered C₀] [FinallySmall C₀],
    ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final
C₀ : Type u
inst✝ : Category.{w, u} C₀
x✝¹ : IsFiltered C₀
x✝ : FinallySmall C₀
⊢ ∃ D x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
by

Goal state after:
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✝ : IsCofilteredOrEmpty C
⊢ F.Initial ↔
    (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'

Tactic:
by

Goal state after:
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 C
⊢ F.Final ↔ ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
by

Goal state after:
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✝ : IsCofilteredOrEmpty C
⊢ F.Initial ↔ ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
by

Goal state after:
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 C
X : C × C
⊢ ∀ (Y : C), IsFiltered (StructuredArrow Y (Under.forget X.1))

Tactic:
by

Goal state after:
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 C
X : C × C
⊢ IsFiltered (StructuredArrow X (Functor.diag C))

Tactic:
by

Goal state after:
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✝ : IsCofilteredOrEmpty C
X : C × C
⊢ ∀ (Y : C), IsCofiltered (CostructuredArrow (Over.forget X.1) Y)

Tactic:
by

Goal state after:
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✝ : IsCofilteredOrEmpty C
X : C × C
⊢ IsCofiltered (CostructuredArrow (Functor.diag C) X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ x✝.as = (F.obj (Classical.choice ⋯)).as

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : FinallySmall C
⊢ ∃ D x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
⊢ F.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ ((const K).obj c.pt).map f ≫ c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : InitiallySmall C
⊢ ∃ D x, ∃ (_ : IsCofiltered D), ∃ F, F.Initial

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ (F.obj (Classical.choice ⋯)).as = x✝.as

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
⊢ (((const J).obj c.pt).map f ≫ (Q j').lift { pt := c.pt, π := { app := fun k ↦ c.π.app (j', k), naturality := ⋯ } }) ≫
      (D.obj j').π.app k =
    ((Q j).lift { pt := c.pt, π := { app := fun k ↦ c.π.app (j, k), naturality := ⋯ } } ≫ D.conePoints.map f) ≫
      (D.obj j').π.app k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
⊢ F.Initial

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: 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₂
X✝ Y✝ : J
x✝ : X✝ ⟶ Y✝
⊢ (Functor.diag J ⋙ externalProduct F₁ F₂).map x✝ ≫ (Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj Y✝)).hom =
    (Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj X✝)).hom ≫ (F₁ ⊗ F₂).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: 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₂
⊢ IsColimit (c₁.tensor c₂)

Tactic:
by

Goal state after:
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 C
T : C ⥤ D
inst✝ : T.Final
Y : D
⊢ (proj Y T).Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones (curry.obj G)
Q : (j : J) → IsLimit (D.obj j)
c : Cone G
x✝¹ j' : J
x✝ : x✝¹ ⟶ j'
⊢ ∀ (j : K),
    (((const J).obj c.pt).map x✝ ≫
          (Q j').lift { pt := c.pt, π := { app := fun k ↦ c.π.app (j', k), naturality := ⋯ } }) ≫
        (D.obj j').π.app j =
      ((Q x✝¹).lift { pt := c.pt, π := { app := fun k ↦ c.π.app (x✝¹, k), naturality := ⋯ } } ≫ D.conePoints.map x✝) ≫
        (D.obj j').π.app j

Tactic:
by

Goal state after: