mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : C ⥤ Type w
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
⊢ F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (f.app Δ')) ((ConcreteCategory.hom (A'.map φ)) a)) =
    F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (A.map φ)) ((ConcreteCategory.hom (f.app Δ)) a))

Tactic:
f.naturality_apply φ a

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : C ⥤ Type w
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
⊢ F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (A.map φ)) ((ConcreteCategory.hom (f.app Δ)) a)) =
    F.map φ ≫ x.app Δ' ((ConcreteCategory.hom (A.map φ)) ((ConcreteCategory.hom (f.app Δ)) a))
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U U' : C
f : U ⟶ U'
⊢ (X.fst ⊗ Y.fst) ◁ f ≫
      (α_ X.fst Y.fst U').hom ≫
        X.fst ◁ (Y.snd.β U').hom ≫ (α_ X.fst U' Y.fst).inv ≫ (X.snd.β U').hom ▷ Y.fst ≫ (α_ U' X.fst Y.fst).hom =
    𝟙 ((X.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y.fst ◁ f ≫ (Y.snd.β U').hom) ⊗≫ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 (U' ⊗ X.fst ⊗ Y.fst)

Tactic:
by monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ (X.fst ◁ f.f) ▷ U ≫
      (α_ X.fst Y₂.fst U).hom ≫
        X.fst ◁ (Y₂.snd.β U).hom ≫ (α_ X.fst U Y₂.fst).inv ≫ (X.snd.β U).hom ▷ Y₂.fst ≫ (α_ U X.fst Y₂.fst).hom =
    𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (f.f ▷ U ≫ (Y₂.snd.β U).hom) ⊗≫ (X.snd.β U).hom ▷ Y₂.fst ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst)

Tactic:
by monoidal

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: K : SSet
φ : 𝟙_ SSet ⟶ K
⊢ (fun x ↦
        { app := fun Δ ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) x,
          naturality := ⋯ })
      ((fun φ ↦ (ConcreteCategory.hom (φ.app (Opposite.op ⦋0⦌))) PUnit.unit) φ) =
    φ

Tactic:
by
    ext Δ ⟨⟩
    dsimp [-Monoidal.tensorUnit_obj]
    rw [← NatTrans.naturality_apply]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ f.f ▷ Y.fst ▷ U ≫
      (α_ X₂.fst Y.fst U).hom ≫
        X₂.fst ◁ (Y.snd.β U).hom ≫ (α_ X₂.fst U Y.fst).inv ≫ (X₂.snd.β U).hom ▷ Y.fst ≫ (α_ U X₂.fst Y.fst).hom =
    𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (Y.snd.β U).hom) ⊗≫ (X₂.snd.β U).hom ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst)

Tactic:
by monoidal

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x : Paths (OneTruncation₂ V)
⊢ ∃ a, mk a = { as := { as := x } }

Tactic:
exact ⟨x, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g : Edge x y
hfg : HomotopicR f g
⊢ HomotopicR g f

Tactic:
by
  rcases hfg with ⟨hfg⟩
  exact Quasicategory₂.fill32 (idComp (id x)) hfg (idComp f)

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ r.degHom (f ≫ g) ≤ r.degHom f

Tactic:
have ⟨_, f₁, f₂, _, _, h_fac, h_deg⟩ := r.exists_fac f
  rw [h_deg, ← h_fac, Category.assoc]
  exact r.degHom_le f₁ (f₂ ≫ g)

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
hfg : r.deg Z ≤ r.degHom f ∧ r.deg Z ≤ r.degHom g
φ : W₁.MapFactorizationData W₂ (f ≫ g) := { Z := Z, i := f, p := g, fac := ⋯, hi := ⋯, hp := ⋯ }
⊢ r.deg Z ≤ r.degHom (f ≫ g)

Tactic:
r.degHom_eq φ

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
hfg : r.deg Z ≤ r.degHom f ∧ r.deg Z ≤ r.degHom g
φ : W₁.MapFactorizationData W₂ (f ≫ g) := { Z := Z, i := f, p := g, fac := ⋯, hi := ⋯, hp := ⋯ }
⊢ r.deg Z ≤ r.deg φ.Z
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : generators.multiplicativeClosure ≤ P
⊢ P f

Tactic:
rw [multiplicativeClosure_isGenerator_eq_top, top_le_iff] at this

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case of
x✝¹ y : SimplexCategoryGenRel
e : x✝¹ ⟶ y
x✝ y✝ : SimplexCategoryGenRel
x : x✝ ⟶ y✝
hx : degeneracies x
⊢ IsSplitEpi x

Tactic:
cases hx; infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case of
x✝¹ y : SimplexCategoryGenRel
m : x✝¹ ⟶ y
x✝ y✝ : SimplexCategoryGenRel
x : x✝ ⟶ y✝
hx : faces x
⊢ IsSplitMono x

Tactic:
cases hx; infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
h_δ : P_δ f
⊢ (∃ (h : x = y), f = eqToHom h) ∨ x.len < y.len

Tactic:
by
  induction h_δ with
  | of _ hx => cases hx; right; simp
  | id => left; use rfl; simp
  | comp_of i u _ hg h' =>
    rcases h' with ⟨e, _⟩ | h' <;>
    apply Or.inr <;>
    cases hg
    · rw [e]
      exact Nat.lt_add_one _
    · exact Nat.lt_succ_of_lt h'

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: x✝² x✝¹ x✝ : Truncated 2
⊢ (iso x✝² x✝¹).symm.hom ▷ hoFunctor₂.obj x✝ ≫ (iso (x✝² ⊗ x✝¹) x✝).symm.hom ≫ hoFunctor₂.map (α_ x✝² x✝¹ x✝).hom =
    (α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
      hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom

Tactic:
by ext; apply associativity

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: Y : Truncated 2
⊢ (λ_ (hoFunctor₂.obj Y)).hom =
    (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ▷ hoFunctor₂.obj Y ≫
      (iso (𝟙_ (Truncated 2)) Y).symm.hom ≫ hoFunctor₂.map (λ_ Y).hom

Tactic:
ext; apply left_unitality

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : i.castSucc < (S.min' hS).castSucc
hi : i ∉ S
⊢ 0 = (ConcreteCategory.hom f) i

Tactic:
simp [S] at hi

Goal state after:
case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : i.castSucc < (S.min' hS).castSucc
hi : ¬(ConcreteCategory.hom f) i = 1
⊢ 0 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ upperBounds x✝

Tactic:
intro K

Goal state after:
case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
⊢ K ∈ x✝ → K ≤ sSup x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
x : Fin (n + 1)
⊢ map' OrderHom.id x.castSucc = x.castSucc

Tactic:
rw [map'_eq_castSucc_iff]

Goal state after:
case inl
n : ℕ
x : Fin (n + 1)
⊢ x.castSucc ≤ (OrderHom.id x).castSucc ∧ ∀ i < x, (OrderHom.id i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (𝟙_ SSet).obj n✝
⊢ (ConcreteCategory.hom ((eId SSet i ≫ nerveMap (functorMap f i i)).app n✝)).toFun x✝ =
    (ConcreteCategory.hom ((eId SSet { as := f i.as }).app n✝)).toFun x✝

Tactic:
simp only [eId, EnrichedCategory.id]

Goal state after:
J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (𝟙_ SSet).obj n✝
⊢ (ConcreteCategory.hom
          (({ app := fun x ↦ ↾fun x_1 ↦ (Functor.const (Fin ((Opposite.unop x).len + 1))).obj (𝟙 i), naturality := ⋯ } ≫
                nerveMap (functorMap f i i)).app
            n✝)).toFun
      x✝ =
    (ConcreteCategory.hom (↾fun x ↦ (Functor.const (Fin ((Opposite.unop n✝).len + 1))).obj (𝟙 { as := f i.as }))).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ (opEquiv.symm x).IsUniquelyCodimOneFace (opEquiv.symm y)

Tactic:
obtain ⟨d, x, rfl⟩ := x.mk_surjective

Goal state after:
X : SSet
y : X.S
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace y
⊢ (opEquiv.symm { dim := d, simplex := x }).IsUniquelyCodimOneFace (opEquiv.symm y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
⊢ { dim := x.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }

Tactic:
obtain ⟨d, x, rfl⟩ := x.mk_surjective

Goal state after:
X : SSet
y : X.S
Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace y
⊢ { dim := { dim := d, simplex := x }.dim,
        simplex :=
          (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x }.dim⦌)))
            { dim := d, simplex := x }.simplex }.IsUniquelyCodimOneFace
    { dim := y.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ Function.Injective ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj ↔
    Function.Injective ⇑(objEquiv z)

Tactic:
← Function.Injective.of_comp_iff ULift.down_injective

Goal state after:
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ Function.Injective (ULift.down ∘ ((ConcreteCategory.hom ((isoNerve p q).hom.app (Opposite.op ⦋n⦌))) z).obj) ↔
    Function.Injective ⇑(objEquiv z)
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 : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
obtain hd | rfl := (SimplexCategory.le_of_mono g).lt_or_eq

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd : d < x.dim + 1
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate (x.dim + 1)
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : HasCardinalFilteredGenerator C κ
P : ObjectProperty C
w✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ∃ P, ∃ (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ

Tactic:
exact ⟨Q, inferInstance, hP.of_le_isoClosure h₂ (h₁.trans hP.le_isCardinalPresentable)⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Injective h.functor.mapArrow.obj

Tactic:
rintro ⟨x, y, f⟩ ⟨x', y', g⟩ hfg

Goal state after:
case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
x y : ↑h.smallCategoryOfSet.obj
f : (𝟭 ↑h.smallCategoryOfSet.obj).obj x ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y
x' y' : ↑h.smallCategoryOfSet.obj
g : (𝟭 ↑h.smallCategoryOfSet.obj).obj x' ⟶ (𝟭 ↑h.smallCategoryOfSet.obj).obj y'
hfg :
  h.functor.mapArrow.obj { left := x, right := y, hom := f } =
    h.functor.mapArrow.obj { left := x', right := y', hom := g }
⊢ { left := x, right := y, hom := f } = { left := x', right := y', hom := g }
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) κ
X : C
hX : (isCardinalPresentable C κ).ColimitOfShape J X
this : ∀ (j : J), isCardinalPresentable C κ (hX.diag.obj j)
⊢ isCardinalPresentable C κ X

Tactic:
simp only [isCardinalPresentable_iff] at this ⊢

Goal state after:
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) κ
X : C
hX : (isCardinalPresentable C κ).ColimitOfShape J X
this : ∀ (j : J), IsCardinalPresentable (hX.diag.obj j) κ
⊢ IsCardinalPresentable X κ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr
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
⊢ { dim := (↑c.s).dim, simplex := (↑c.s).simplex }.simplex ∈
    X.nonDegenerate { dim := (↑c.s).dim, simplex := (↑c.s).simplex }.dim

Tactic:
exact c.s.val.nonDegenerate

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 : ℕ
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₁
⊢ x₁ = x₂

Tactic:
obtain ⟨s₂, g₂, _, hg₂⟩ := (Subcomplex.range (f.m j)).existsN x₂ hx₂

Goal state after:
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₂
⊢ x₁ = x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
j : ℕ
hj : ¬IsMax j
⊢ (coproducts.{u, u, u + 1} (ofHoms (P.rankFunction.basicCell j))).pushouts ≤ SSet.anodyneExtensions

Tactic:
simp only [pushouts_le_iff, coproducts_le_iff]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsRegular
j : ℕ
hj : ¬IsMax j
⊢ ofHoms (P.rankFunction.basicCell j) ≤ SSet.anodyneExtensions
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
⊢ (coproducts.{u, u, u + 1} (ofHoms (P.rankFunction.basicCell j))).pushouts ≤ SSet.innerAnodyneExtensions

Tactic:
simp only [pushouts_le_iff, coproducts_le_iff]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝¹ : P.IsRegular
inst✝ : P.IsInner
j : ℕ
hj : ¬IsMax j
⊢ ofHoms (P.rankFunction.basicCell j) ≤ SSet.innerAnodyneExtensions
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne

Goal state before:
pp: case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + ↑((objMk₁ i.castSucc.succ) j) = ↑j

Tactic:
objMk₁_of_castSucc_lt _ _ (by simpa),

Goal state after:
case pos
p : ℕ
i : Fin (p + 1)
j : Fin (p + 1 + 1)
hj : j ≤ i.castSucc
⊢ ↑((stdSimplex.objEquiv.symm (SimplexCategory.σ i)) j) + ↑0 = ↑j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)).2
      k =
    ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ)).2
      k

Tactic:
rw [stdSimplex.δ_objMk₁_of_lt _ _ (by simp), stdSimplex.δ_objMk₁_of_le _ _ (by simp)]

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
            x,
          stdSimplex.objMk₁ (i.castSucc.succ.succ.pred ⋯)).2
      k =
    ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
            x,
          stdSimplex.objMk₁ (i.castSucc.castSucc.succ.castPred ⋯)).2
      k
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms

Goal state before:
pp: ⊢ (monomorphisms SSet).IsStableUnderCobaseChange

Tactic:
change (monomorphisms (_ ⥤ _)).IsStableUnderCobaseChange

Goal state after:
⊢ (monomorphisms (SimplexCategoryᵒᵖ ⥤ Type u_1)).IsStableUnderCobaseChange
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = const x

Tactic:
rw [stdSimplex.δ_comp_yonedaEquiv_symm, δ_opObjEquiv,
      ← stdSimplex.yonedaEquiv_δ_comp, h.δ_map_of_lt _ (by grind)]
    simp [opObjEquiv_yonedaEquiv_const]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.CountableCover

Goal state before:
pp: α : Type u
ι : Type v
a : Cardinal.{u}
inst✝¹ : Countable ι
f : ι → Set α
l : Filter ι
inst✝ : l.NeBot
t : Set α
ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i
h'f : ∀ (i : ι), #↑(f i) ≤ a
⊢ #↑t ≤ a

Tactic:
by
  let g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (ULift.down ⁻¹' ·) ∘ f ∘ ULift.down
  suffices #(ULift.down.{v} ⁻¹' t) ≤ Cardinal.lift.{v, u} a by simpa
  let l' : Filter (ULift.{u} ι) := Filter.map ULift.up l
  apply mk_subtype_le_of_countable_eventually_mem_aux (ι := ULift.{u} ι) (l := l') (f := g)
  · intro x hx
    simpa only [Function.comp_apply, mem_preimage, eventually_map] using! ht _ hx
  · intro i
    simpa [g] using! h'f i.down

Goal state after: