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

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ Arrow.Hom.right (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.right A

Tactic:
dsimp

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ WidePushout.ι (fun x ↦ F.hom) 0 ≫
      WidePushout.desc (Arrow.Hom.left A ≫ X.hom.app ⦋0⦌) (fun i ↦ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ i))
        ⋯ =
    Arrow.Hom.right A
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ f = Pi.lift fun j ↦ s.π.app (some j)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
⊢ f = Pi.lift fun j ↦ s.π.app (some j)
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun x ↦ X) j = (Fan.mk s.pt fun j ↦ s.π.app (some j)).π.app { as := j }

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun x ↦ X) j = s.π.app (some j)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ IsIso (factorThruImage (g hf₁ f₂))

Tactic:
have := map_g_op_y₂ hf₁ hy₁ hy₂
  rw [← image.fac (g hf₁ f₂), op_comp, Functor.map_comp, comp_apply] at this
  exact X.isIso_of_nonDegenerate y₁ (factorThruImage (g hf₁ f₂)) _ this

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

Goal state before:
pp: X : SSet
x y : X.op.N
⊢ { toFun := fun x ↦ mk (opObjEquiv x.simplex) ⋯, invFun := fun y ↦ mk (opObjEquiv.symm y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        x ≤
      { toFun := fun x ↦ mk (opObjEquiv x.simplex) ⋯, invFun := fun y ↦ mk (opObjEquiv.symm y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        y ↔
    x ≤ y

Tactic:
dsimp

Goal state after:
X : SSet
x y : X.op.N
⊢ mk (opObjEquiv x.simplex) ⋯ ≤ mk (opObjEquiv y.simplex) ⋯ ↔ x ≤ y
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
⊢ { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        x ≤
      { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        y ↔
    x ≤ y

Tactic:
dsimp

Goal state after:
X Y : SSet
e : X ≅ Y
x y : X.N
⊢ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯ ≤
      mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯ ↔
    x ≤ y
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this✝ : IsSplitEpi f
this : Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))
⊢ (ConcreteCategory.hom (X.map f.op))
      ((ConcreteCategory.hom (X.map (section_ f).op))
        { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.simplex) =
    (ConcreteCategory.hom (X.map f.op)) (N.mk ↑y ⋯).simplex

Tactic:
dsimp

Goal state after:
case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this✝ : IsSplitEpi f
this : Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))
⊢ (ConcreteCategory.hom (X.map f.op))
      ((ConcreteCategory.hom (X.map (section_ f).op)) ((ConcreteCategory.hom (X.map f.op)) ↑y)) =
    (ConcreteCategory.hom (X.map f.op)) ↑y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ x ∈ A.toSSet.nonDegenerate n ↔ ↑x ∈ X.nonDegenerate n

Tactic:
mem_nonDegenerate_iff_notMem_degenerate,

Goal state after:
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ x ∉ A.toSSet.degenerate n ↔ ↑x ∈ X.nonDegenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ x ∉ A.toSSet.degenerate n ↔ ↑x ∈ X.nonDegenerate n

Tactic:
mem_nonDegenerate_iff_notMem_degenerate,

Goal state after:
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ x ∉ A.toSSet.degenerate n ↔ ↑x ∉ X.degenerate n
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Odd j
⊢ (alternatingConst A hOdd hEven hc).iCycles j ≫ ψ = 0

Tactic:
by
  rw [← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)).inv]
  simpa [HomologicalComplex.iCycles, -Preadditive.IsIso.comp_left_eq_zero, HomologicalComplex.sc,
    HomologicalComplex.shortComplexFunctor, alternatingConstScIsoOdd,
    Category.id_comp (X := (alternatingConst A hOdd hEven hc).X _)]
    using (ShortComplex.mk φ ψ hOdd).iCycles_g

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
inst✝ : ∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p
X₁ X₂ : GradedObject I C₁
φ : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
ψ : Y₁ ⟶ Y₂
⊢ { obj := fun Y ↦ mapBifunctorMapObj F p X₁ Y, map := fun {X Y} ψ ↦ mapBifunctorMapMap F p (𝟙 X₁) ψ, map_id := ⋯,
            map_comp := ⋯ }.map
        ψ ≫
      mapBifunctorMapMap F p φ (𝟙 Y₂) =
    mapBifunctorMapMap F p φ (𝟙 Y₁) ≫
      { obj := fun Y ↦ mapBifunctorMapObj F p X₂ Y, map := fun {X Y} ψ ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
            map_comp := ⋯ }.map
        ψ

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
inst✝ : ∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p
X₁ X₂ : GradedObject I C₁
φ : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
ψ : Y₁ ⟶ Y₂
⊢ mapMap (((mapBifunctor F I J).map (𝟙 X₁)).app Y₁ ≫ ((mapBifunctor F I J).obj X₁).map ψ) p ≫
      mapMap (((mapBifunctor F I J).map φ).app Y₂ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₂)) p =
    mapMap (((mapBifunctor F I J).map φ).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map (𝟙 Y₁)) p ≫
      mapMap (((mapBifunctor F I J).map (𝟙 X₂)).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map ψ) p
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ ![a, b, c] (Fin.castSucc 0) ≤ ![a, b, c] (Fin.succ 0) ∧ ![a, b, c] (Fin.castSucc 1) ≤ ![a, b, c] (Fin.succ 1)

Tactic:
dsimp

Goal state after:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ b ∧ b ≤ c
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
⊢ face ∅ = ⊥

Tactic:
ext
  simpa using Finset.univ_neq_empty _

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

Goal state before:
pp: n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ≤ face S₂ ↔ S₁ ⊆ S₂

Tactic:
refine ⟨fun h i hi ↦ ?_, fun h d a ha ↦ ha.trans h⟩

Goal state after:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
h : face S₁ ≤ face S₂
i : Fin (n + 1)
hi : i ∈ S₁
⊢ i ∈ S₂
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = (X.hom ≫ ed.section_).app (op ⦋n⦌)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x✝ : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : x ∈ (face S).obj (op ⦋j⦌)
⊢ (fun f ↦
        ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ })
        ⟨x, hx⟩) =
    ⟨x, hx⟩

Tactic:
dsimp

Goal state after:
case mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x✝ : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : x ∈ (face S).obj (op ⦋j⦌)
⊢ ⟨objMk
        ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp
          (e.toOrderEmbedding.toOrderHom.comp { toFun := fun i ↦ e.symm ⟨x i, ⋯⟩, monotone' := ⋯ })),
      ⋯⟩ =
    ⟨x, hx⟩
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ h ed j.succ ≫ X.left.δ i.castSucc = ((𝟭 (SimplicialObject C)).obj X.left).δ i ≫ h ed j

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ h ed j.succ ≫ X.left.δ i.castSucc = X.left.δ i ≫ h ed j
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ X.left.δ₀Iter ↑j.succ ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j.succ ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ X.left.δ₀Iter (↑j + 1) ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑j + 1) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter ↑i.succ ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑i.succ ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter ↑i.castSucc ⋯ ≫ ed.s (↑k + 1) ≫ X.left.σ₀Iter ↑i.castSucc ⋯ ≫ X.left.δ i.castSucc.succ

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ X.left.δ₀Iter (↑i + 1) ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑i + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter ↑i ⋯ ≫ ed.s (↑k + 1) ≫ X.left.σ₀Iter ↑i ⋯ ≫ X.left.δ i.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
⊢ stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc

Tactic:
dsimp

Goal state after:
n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
⊢ stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n m : ℕ
x✝ : { x // x ∈ Δ[n].nonDegenerate m }
x : Δ[n] _⦋m⦌
hx : x ∈ Δ[n].nonDegenerate m
⊢ Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ ∈ {S | #S = m + 1}

Tactic:
dsimp

Goal state after:
n m : ℕ
x✝ : { x // x ∈ Δ[n].nonDegenerate m }
x : Δ[n] _⦋m⦌
hx : x ∈ Δ[n].nonDegenerate m
⊢ #(Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ) = m + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
⊢ Fintype.card ↥S = m + 1

Tactic:
by simpa using hS

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

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b

Tactic:
dsimp

Goal state after:
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ ⟨↑x a, ⋯⟩ ≤ ⟨↑x b, ⋯⟩ ↔ a ≤ b
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ X.left.δ i ≫ X.left.δ₀Iter ↑j.castSucc ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j.castSucc ⋯ =
    X.left.δ i ≫ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯

Tactic:
dsimp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ h ed j ≫ X.left.σ i.castSucc = ((𝟭 (SimplicialObject C)).obj X.left).σ i ≫ h ed j.succ

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ h ed j ≫ X.left.σ i.castSucc = X.left.σ i ≫ h ed j.succ
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter ↑j.succ ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j.succ ⋯

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter (↑j + 1) ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter (↑j + 1) ⋯
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ h ed j ≫ X.left.σ i.succ = ((𝟭 (SimplicialObject C)).obj X.left).σ i ≫ h ed j.castSucc

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ h ed j ≫ X.left.σ i.succ = X.left.σ i ≫ h ed j.castSucc
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ X.left.δ₀Iter ↑j ⋯ ≫
      ed.s ↑k ≫
        X.left.σ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_43 n i j k hk l hl⟩ ≫
          X.left.σ₀Iter ↑j ⋯ =
    X.left.δ₀Iter (↑j.castSucc)
        (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_32 n j k hk) ≫
      ed.s ↑k ≫
        X.left.σ
            ⟨l, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_41 n i j k hk l hl⟩.succ ≫
          X.left.σ₀Iter ↑j.castSucc ⋯

Tactic:
dsimp

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

Goal state before:
pp: n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ ((ConcreteCategory.hom ((stdSimplex.obj n).op.map f ≫ stdSimplex.opObjEquiv.toIso.hom)).toFun g) i =
    ((ConcreteCategory.hom (stdSimplex.opObjEquiv.toIso.hom ≫ (stdSimplex.obj n).map f)).toFun g) i

Tactic:
dsimp

Goal state after:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ (stdSimplex.opObjEquiv ((ConcreteCategory.hom ((stdSimplex.obj n).op.map f)) g)) i =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ (((ConcreteCategory.hom ((stdSimplex.obj n).map (rev.map f.unop).op)) (opObjEquiv g)) i.rev).rev =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i

Tactic:
dsimp

Goal state after:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ (((ConcreteCategory.hom ((stdSimplex.obj n).map (rev.map f.unop).op)) (opObjEquiv g)) i.rev).rev =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
⊢ (↾fun x ↦ objMk ((OrderHom.const (Fin ((unop (op ⦋0⦌)).len + 1))) 0)) ≫ (stdSimplex.obj Δ).hom.app (op ⦋0⦌) =
    𝟙 (stdSimplex.obj Δ).right

Tactic:
dsimp

Goal state after:
Δ : SimplexCategory
⊢ (↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0)) ≫ Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) = 𝟙 (⊤_ Type ?u.22)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
⊢ (↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.δ 1 =
    (stdSimplex.obj Δ).hom.app (op ⦋0⦌) ≫ ↾fun x ↦ objMk ((OrderHom.const (Fin ((unop (op ⦋0⦌)).len + 1))) 0)

Tactic:
dsimp

Goal state after:
Δ : SimplexCategory
⊢ (↾fun f ↦
        objEquiv.symm
          (SimplexCategory.Hom.mk
            { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
      SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1 =
    Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫ ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ (ConcreteCategory.hom ((ofSimplex x).toSSet.map u)) ⟨x, ⋯⟩ = ⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩

Tactic:
dsimp

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ { toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨x, ⋯⟩ = ⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩