mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
⊢ i ≤ i + k

Tactic:
by simp

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

Goal state before:
pp: i : Fin (0 + 1)
⊢ 𝟙 (mk (0 + 1)) ≫ σ i = σ i ≫ 𝟙 (mk 0)

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
⊢ 𝟙 (mk (n + 1 + 1)) ≫ σ i = σ i ≫ 𝟙 (mk (n + 1))

Tactic:
by simp

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

Goal state before:
pp: x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 2)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk n'
he : P_σ e
hm : P_δ m
⊢ (e ≫ m) ≫ δ j = e ≫ m ≫ δ j

Tactic:
by simp

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

Goal state before:
pp: x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
e : mk n ⟶ mk (n' + 1)
he : P_σ e
⊢ (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = (e ≫ σ j) ≫ 𝟙 (mk n')

Tactic:
by simp

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

Goal state before:
pp: m a : ℕ
L : List ℕ
h : IsAdmissible m (a :: L)
⊢ IsAdmissible (m + 1) L

Tactic:
by cases L <;> grind

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

Goal state before:
pp: m a : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
ha : a ≤ m
ha' : ∀ (x : 0 < L.length), a < L[0]
⊢ IsAdmissible m (a :: L)

Tactic:
by cases L <;> grind

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ∀ (x_1 : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })),
    homMk ((Edge.id x).tensor (Edge.id x_1)) = 𝟙 (mk (x, x_1))

Tactic:
by simp

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

Goal state before:
pp: case cons
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) ⋯))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j

Tactic:
have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop

Goal state after:
case cons
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
ha₀ : Fin.ofNat (m₂ + 1) a = a₀
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) ⋯))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j
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₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (Edge.id y) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom
              (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x₁, y))) =
    𝟙
        (mk
          ((ConcreteCategory.hom
              (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x₀, y))) ≫
      𝟙 (mk y)

Tactic:
simp only [Category.comp_id]

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.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk (Edge.id y) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom
              (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x₁, y))) =
    𝟙
      (mk
        ((ConcreteCategory.hom
            (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
              (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
          (x₀, y)))
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ a.len ≤ max a.len b.len

Tactic:
by simp

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

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ b.len ≤ max a.len b.len

Tactic:
by simp

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : i < k
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k

pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k

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 [Fin.predAbove_of_castSucc_lt, toMk₁_of_le_castSucc]` -/
    simp; grind [Fin.predAbove_of_castSucc_lt, toMk₁_of_le_castSucc]

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
t : RelUpperSet P
carrier✝ : Set α
isRelUpperSet'✝ : IsRelUpperSet carrier✝ P
h : { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ } = t

Tactic:
cases t

Goal state after:
case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelUpperSet'✝¹ : IsRelUpperSet carrier✝¹ P
carrier✝ : Set α
isRelUpperSet'✝ : IsRelUpperSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ } =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
t : RelLowerSet P
carrier✝ : Set α
isRelLowerSet'✝ : IsRelLowerSet carrier✝ P
h : { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ } = t

Tactic:
cases t

Goal state after:
case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelLowerSet'✝¹ : IsRelLowerSet carrier✝¹ P
carrier✝ : Set α
isRelLowerSet'✝ : IsRelLowerSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ } =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ i.castSucc < Fin.last (n + 1)

Tactic:
by simp

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin i
⊢ (strArrowMk₂ f (SSet.StrictSegal.isPointwiseRightKanExtensionAt._proof_1 i hi)).hom ≫
      (inclusion 2).op.map (Hom.tr (mkOfSucc k) ⋯ hi).op =
    (strArrowMk₂ (mkOfSucc k ≫ f) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom

Tactic:
by simp

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

Goal state before:
pp: x y : SimplexCategory
i : Fin (x.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)

Tactic:
ext
  simp [inl', inl, MonoidalCategoryStruct.rightUnitor, MonoidalCategoryStruct.whiskerLeft,
    MonoidalCategoryStruct.tensorUnit, MonoidalCategoryStruct.tensorObj,
    tensorUnit, tensorHom, WithInitial.down, rightUnitor, tensorObj, CategoryStruct.id,
    CategoryStruct.comp, WithInitial.comp, WithInitial.id,
    OrderEmbedding.toOrderHom]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ (by simpa), Fin.castPred_castSucc]
      obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
      · simp only [map'_eq_castSucc_iff, OrderEmbedding.toOrderHom_coe,
          Fin.succAboveOrderEmb_apply, Fin.castSucc_le_castSucc_iff,
          Fin.castSucc_lt_castSucc_iff]
        constructor
        · obtain hx | rfl := hx.lt_or_eq
          · rwa [Fin.succAbove_of_castSucc_lt]
          · simpa only [Fin.succAbove_castSucc_self] using Fin.castSucc_le_succ x
        · intro j hj
          rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]
      · obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx
        simp [map'_eq_last_iff]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
⊢ ∀ (a : B.N), a ∈ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.II ↔ (N.orderIsoOfIso e hA).toEquiv a ∈ P.II

Tactic:
by simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
⊢ ∀ (a : A.N), a ∈ P.I ↔ (N.orderIsoOfIso e hA).symm.toEquiv a ∈ ⇑(N.orderIsoOfIso e hA) ⁻¹' P.I

Tactic:
by simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
⊢ (N.orderIsoOfIso e hA).symm ↑x ∈ (P.ofIso e hA).II

Tactic:
by simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
⊢ (N.orderIsoOfIso e hA).symm ↑(P.p x) ∈ (P.ofIso e hA).I

Tactic:
by simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x y : ↑P.II
⊢ (N.orderIsoOfIso e hA).symm ↑x ∈ (P.ofIso e hA).II

Tactic:
by simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x y : ↑P.II
⊢ (N.orderIsoOfIso e hA).symm ↑y ∈ (P.ofIso e hA).II

Tactic:
by simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x y : ↑P.II
⊢ ↑⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ < ↑((P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm ↑y, ⋯⟩) ↔ ↑x < ↑(P.p y)

Tactic:
by simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
d : ℕ
hd : (↑x).dim = d
inst✝ : P.IsProper
⊢ (N.orderIsoOfIso e hA).symm ↑x ∈ (P.ofIso e hA).II

Tactic:
by simp

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

Goal state before:
pp: p q n : ℕ
x✝ : (Δ[p] ⊗ Δ[q]) _⦋n⦌
x : Δ[p] _⦋n⦌
y : Δ[q] _⦋n⦌
⊢ (fun f ↦
        (stdSimplex.objEquiv.symm (SimplexCategory.Hom.mk (OrderHom.fst.comp f)),
          stdSimplex.objEquiv.symm (SimplexCategory.Hom.mk (OrderHom.snd.comp f))))
      ((fun x ↦
          match x with
          | (x, y) =>
            (SimplexCategory.Hom.toOrderHom (stdSimplex.objEquiv x)).prod
              (SimplexCategory.Hom.toOrderHom (stdSimplex.objEquiv y)))
        (x, y)) =
    (x, y)

Tactic:
by simp

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

Goal state before:
pp: X : SSet
inst✝¹ : X.Nonsingular
x y : X.N
h : x ≤ y
g : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Mono g
h' : (ConcreteCategory.hom (X.map g.op)) y.simplex = x.simplex
⊢ (ConcreteCategory.hom (X.map (monoOfLE h).op)) y.simplex = x.simplex

Tactic:
by simp

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.RankFunction α
⊢ (fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ })
      ((fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ }) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.pairing.RankFunction α
⊢ (fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ })
      ((fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ }) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.WeakRankFunction α
⊢ (fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ })
      ((fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ }) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
x✝ : h.pairing.WeakRankFunction α
⊢ (fun f ↦ { rank := fun s ↦ f.rank (h.equivII.symm s), lt := ⋯ })
      ((fun g ↦ { rank := fun x ↦ g.rank (h.equivII x), lt := ⋯ }) x✝) =
    x✝

Tactic:
by simp

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : SimplexCategoryᵒᵖ
x : c.1.obj n
⊢ ∃ i y, (ConcreteCategory.hom ((c.ι.app i).app n)) y = x

Tactic:
exact Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves ((evaluation _ _).obj n) hc) x

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

Goal state before:
pp: X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n

Tactic:
have := X₁.dim_lt_of_nonDegenerate ⟨_, x₁.nonDegenerate⟩ d₁

Goal state after:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this : x₁.dim < d₁
⊢ (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm x₂.simplex)).toSSet.HasDimensionLT n
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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
g : unop (op ⦋(↑c.s).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ : stdSimplex.objEquiv.symm g ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ : (ConcreteCategory.hom (c.map.app (op ⦋(↑c.s).dim⦌))) (stdSimplex.objEquiv.symm g) = (↑c.s).simplex
⊢ False

Tactic:
← stdSimplex.map_objEquiv_op_apply,

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
g : unop (op ⦋(↑c.s).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ : stdSimplex.objEquiv.symm g ∈ c.horn.obj (op ⦋(↑c.s).dim⦌)
h₂ :
  (ConcreteCategory.hom (X.map (stdSimplex.objEquiv (stdSimplex.objEquiv.symm g)).op)) ((↑(P.p c.s)).cast ⋯).simplex =
    (↑c.s).simplex
⊢ False
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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ (ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))).image c.map = (↑c.s).subcomplex

Tactic:
image_ofSimplex

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ ofSimplex ((ConcreteCategory.hom (c.map.app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))) =
    (↑c.s).subcomplex
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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ f.filtration ⊥

Tactic:
by simp

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

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ f.filtration i ≤ ⨆ j, ⨆ (_ : j < i), f.filtration j

pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ ⨆ j, ⨆ (_ : j < i), f.filtration j ≤ f.filtration i

Tactic:
· conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff]
    refine ⟨?_, fun j hj c ↦ ?_⟩
    · refine le_trans ?_ (le_iSup _ ⊥)
      exact le_trans (by simp) (le_iSup _ hi.bot_lt)
    · refine le_trans ?_ (le_iSup _ (Order.succ j))
      refine le_trans ?_ (le_iSup _
        (by rwa [← Order.IsSuccLimit.succ_lt_iff hi] at hj))
      exact f.subcomplex_le_filtration _ (Order.lt_succ_of_not_isMax hj.not_isMax)

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ ⨆ j, ⨆ (_ : j < i), f.filtration j ≤ f.filtration i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
⊢ ↑c.s ≤ ↑(P.p c'.s)

Tactic:
rw [← ofSimplex_le_iff] at h

Goal state after:
case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : ofSimplex (↑c.s).simplex ≤ (↑(P.p c'.s)).subcomplex
⊢ ↑c.s ≤ ↑(P.p c'.s)
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✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
⊢ ⨆ i, f.filtration i ≤ ⊤

Tactic:
by simp

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✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
s : X.N
a✝ : s.subcomplex ≤ ⊤
hs : s.subcomplex ≤ A
⊢ A ≤ f.filtration ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : ExtremalEpi f
A : Subobject Y
hA : A.Factors f
⊢ A.factorThru f hA ≫ A.arrow = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasEqualizers C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
⊢ equalizer.lift f h ≫ equalizer.ι p q = f

Tactic:
by simp

Goal state after: