mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
⊢ ∀ (G : C),
    P G →
      ∀
        (g₁ g₂ :
          G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
        g₁ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) =
            g₂ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) →
          g₁ = g₂

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
⊢ ∀ (G : C),
    P G →
      ∀
        (g₁ g₂ :
          G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
        g₁ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) =
            g₂ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) →
          g₁ = g₂
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
hP : P.IsSeparating ∧ ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
⊢ (ObjectProperty.ofObj fun T ↦ freeYoneda T.1 ↑T.2).IsSeparating ∧
    ∀ ⦃X Y : Cᵒᵖ ⥤ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i) →
        IsIso i

Tactic:
]

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
hP : P.IsSeparating ∧ ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
⊢ (ObjectProperty.ofObj fun T ↦ freeYoneda T.1 ↑T.2).IsSeparating ∧
    ∀ ⦃X Y : Cᵒᵖ ⥤ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i) →
        IsIso i
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
⊢ ∀ (X : Cᵒᵖ), IsIso (i.app X)

Tactic:
]

Goal state after:
A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
⊢ ∀ (X : Cᵒᵖ), IsIso (i.app X)
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ ∃ P,
    ∃ (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Cᵒᵖ ⥤ A) κ

Tactic:
]

Goal state after:
A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ ∃ P,
    ∃ (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Cᵒᵖ ⥤ A) κ
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
this : IsCardinalPresentable G κ
⊢ IsCardinalPresentable (freeYoneda (X, ⟨G, hG⟩).1 ↑(X, ⟨G, hG⟩).2) κ

Tactic:
]

Goal state after:
A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
X : C
G : A
hG : P G
this : IsCardinalPresentable G κ
⊢ IsCardinalPresentable (freeYoneda (X, ⟨G, hG⟩).1 ↑(X, ⟨G, hG⟩).2) κ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ modelCategoryQuillen.J.rlp.llp Λ[n, i].ι

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ modelCategoryQuillen.J.rlp.llp Λ[n, i].ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: ⊢ (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts).retracts

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: ⊢ ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
    ((coproducts.{u, u, u + 1} modelCategoryQuillen.J).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
a : (P.colimitsCardinalClosure κ).ι.obj obj ⟶ X := coequalizer.desc ((E.coconeAt X).ι.app j) ⋯
ψ : j ⟶ CostructuredArrow.mk a := CostructuredArrow.homMk (homMk (coequalizer.π φ₁ φ₂)) ⋯
⊢ φ₁ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a) = φ₂ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a)

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this✝¹ : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
this✝ : IsCardinalPresentable G κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ₁ φ₂ : G ⟶ Φ.obj j
h : (φ₁ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X) = (φ₂ ≫ colimit.ι Φ j) ≫ colimit.desc Φ (E.coconeAt X)
this : (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape WalkingParallelPair
obj : (P.colimitsCardinalClosure κ).FullSubcategory := { obj := coequalizer φ₁ φ₂, property := ⋯ }
a : (P.colimitsCardinalClosure κ).ι.obj obj ⟶ X := coequalizer.desc ((E.coconeAt X).ι.app j) ⋯
ψ : j ⟶ CostructuredArrow.mk a := CostructuredArrow.homMk (homMk (coequalizer.π φ₁ φ₂)) ⋯
⊢ φ₁ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a) = φ₂ ≫ Φ.map ψ ≫ colimit.ι Φ (CostructuredArrow.mk a)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
h✝ : P.IsRegular
⊢ anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
h✝ : P.IsRegular
⊢ anodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions.rlp.llp Λ[n, i].ι

Tactic:
]

Goal state after:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions.rlp.llp Λ[n, i].ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp

Tactic:
]

Goal state after:
⊢ modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ IsSmall.{u, u, u + 1} (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι)

Tactic:
]

Goal state after:
⊢ IsSmall.{u, u, u + 1} (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts =
    (transfiniteCompositions.{u, u, u + 1} (coproducts.{u, u, u + 1} innerHornInclusions).pushouts).retracts

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts =
    ((coproducts.{u, u, u + 1} innerHornInclusions).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case hx
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ ↑((ConcreteCategory.hom ((f.b j).app (op ⦋s₁.dim⦌))) s₁.simplex) ∈ X.nonDegenerate s₁.dim

Tactic:
]

Goal state after:
case hx
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ ↑((ConcreteCategory.hom ((f.b j).app (op ⦋s₁.dim⦌))) s₁.simplex) ∈ X.nonDegenerate s₁.dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
w✝ : P.IsRegular
h✝ : P.IsInner
⊢ innerAnodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
left✝ : Mono f
P : (Subcomplex.range f).Pairing
w✝ : P.IsRegular
h✝ : P.IsInner
⊢ innerAnodyneExtensions (Subfunctor.toRange f ≫ (Subfunctor.range f).ι)
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable X κ
⊢ P.colimitsCardinalClosure κ X

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable X κ
⊢ P.colimitsCardinalClosure κ X
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable X κ
⊢ (P.colimitsCardinalClosure κ).retractClosure X

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable X κ
⊢ (P.colimitsCardinalClosure κ).retractClosure X
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case hy
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ ↑((ConcreteCategory.hom ((f.b j).app (op ⦋s₂.dim⦌))) s₂.simplex) ∈ X.nonDegenerate s₂.dim

Tactic:
]

Goal state after:
case hy
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
s₂ : (range (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left✝ : Epi g₂
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₂.op)) s₂.simplex = x₂
⊢ ↑((ConcreteCategory.hom ((f.b j).app (op ⦋s₂.dim⦌))) s₂.simplex) ∈ X.nonDegenerate s₂.dim
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : IsCardinalLocallyPresentable C κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : IsCardinalLocallyPresentable C κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.m j)))
h :
  (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₁ =
    (ConcreteCategory.hom (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.map (f.b j))) x₂
s₁ : (range (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left✝¹ : Epi g₁
hg₁ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₁
left✝ : Epi g₁
hg₂ : (ConcreteCategory.hom ((f.sigmaStdSimplex j).map g₁.op)) s₁.simplex = x₂
⊢ x₂ = x₂

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) (⨆ i, f.filtration ↑i)

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) (⨆ i, f.filtration ↑i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) (⨆ i, f.filtration i)

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁵ : LinearOrder ι
f : P.RankFunction ι
inst✝⁴ : P.IsProper
inst✝³ : SuccOrder ι
inst✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) (⨆ i, f.filtration i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ IsEmpty { f // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Q ◁ h = Q ◁ h

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Q ◁ inl ≫ Q ◁ hP.desc h k w = Q ◁ h

Tactic:
by
  rw [← MonoidalCategory.whiskerLeft_comp, IsPushout.inl_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Q ◁ k = Q ◁ k

Tactic:
]

Goal state after: