mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) ≍ η

Tactic:
rw [id_eq, ← Functor.map_id]
  exact congr_arg_heq (·.toFunctor.map η) (e_comp_id (V := Cat) a b)

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 : Center C
U U' : C
⊢ (α_ X.fst Y.fst (U ⊗ U')).hom ≫
      X.fst ◁
          ((α_ Y.fst U U').inv ≫
            (Y.snd.β U).hom ▷ U' ≫ (α_ U Y.fst U').hom ≫ U ◁ (Y.snd.β U').hom ≫ (α_ U U' Y.fst).inv) ≫
        (α_ X.fst (U ⊗ U') Y.fst).inv ≫
          ((α_ X.fst U U').inv ≫
                (X.snd.β U).hom ▷ U' ≫ (α_ U X.fst U').hom ≫ U ◁ (X.snd.β U').hom ≫ (α_ U U' X.fst).inv) ▷
              Y.fst ≫
            (α_ (U ⊗ U') X.fst Y.fst).hom =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ 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) ▷
          U' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          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) ≫
            (α_ U U' (X.fst ⊗ Y.fst)).inv

Tactic:
calc
          _ = 𝟙 _ ⊗≫
            X.1 ◁ (HalfBraiding.β Y.2 U).hom ▷ U' ⊗≫
              (_ ◁ (HalfBraiding.β Y.2 U').hom ≫
                (HalfBraiding.β X.2 U).hom ▷ _) ⊗≫
                  U ◁ (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by monoidal
          _ = _ := by rw [whisker_exchange]; monoidal

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 : C
f : X ⟶ Y
hf : r.degHom f = r.deg X
⊢ W₂ f

Tactic:
obtain ⟨Z, p, i, hp, hi, fac, h⟩ := r.exists_fac f
  obtain ⟨_⟩ := r.identities_of_prop₁_of_eq hp (by aesop)
  obtain rfl : i = f := by simpa using fac
  exact hi

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ mkNatTrans (fun y ↦ homMk (e₀₁.tensor (Edge.id y))) ⋯ ≫ mkNatTrans (fun y ↦ homMk (e₁₂.tensor (Edge.id y))) ⋯ =
    mkNatTrans (fun y ↦ homMk (e₀₂.tensor (Edge.id y))) ⋯

Tactic:
ext y

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
y : Y.HomotopyCategory
⊢ (mkNatTrans (fun y ↦ homMk (e₀₁.tensor (Edge.id y))) ⋯ ≫ mkNatTrans (fun y ↦ homMk (e₁₂.tensor (Edge.id y))) ⋯).app
      y =
    (mkNatTrans (fun y ↦ homMk (e₀₂.tensor (Edge.id y))) ⋯).app y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
f : X ⟶ X'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e)

Tactic:
ext y

Goal state after:
X X' Y Y' Z : Truncated 2
f : X ⟶ X'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                        (mk x₁)).obj
                    (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                        (mk x₀)).obj
                    (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e)).app
      y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)

Tactic:
ext y

Goal state after:
X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x₁)).obj
                    (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl
                  (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                        (mk x₀)).obj
                    (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)).app
      y
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case right
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
b₁ : ℕ
h' : L₁.length = b₁
h₁' : mk (m + 1) = mk (m + 1)
g : mk (m + 1 + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
hL₁ : IsAdmissible (m + 1) L₁
e₁ : g = standardσ L₁ ⋯
⊢ g ≫ σ k = standardσ (simplicialInsert (↑k) L₁) ⋯

Tactic:
subst_vars

Goal state after:
case right
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
h₁' : mk (m + 1) = mk (m + 1)
hL₁ : IsAdmissible (m + 1) L₁
hg : degeneracies.multiplicativeClosure (standardσ L₁ ⋯)
⊢ standardσ L₁ ⋯ ≫ σ k = standardσ (simplicialInsert (↑k) L₁) ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₁)).obj (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₀)).obj (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)

Tactic:
ext y

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₀)).obj (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)).app
      y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₁)).obj (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀)).obj (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)

Tactic:
ext y

Goal state after:
X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y : Y.HomotopyCategory
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).map (homMk e) ≫
          (mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₁)).obj (mk y)))
              ⋯).hom).app
      y =
    ((mkNatIso
              (fun y ↦
                Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀)).obj (mk y)))
              ⋯).hom ≫
          (Functor.curry.obj (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)).app
      y
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
this : (ConcreteCategory.hom (toMk₁ i)) ⟨↑i, ⋯⟩ = (ConcreteCategory.hom (toMk₁ j)) ⟨↑i, ⋯⟩
⊢ i = j

Tactic:
simp [toMk₁_apply, if_pos hij] at this

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

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
this : (Hom.toOrderHom f) j ≤ (Hom.toOrderHom f) i
⊢ 1 = (ConcreteCategory.hom f) i

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was:
      `grind [show f j ≤ f i from f.toOrderHom.monotone hij]` -/

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
this : (Hom.toOrderHom f) j ≤ (Hom.toOrderHom f) i
⊢ 1 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
t : Finset ι
hts : t ⊆ x
ht : t.Nonempty
⊢ t ∈ {t | ∃ v, t = {v}}

Tactic:
cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
            | inl h => exact (ht.ne_empty h).elim
            | inr h => exact ⟨v, h⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i = Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))
⊢ (SimplexCategory.Hom.toOrderHom (eqToHom ⋯))
      ({
          toFun := fun i ↦
            Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
              (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i,
          monotone' := ⋯ }
        ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯)) (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)))) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))

Tactic:
simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk,
      OrderEmbedding.toOrderHom_coe, OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply,
      Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj]

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i = Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))
⊢ {
        toFun := fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i,
        monotone' := ⋯ }
      (Fin.castAdd (x₂.len + 1) i) =
    Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
⊢ motive s

Tactic:
by_cases hs : s.subcomplex ≤ A

Goal state after:
case pos
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : s.subcomplex ≤ A
⊢ motive s

case neg
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : ¬s.subcomplex ≤ A
⊢ motive s
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ (opEquiv.symm { dim := d, simplex := x }).IsUniquelyCodimOneFace (opEquiv.symm { dim := d + 1, simplex := y })

Tactic:
simp only [opEquiv_symm_apply, iff]

Goal state after:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ ∃! i, (ConcreteCategory.hom (SimplicialObject.δ X.op i)) (opObjEquiv.symm y) = opObjEquiv.symm x
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X Y : C
i : X ⟶ Y
x✝ : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ Y
h✝ : ExtremalEpi p
φ : (j : ι) → s j ⟶ X
hφ : ∀ (j : ι), (fun f ↦ f ≫ i) (φ j) = c.inj j ≫ p
⊢ ∀ (i_1 : ι), c.inj i_1 ≫ Cofan.IsColimit.desc hc φ ≫ i = c.inj i_1 ≫ p

Tactic:
by simp [hφ]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
inst✝ : LocallySmall.{w, v, u} C
X : C
J : Type w
w✝² : SmallCategory J
w✝¹ : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
w✝ : Fact κ'.IsRegular
le : κ ≤ κ'
hκ' : HasCardinalLT (Arrow J) κ'
this : IsCardinalPresentable X κ'
⊢ IsPresentable.{w, v, u} X

Tactic:
exact isPresentable_of_isCardinalPresentable _ κ'

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

Goal state before:
pp: case hinj
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)
this : IsFiltered J
⊢ ∀ (i : J) (x y : (fun X ↦ X) ((X ⋙ c.pt).obj i)),
    (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) y →
      ∃ k f, (ConcreteCategory.hom ((X ⋙ c.pt).map f)) x = (ConcreteCategory.hom ((X ⋙ c.pt).map f)) y

Tactic:
· exact isColimitMapCocone.injective c hc κ hK cX hF

Goal state after:
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
⊢ (f.mapN (Cell.type₂ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₂ f c)).dim

Tactic:
· rw [f.mapN_type₂]
    exact c.s.val.nonDegenerate

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 simp [hφ]

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 ∈
    (f.filtration (Order.succ j)).toSSet.nonDegenerate s₁.dim

Tactic:
rw [Subcomplex.mem_nonDegenerate_iff]

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.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 ∈
    (f.filtration (Order.succ j)).toSSet.nonDegenerate s₂.dim

Tactic:
rw [Subcomplex.mem_nonDegenerate_iff]

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