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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n⦌)))
      ((ConcreteCategory.hom (δ (Δ[n] ⊗ Δ[1]) 0)) ↑(prodStdSimplex.nonDegenerateEquiv₁ 0)) =
    (ConcreteCategory.hom ((ι₁ ≫ H.h).app (op ⦋n⦌))) x

Tactic:
dsimp

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] 0)) (stdSimplex.objMk₁ 1)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n⦌))) ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n⦌)))
      ((ConcreteCategory.hom (δ (Δ[n] ⊗ Δ[1]) (Fin.last (n + 1)))) ↑(prodStdSimplex.nonDegenerateEquiv₁ (Fin.last n))) =
    (ConcreteCategory.hom ((ι₀ ≫ H.h).app (op ⦋n⦌))) x

Tactic:
dsimp

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n] (Fin.last (n + 1))))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ (Fin.last n))))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] (Fin.last (n + 1)))) (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n⦌))) ((ConcreteCategory.hom (ι₀.app (op ⦋n⦌))) x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom (δ (Δ[n + 1] ⊗ Δ[1]) i.castSucc)) ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ)) =
    (ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x) ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
      ↑(prodStdSimplex.nonDegenerateEquiv₁ j)

Tactic:
dsimp

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
        stdSimplex.objMk₁ j.castSucc.succ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Splitting

Goal state before:
pp: case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
x✝¹ x✝ : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝¹ : Epi f
x :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
property✝ : Epi f
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩

Tactic:
dsimp

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

Goal state before:
pp: case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
x✝¹ x✝ : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝¹ : Epi f
x :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
p : ℕ
g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)
property✝ : Epi g
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩

Tactic:
· obtain rfl : m = p := unique_nonDegenerate_dim _ _ _ _ rfl _ _ h
      obtain rfl : f = g := unique_nonDegenerate_map _ _ _ _ rfl _ _ h
      dsimp

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom (δ (Δ[n + 1] ⊗ Δ[1]) i.castSucc.succ)) ↑(prodStdSimplex.nonDegenerateEquiv₁ i.succ)) =
    (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom (δ (Δ[n + 1] ⊗ Δ[1]) i.castSucc.succ)) ↑(prodStdSimplex.nonDegenerateEquiv₁ i.castSucc))

Tactic:
dsimp

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom (δ (Δ[n + 1] ⊗ Δ[1]) i.succ)) ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)) =
    (ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x) ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
      ↑(prodStdSimplex.nonDegenerateEquiv₁ j)

Tactic:
dsimp

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.castSucc.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
        stdSimplex.objMk₁ j.castSucc.succ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k = Fin.last (m + 1)
⊢ (Λ[m + 1, Fin.castSucc 0].unionProd ∂Δ[n]).op.preimage
      (((stdSimplex.opIso ⦋m + 1⦌).symm ⊗ᵢ (stdSimplex.opIso ⦋n⦌).symm) ≪≫
          Functor.Monoidal.μIso opFunctor Δ[m + 1] Δ[n]).hom =
    Λ[m + 1, k].unionProd ∂Δ[n]

Tactic:
dsimp

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 2)
n : ℕ
hk : k = Fin.last (m + 1)
⊢ (Λ[m + 1, 0].unionProd ∂Δ[n]).op.preimage
      (((stdSimplex.opIso ⦋m + 1⦌).inv ⊗ₘ (stdSimplex.opIso ⦋n⦌).inv) ≫ Functor.LaxMonoidal.μ opFunctor Δ[m + 1] Δ[n]) =
    Λ[m + 1, k].unionProd ∂Δ[n]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
      ((ConcreteCategory.hom (σ (Δ[n] ⊗ Δ[1]) i.castSucc)) ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) =
    (ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x) ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
      ↑(prodStdSimplex.nonDegenerateEquiv₁ j.succ)

Tactic:
dsimp

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n + 1 + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
          ((ConcreteCategory.hom (σ Δ[n] i.castSucc)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
        (ConcreteCategory.hom (σ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n + 1 + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)),
        stdSimplex.objMk₁ j.castSucc.succ.succ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
      ((ConcreteCategory.hom (σ (Δ[n] ⊗ Δ[1]) i.succ)) ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) =
    (ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x) ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
      ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)

Tactic:
dsimp

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n + 1 + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
          ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
        (ConcreteCategory.hom (σ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n + 1 + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (σ X i)) x)).app (op ⦋n + 1 + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)),
        stdSimplex.objMk₁ j.castSucc.castSucc.succ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y : X.N
⊢ ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).map Subcomplex.toSSetFunctor).fst (x, y) ≫
      s.ι.app ((MultispanShape.prod X.N).fst (x, y)) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).map Subcomplex.toSSetFunctor).snd (x, y) ≫
      s.ι.app ((MultispanShape.prod X.N).snd (x, y))

Tactic:
dsimp

Goal state after:
X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y : X.N
⊢ Subcomplex.homOfLE ⋯ ≫ s.ι.app x = Subcomplex.homOfLE ⋯ ≫ s.ι.app y
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : f.RelStruct g i.succ
⊢ stdSimplex.δ i.castSucc.succ ≫ h.map = f.map

Tactic:
rw [← Fin.castSucc_succ, h.δ_castSucc_map]

Goal state after:
Module: Mathlib.AlgebraicTopology.TopologicalSimplex

Goal state before:
pp: n : SimplexCategory
⊢ Nonempty ↑(toTop₀.obj n)

Tactic:
dsimp

Goal state after:
n : SimplexCategory
⊢ Nonempty ↑(stdSimplex ℝ (Fin (n.len + 1)))
Module: Mathlib.AlgebraicTopology.TopologicalSimplex

Goal state before:
pp: n : SimplexCategory
⊢ PathConnectedSpace ↑(toTop₀.obj n)

Tactic:
dsimp

Goal state after:
n : SimplexCategory
⊢ PathConnectedSpace ↑(stdSimplex ℝ (Fin (n.len + 1)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
⊢ (sSetTopAdj.homEquiv Δ[0] X) f = SSet.const (TopCat.toSSetObj₀Equiv.symm ((ConcreteCategory.hom f) default))

Tactic:
have : sSetTopAdj.unit.app Δ[0] =
      SSet.const (TopCat.toSSetObj₀Equiv.symm default) :=
    SSet.yonedaEquiv.injective (TopCat.toSSetObj₀Equiv.injective (by subsingleton))

Goal state after:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this : sSetTopAdj.unit.app Δ[0] = SSet.const (TopCat.toSSetObj₀Equiv.symm default)
⊢ (sSetTopAdj.homEquiv Δ[0] X) f = SSet.const (TopCat.toSSetObj₀Equiv.symm ((ConcreteCategory.hom f) default))
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
R : C
⊢ ((Sigma.ι (fun x ↦ R) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)) ≫
        (𝟙 (∐ fun x ↦ R) ≫
            ((Adjunction.whiskerLeft C sSetTopAdj).unit.app
                    (((Functor.postcompose₂.obj (eval C (ComplexShape.down ℕ) n)).obj
                          ((Functor.postcompose₂.obj (alternatingFaceMapComplex C)).obj
                            (sigmaConst ⋙ SimplicialObject.whiskering (Type w) C))).obj
                      R)).app
                Δ[n] ≫
              𝟙 (∐ fun x ↦ R)) ≫
          𝟙 (∐ fun x ↦ R)) ≫
      Sigma.map' ⇑(ConcreteCategory.hom ((TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)).app (Opposite.op ⦋n⦌))) fun x ↦
        𝟙 R) =
    Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom ((stdSimplexToTop.app ⦋n⦌).app (Opposite.op ⦋n⦌))) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))

Tactic:
simp [stdSimplexToTop]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
R : C
⊢ Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom ((TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)).app (Opposite.op ⦋n⦌)))
        ((ConcreteCategory.hom ((sSetTopAdj.unit.app Δ[n]).app (Opposite.op ⦋n⦌)))
          (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))) =
    Sigma.ι (fun x ↦ R)
      ((ConcreteCategory.hom
          ((sSetTopAdj.unit.app Δ[n]).app (Opposite.op ⦋n⦌) ≫
            (TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)).app (Opposite.op ⦋n⦌)))
        (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «0»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x))).arrow
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow
      ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
dsimp

Goal state after:
case «0»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x))).arrow
      0 =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «1»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow
      ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
dsimp

Goal state after:
case «1»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_15 _proof_12).op)) x))).arrow
      1 =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 0 _proof_15 _proof_12).op)) (f₁ x))).arrow 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: case «0»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x))).arrow
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))).arrow
      ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
dsimp

Goal state after:
case «0»
X Y : Truncated 2
f₀ : X.obj (op { obj := ⦋0⦌, property := _proof_11 }) → Y.obj (op { obj := ⦋0⦌, property := _proof_11 })
f₁ : X.obj (op { obj := ⦋1⦌, property := _proof_12 }) → Y.obj (op { obj := ⦋1⦌, property := _proof_12 })
hδ₁ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 1 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_11 _proof_13).op)) (f₁ x)
hδ₀ :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })),
    f₀ ((ConcreteCategory.hom (X.map (δ₂ 0 _proof_11 _proof_13).op)) x) =
      (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_11 _proof_13).op)) (f₁ x)
hσ :
  ∀ (x : X.obj (op { obj := ⦋0⦌, property := _proof_11 })),
    f₁ ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_13 _proof_11).op)) x) =
      (ConcreteCategory.hom (Y.map (σ₂ 0 _proof_13 _proof_11).op)) (f₀ x)
hY : Y.StrictSegal
x : X.obj (op { obj := ⦋1⦌, property := _proof_12 })
⊢ ((hY.spineEquiv 2 f₂._proof_4)
          (f₂ f₀ f₁ hδ₁ hδ₀ hY ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_15 _proof_12).op)) x))).arrow
      0 =
    ((hY.spineEquiv 2 f₂._proof_4) ((ConcreteCategory.hom (Y.map (σ₂ 1 _proof_15 _proof_12).op)) (f₁ x))).arrow 0