mathlib-initiative/mathlib-tactics huggingface dataset:
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 })
⊢ ((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
      (mk 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
      (mk y)

Tactic:
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
⊢ a.len ≤ max a.len b.len

Tactic:
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:
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 : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : k < i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.castSucc)) k

Tactic:
simp

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : k < i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.castSucc)) k
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : ¬k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
grind [Fin.predAbove]

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

Tactic:
simp

Goal state after:
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
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:
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 : SimplexCategory
hi : i.len ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := i, property := hi })) ⟶ unop (op ⦋n⦌)
⊢ (ConcreteCategory.hom
          ((↾fun x ↦ lift sx s x) ≫
            ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app (StructuredArrow.mk (op f)))).toFun
      x =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))).toFun x

Tactic:
obtain ⟨i, rfl⟩ : ∃ j, ⦋j⦌ = i := ⟨_, i.mk_len⟩

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : ⦋i⦌.len ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
⊢ (ConcreteCategory.hom
          ((↾fun x ↦ lift sx s x) ≫
            ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app (StructuredArrow.mk (op f)))).toFun
      x =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))).toFun x
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 + 1)
⊢ (strArrowMk₂ f hi).hom ≫ (inclusion 2).op.map (Hom.tr (⦋0⦌.const ⦋i⦌ k) ⋯ hi).op =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f) k))
        SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom

Tactic:
simp

Goal state after:
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 + 1)
⊢ f.op ≫ (⦋0⦌.const ⦋i⦌ k).op = (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f) k)).op
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:
simp

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

Goal state before:
pp: x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x.len = y.len

Tactic:
by injection h with h; rw [h]

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

Goal state before:
pp: case inl
n : ℕ
x : Fin (n + 1)
⊢ x.castSucc ≤ (OrderHom.id x).castSucc ∧ ∀ i < x, (OrderHom.id i).castSucc < x.castSucc

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
x✝³ : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((𝟙_ SSet).map x✝ ≫ ↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝¹).len + 1))).obj (𝟙 x✝³)) =
    (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝²).len + 1))).obj (𝟙 x✝³)) ≫ (nerve (x✝³ ⟶ x✝³)).map x✝

Tactic:
simp

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
x✝³ : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝¹).len + 1))).obj (𝟙 x✝³)) =
    (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝²).len + 1))).obj (𝟙 x✝³)) ≫ (nerve (x✝³ ⟶ x✝³)).map x✝
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((nerve (i ⟶ j) ⊗ nerve (j ⟶ k)).map x✝ ≫ ↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) =
    (↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) ≫ (nerve (i ⟶ k)).map x✝

Tactic:
simp

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (((nerve (i ⟶ j)).map x✝ ⊗ₘ (nerve (j ⟶ k)).map x✝) ≫ ↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) =
    (↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) ≫ (nerve (i ⟶ k)).map x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: 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

pp: 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

Tactic:
· exact mem s hs

Goal state after:
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.SimplicialObject.II

Goal state before:
pp: case inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
⊢ map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))

Tactic:
simp

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

Goal state before:
pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ ∀ i_1 < x, i.succAbove i_1 < x.castSucc

Tactic:
intro j

Goal state after:
case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
⊢ j < x → i.succAbove j < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ map' i.succAboveOrderEmb.toOrderHom x.succ.castSucc = x.succ.castSucc.pred ⋯

Tactic:
Fin.pred_castSucc_succ,

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ map' i.succAboveOrderEmb.toOrderHom x.succ.castSucc = x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ ∀ i_1 < x, i.succAbove i_1 < x.succ

Tactic:
intro j

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
⊢ j < x → i.succAbove j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))

Tactic:
simp

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

Goal state before:
pp: case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ ∀ i_1 < x.succ, i.predAbove i_1 < x

Tactic:
intro j

Goal state after:
case pos.right
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
⊢ j < x.succ → i.predAbove j < x
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:
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:
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:
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:
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
e' : B.N ≃o A.N := N.orderIsoOfIso e hA
⊢ e'.symm ↑(P.p ⟨e' (e'.symm ↑x), ⋯⟩) = e'.symm ↑(P.p x)

Tactic:
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:
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:
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:
simp

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

Goal state before:
pp: case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ ∀ i_1 < x.castSucc, i.predAbove i_1 < x

Tactic:
intro j

Goal state after:
case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
⊢ j < x.castSucc → i.predAbove j < x
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:
simp

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

Goal state before:
pp: case inr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
hz : Fin.last (n + 1) ∈ finset f y
⊢ Fin.last (n + 1) ∈ finset f x

Tactic:
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:
simp

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

Goal state before:
pp: p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
⊢ z ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n ↔ StrictMono ⇑(objEquiv z)

Tactic:
rw [← nonDegenerate_iff_of_mono (isoNerve p q).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_strictMono]
  rfl

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

Goal state before:
pp: case zero
p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
⊢ ↑0 ≤ ↑((orderHomOfSimplex (↑x) hm) 0)

Tactic:
simp

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

Goal state before:
pp: case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
h₁ : ↑z₁ ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n
h₂ : ↑z₂ ∈ (Δ[p] ⊗ Δ[q]).nonDegenerate n
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2

Tactic:
rw [nonDegenerate_max_dim_iff] at h₁ h₂

Goal state after:
case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
h₁ : orderHomOfSimplex ↑z₁ ⋯ = OrderHom.id
h₂ : orderHomOfSimplex ↑z₂ ⋯ = OrderHom.id
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

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

Tactic:
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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
⊢ ↑(⋯.index ⋯) = ↑(h.index s)

Tactic:
simp

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

Goal state before:
pp: X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ x₁ ∈ ⊤.obj m

Tactic:
simp

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

Goal state before:
pp: X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : x₁ ∈ ⊤.obj m
⊢ x₂ ∈ ⊤.obj m

Tactic:
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 ι
i₁ i₂ : ι
h : i₁ ≤ i₂
⊢ ∀ i < i₁, ∀ (i_2 : f.Cell i), (↑(P.p i_2.s)).subcomplex ≤ f.filtration i₂

Tactic:
intro j

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ i₂
j : ι
⊢ j < i₁ → ∀ (i : f.Cell j), (↑(P.p i.s)).subcomplex ≤ f.filtration i₂
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app none =
    𝟙 (c x✝).pt ≫ (c x✝).π.app none

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.left) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.left)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x✝ : D
⊢ (hc x✝).lift { pt := (c x✝).pt, π := (c x✝).π ≫ cospanHomMk (H.map (𝟙 x✝)) (F.map (𝟙 x✝)) (G.map (𝟙 x✝)) ⋯ ⋯ } ≫
      (c x✝).π.app (some WalkingPair.right) =
    𝟙 (c x✝).pt ≫ (c x✝).π.app (some WalkingPair.right)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app none =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app none

Tactic:
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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ A ≤ f.filtration ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.left) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.left)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X✝ Y✝ Z✝ : D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (hc Z✝).lift
        { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map (x✝¹ ≫ x✝)) (F.map (x✝¹ ≫ x✝)) (G.map (x✝¹ ≫ x✝)) ⋯ ⋯ } ≫
      (c Z✝).π.app (some WalkingPair.right) =
    ((hc Y✝).lift { pt := (c X✝).pt, π := (c X✝).π ≫ cospanHomMk (H.map x✝¹) (F.map x✝¹) (G.map x✝¹) ⋯ ⋯ } ≫
        (hc Z✝).lift { pt := (c Y✝).pt, π := (c Y✝).π ≫ cospanHomMk (H.map x✝) (F.map x✝) (G.map x✝) ⋯ ⋯ }) ≫
      (c Z✝).π.app (some WalkingPair.right)

Tactic:
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
⊢ ∀ i_1 < i, f.filtration i_1 ≤ f.filtration i

Tactic:
intro j

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