mathlib-initiative/mathlib-tactics huggingface dataset:
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
j : ι
s : (range (f.m j)).N
⊢ ∃ c, s = Cell.type₁ f c ∨ s = Cell.type₂ f c

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ c.ιSigmaStdSimplex ≫ f.b j = c.mapToSucc

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
⊢ f.t j ≫ homOfLE ⋯ = f.m j ≫ f.b j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
⊢ Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → (X ⟶ Y) ↪ Ω := fun X Y ↦ ⋯.some
e : C ≃ ↑(Set.range ⇑f₁) := Equiv.ofInjective ⇑f₁ ⋯
x✝¹ x✝ : ↑(Set.range ⇑f₁)
⊢ ↑(Set.range ⇑(f₂ (e.symm x✝¹) (e.symm x✝))) ≃ (e.symm x✝¹ ⟶ e.symm x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
⊢ ∃ S, Nonempty (categoryFamily κ S ≌ C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderIsomorphisms

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsCardinalClosure κ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
S : SmallCategoryCardinalLT κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape (SmallCategoryCardinalLT.categoryFamily κ S)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
J : Type u'
inst✝ : Category.{v', u'} J
hJ : HasCardinalLT (Arrow J) κ
⊢ (P.colimitsCardinalClosure κ).IsClosedUnderColimitsOfShape J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
hQ : ∀ (J : Type w) [inst : SmallCategory J], HasCardinalLT (Arrow J) κ → Q.IsClosedUnderColimitsOfShape J
h : P ≤ Q
⊢ P.colimitsCardinalClosure κ ≤ Q

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
⊢ (P.colimitsCardinalClosure κ).IsStableUnderRetracts

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
⊢ b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
⊢ ∃ j' α, (ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (ConcreteCategory.hom (c.pt.map (X.map α))) x₂

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsLimit (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.mapCone (PullbackCone.mk (f.t j) (f.m j) ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
hY : F.DenseAt Y
G : C ⥤ D
e : F ≅ G
⊢ (Cocone.precompose
          (((CostructuredArrow.mapNatIso e.symm).functor.associator (CostructuredArrow.proj F Y) F).symm ≪≫
              ((CostructuredArrow.mapNatIso e.symm).functor ⋙ CostructuredArrow.proj F Y).isoWhiskerLeft e).inv).obj
      (Cocone.whisker (CostructuredArrow.mapNatIso e.symm).functor
        ((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y)) ≅
    (LeftExtension.mk (𝟭 D) G.rightUnitor.inv).coconeAt Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
hY : F.DenseAt Y
⊢ F.isDenseAt.IsClosedUnderIsomorphisms

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
⊢ IsColimit (c.pt.mapCocone cX)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
⊢ F.isDenseAt = G.isDenseAt

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : IsLimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape K (Type w')
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), (F.obj k).IsCardinalAccessible κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hcX : IsColimit cX
⊢ Nonempty (IsColimit (c.pt.mapCocone cX))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
k : Kᵒᵖ
⊢ ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
this : ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
⊢ HasCardinalLT (Arrow Kᵒᵖ) κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
⊢ IsCardinalPresentable c.pt κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
e : C ≌ ShrinkHoms.{u} C := ShrinkHoms.equivalence C
k : K
⊢ IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
⊢ Set.range ⇑(ConcreteCategory.hom ((homOfLE ⋯).app d)) ⊔ Set.range ⇑(ConcreteCategory.hom ((f.b j).app d)) = Set.univ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : LocallySmall.{w, v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
inst✝² : HasLimitsOfShape Kᵒᵖ (Type w)
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
⊢ IsCardinalPresentable c.pt κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : HasLimitsOfShape Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow J) κ
⊢ (isCardinalPresentable C κ).colimitsOfShape J ≤ isCardinalPresentable C κ

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ f.mapN (Cell.type₁ f c) = { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ f.mapN (Cell.type₂ f c) = { dim := (↑c.s).dim, simplex := (↑c.s).simplex }

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
s : (range (f.m j)).N
⊢ (f.mapN s).simplex ∈ X.nonDegenerate (f.mapN s).dim

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : P.p c.s = P.p c'.s
⊢ c = c'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
⊢ ⊤.map F ≤ isCardinalPresentable C κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
ip : F.DenseAt X
e : CostructuredArrow F X ≌ SmallModel.{w, v', max u' v} (CostructuredArrow F X) :=
  equivSmallModel (CostructuredArrow F X)
j : SmallModel.{w, v', max u' v} (CostructuredArrow F X)
⊢ ⊤ ((CostructuredArrow.proj F X).obj (e.symm.functor.obj j))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsDense
Y : D
⊢ G.isDenseAt Y

Tactic:
by

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✝ : NoMaxOrder ι
j : ι
⊢ Function.Injective f.mapN

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
G : C' ⥤ C
inst✝ : G.IsEquivalence
⊢ (G ⋙ F).IsDense ↔ F.IsDense

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : LocallySmall.{w, v, u} C
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : EssentiallySmall.{w, v', u'} J
F : J ⥤ C
inst✝³ : F.IsDense
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (j : J), IsCardinalPresentable (F.obj j) κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow F X) κ
X : C
⊢ ∃ J_1 x, ∃ (_ : IsCardinalFiltered J_1 κ), (⊤.map F).colimitsOfShape J_1 X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
G : D ⥤ C'
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsDense ↔ F.IsDense

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
inst✝ : F.IsDense
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (restrictedULiftYoneda F).map a₁✝ = (restrictedULiftYoneda F).map a₂✝
X : C
p : F.obj X ⟶ X✝
⊢ (StructuredArrow.hom (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).app X ≫
      (StructuredArrow.right (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).map p ≫ a₁✝ =
    (StructuredArrow.hom (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).app X ≫
      (StructuredArrow.right (LeftExtension.mk (𝟭 D) F.rightUnitor.inv)).map p ≫ a₂✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
inst✝ : F.IsDense
Y Z : D
f : (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj Z
g₁ g₂ : CostructuredArrow F Y
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.proj F Y ⋙ F).map φ ≫ ((ConcreteCategory.hom (f.app (op g₂.left))) { down := g₂.hom }).down =
    ((ConcreteCategory.hom (f.app (op g₁.left))) { down := g₁.hom }).down ≫
      ((const (CostructuredArrow F Y)).obj Z).map φ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
inst✝⁴ : ObjectProperty.EssentiallySmall.{w, v, u} P
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : P.ι.IsDense
inst✝¹ : LocallySmall.{w, v, u} C
hP : P ≤ isCardinalPresentable C κ
inst✝ : ∀ (X : C), IsCardinalFiltered (CostructuredArrow P.ι X) κ
⊢ P.IsCardinalFilteredGenerator κ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasColimitsOfSize.{w, w, v, u} C
X : C
J : Type w
x✝ : SmallCategory J
K : J ⥤ CostructuredArrow (P.colimitsCardinalClosure κ).ι X
hJ : HasCardinalLT (Arrow J) κ
⊢ Cocone K

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
inst✝ : F.IsDense
Y Z : D
f : (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj Z
⊢ ∃ a, (restrictedULiftYoneda F).map a = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
⊢ ∀ ⦃X Y_1 : Cᵒᵖ⦄ (f : X ⟶ Y_1),
    (((restrictedULiftYoneda F).obj Y).map f ≫
        match Y_1 with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) =
      (match X with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) }) ≫
        ((restrictedULiftYoneda F).obj s.pt).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
⊢ (restrictedULiftYoneda F).map j.hom ≫ φ s = (restrictedULiftYoneda F).map (s.ι.app j)

Tactic:
by

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
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ (f₁ ≫ Φ.map (IsFiltered.leftToMax j₁ j₂)) ≫ colimit.ι Φ (IsFiltered.max j₁ j₂) = g₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
h : (restrictedULiftYoneda F).FullyFaithful
Y : D
φ : (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) →
  (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
  fun s ↦
    {
      app := fun x ↦
        match x with
        | op X =>
          ↾fun x ↦
            match x with
            | { down := x } => { down := s.ι.app (CostructuredArrow.mk x) },
      naturality := ⋯ }
hφ :
  ∀ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) (j : CostructuredArrow F Y),
    (restrictedULiftYoneda F).map j.hom ≫ φ s = (restrictedULiftYoneda F).map (s.ι.app j)
s : Cocone (CostructuredArrow.proj F Y ⋙ F)
j : CostructuredArrow F Y
⊢ (restrictedULiftYoneda F).map (((LeftExtension.mk (𝟭 D) F.rightUnitor.inv).coconeAt Y).ι.app j ≫ h.preimage (φ s)) =
    (restrictedULiftYoneda F).map (s.ι.app j)

Tactic:
by

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
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
this : IsCardinalPresentable G κ
j₁ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₁ : G ⟶ Φ.obj j₁
hf₁ : f₁ ≫ (colimit.cocone Φ).ι.app j₁ = g₁
j₂ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
f₂ : G ⟶ Φ.obj j₂
hf₂ : f₂ ≫ (colimit.cocone Φ).ι.app j₂ = g₂
⊢ (f₂ ≫ Φ.map (IsFiltered.rightToMax j₁ j₂)) ≫ colimit.ι Φ (IsFiltered.max j₁ j₂) = g₂

Tactic:
by

Goal state after: