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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Sigma.ι (fun x ↦ R) x ≫ PInfty.f n = Sigma.ι (fun x ↦ R) ⟨x, hx⟩ ≫ (X.fromNormalizedChainComplex R).f n

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Sigma.ι (fun x ↦ R) x ≫ PInfty.f n = Sigma.ι (fun x ↦ R) ⟨x, hx⟩ ≫ (X.fromNormalizedChainComplex R).f n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ 𝟙 ((X.normalizedChainComplex R).X n) = 0

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ 𝟙 ((X.normalizedChainComplex R).X n) = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
            x,
          stdSimplex.objMk₁ (i.castSucc.succ.succ.pred ⋯)).2
      k =
    ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
            x,
          stdSimplex.objMk₁ (i.castSucc.castSucc.succ.castPred ⋯)).2
      k

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ ExactAt (X.normalizedChainComplex R) n

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ ExactAt (X.normalizedChainComplex R) n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ ExactAt (X.chainComplex R) n

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
n d : ℕ
inst✝ : X.HasDimensionLT d
h : d ≤ n
⊢ ExactAt (X.chainComplex R) n
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
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
⊢ s.index.castSucc = 0

Tactic:
]

Goal state after:
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
⊢ s.index.castSucc = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
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⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
            x,
          stdSimplex.objMk₁ (j.castSucc.castSucc.succ.castPred ⋯)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k

Tactic:
]

Goal state after:
case snd
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⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
            x,
          stdSimplex.objMk₁ (j.castSucc.castSucc.succ.castPred ⋯)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k
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.last (m + 1)].unionProd ∂Δ[n] = Λ[m + 1, Fin.last (m + 1)].unionProd ∂Δ[n]

Tactic:
]

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

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
            ((ConcreteCategory.hom (σ Δ[n] i.castSucc)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
          stdSimplex.objMk₁ j.castSucc.succ.succ).2
      k =
    ((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).2
      k

Tactic:
]

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

Goal state before:
pp: case pos
m✝ : ℕ
k : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
⊢ ((pairingCore 0 n).pairing.op.ofIso
      (((stdSimplex.opIso ⦋m + 1⦌).symm ⊗ᵢ (stdSimplex.opIso ⦋n⦌).symm) ≪≫
        Functor.Monoidal.μIso opFunctor Δ[m + 1] Δ[n])
      ⋯).IsRegular

Tactic:
]

Goal state after:
case pos
m✝ : ℕ
k : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
⊢ ((pairingCore 0 n).pairing.op.ofIso
      (((stdSimplex.opIso ⦋m + 1⦌).symm ⊗ᵢ (stdSimplex.opIso ⦋n⦌).symm) ≪≫
        Functor.Monoidal.μIso opFunctor Δ[m + 1] Δ[n])
      ⋯).IsRegular
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
k : Fin (m + 1)
hk : k.castSucc ≠ Fin.last (m + 1)
⊢ (pairingCore k n).pairing.IsRegular

Tactic:
]

Goal state after:
case neg
m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m n : ℕ
k : Fin (m + 1)
hk : k.castSucc ≠ Fin.last (m + 1)
⊢ (pairingCore k n).pairing.IsRegular
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms

Goal state before:
pp: ⊢ ((monomorphisms (Type u_1)).functorCategory SimplexCategoryᵒᵖ).IsStableUnderCobaseChange

Tactic:
]

Goal state after:
⊢ ((monomorphisms (Type u_1)).functorCategory SimplexCategoryᵒᵖ).IsStableUnderCobaseChange
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms

Goal state before:
pp: J : Type u
x✝¹ : Category.{u, u} J
x✝ : IsFiltered J
⊢ ((monomorphisms (Type u)).functorCategory SimplexCategoryᵒᵖ).IsStableUnderColimitsOfShape J

Tactic:
]

Goal state after:
J : Type u
x✝¹ : Category.{u, u} J
x✝ : IsFiltered J
⊢ ((monomorphisms (Type u)).functorCategory SimplexCategoryᵒᵖ).IsStableUnderColimitsOfShape J
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ ((ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n + 1 + 1⦌)))
            ((ConcreteCategory.hom (σ Δ[n] i.succ)) (stdSimplex.objEquiv.symm (SimplexCategory.σ j))),
          stdSimplex.objMk₁ j.castSucc.succ.castSucc).2
      k =
    ((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).2
      k

Tactic:
]

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

Goal state before:
pp: X : SSet
⊢ ∀ (n : ℕ), X.nonDegenerate n ⊆ (⨆ i, i.subcomplex).obj (op ⦋n⦌)

Tactic:
]

Goal state after:
X : SSet
⊢ ∀ (n : ℕ), X.nonDegenerate n ⊆ (⨆ i, i.subcomplex).obj (op ⦋n⦌)
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
⊢ Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y) =
    x.subcomplex ⊓ y.subcomplex

Tactic:
]

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

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y u t : X.N
h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)
⊢ t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)

Tactic:
]

Goal state after:
X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y u t : X.N
h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)
⊢ t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
⊢ Subcomplex.range φ ≠ ⊤

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
⊢ Subcomplex.range φ ≠ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ IsIso ⊤.ι

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
s : X.PtSimplex n x
Y : SSet
φ : Y ⟶ Δ[n]
inst✝ : Y.HasDimensionLT n
h : Subcomplex.range φ = ⊤
⊢ IsIso ⊤.ι
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
H :
  ∀ (u t : X.N) (h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)),
    (ConcreteCategory.hom ((s.ι.app u).app (op ⦋t.dim⦌))) ⟨t.simplex, h⟩ =
      (ConcreteCategory.hom ((s.ι.app t).app (op ⦋t.dim⦌))) ⟨t.simplex, ⋯⟩
⊢ ∀ (n : ℕ) (x_1 : ↑(X.nonDegenerate n)),
    ↑x_1 ∈ (x.subcomplex ⊓ y.subcomplex).obj (op ⦋n⦌) →
      ↑x_1 ∈ (Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y)).obj (op ⦋n⦌)

Tactic:
]

Goal state after:
X : SSet
s : Cocone X.functorN
x✝ : (MultispanShape.prod X.N).L
x y : X.N
H :
  ∀ (u t : X.N) (h : t.simplex ∈ u.subcomplex.obj (op ⦋t.dim⦌)),
    (ConcreteCategory.hom ((s.ι.app u).app (op ⦋t.dim⦌))) ⟨t.simplex, h⟩ =
      (ConcreteCategory.hom ((s.ι.app t).app (op ⦋t.dim⦌))) ⟨t.simplex, ⋯⟩
⊢ ∀ (n : ℕ) (x_1 : ↑(X.nonDegenerate n)),
    ↑x_1 ∈ (x.subcomplex ⊓ y.subcomplex).obj (op ⦋n⦌) →
      ↑x_1 ∈ (Subfunctor.equalizer (Subcomplex.homOfLE ⋯ ≫ s.ι.app x) (Subcomplex.homOfLE ⋯ ≫ s.ι.app y)).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
⊢ f.map = f.map

Tactic:
]

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

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x : X.N
this :
  x.subcomplex.ι ≫ (Subcomplex.topIso X).inv =
    ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).map Subcomplex.toSSetFunctor).π x
⊢ ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).map Subcomplex.toSSetFunctor).π x ≫
      Multicofork.IsColimit.desc ⋯.isColimit (fun x ↦ s.ι.app x) ⋯ =
    s.ι.app x

Tactic:
]

Goal state after:
X : SSet
s : Cocone X.functorN
x : X.N
this :
  x.subcomplex.ι ≫ (Subcomplex.topIso X).inv =
    ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).map Subcomplex.toSSetFunctor).π x
⊢ ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).map Subcomplex.toSSetFunctor).π x ≫
      Multicofork.IsColimit.desc ⋯.isColimit (fun x ↦ s.ι.app x) ⋯ =
    s.ι.app x
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit

Goal state before:
pp: X : SSet
s : Cocone X.functorN
m : X.coconeN.pt ⟶ s.pt
hm : ∀ (j : X.N), X.coconeN.ι.app j ≫ m = s.ι.app j
⊢ (Subcomplex.topIso X).hom ≫ m = (Subcomplex.topIso X).hom ≫ desc s

Tactic:
]

Goal state after:
X : SSet
s : Cocone X.functorN
m : X.coconeN.pt ⟶ s.pt
hm : ∀ (j : X.N), X.coconeN.ι.app j ≫ m = s.ι.app j
⊢ (Subcomplex.topIso X).hom ≫ m = (Subcomplex.topIso X).hom ≫ desc s
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : j.castSucc < i.succ.castSucc
⊢ const x = const x

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: case succ
X : SSet
x : X _⦋0⦌
n : ℕ
f : X.PtSimplex (n + 1) x
i : Fin (n + 1)
j : Fin (n + 1 + 1)
hj : i.castSucc.succ < j.succ
⊢ const x = const x

Tactic:
]

Goal state after:
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 + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ f'.map = f'.map

Tactic:
]

Goal state after:
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 + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
⊢ g'.map = g'.map

Tactic:
]

Goal state after:
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 + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : j < i.castSucc
⊢ const x = const x

Tactic:
]

Goal state after:
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 + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : i.succ < j
⊢ const x = const x

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.succ.succ ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.succ.succ ≫ h.map)))

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.succ ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.succ ≫ h.map)))

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : f.MulStruct g fg i
j : Fin n
hij : i.rev = j
⊢ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.castSucc ≫ h.map))) =
    yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv (stdSimplex.δ i.castSucc.castSucc ≫ h.map)))

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (const (opObjEquiv.symm x)))) = const x

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (const (opObjEquiv.symm x)))) = const x
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (const (opObjEquiv.symm x)))) = const x

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g fg : X.PtSimplex n x
i : Fin n
h : g.op.MulStruct f.op fg.op i
j : Fin n
hij : i.rev = j
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ yonedaEquiv.symm (opObjEquiv (yonedaEquiv (const (opObjEquiv.symm x)))) = const x
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 : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.succ ≤ j
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : MulStruct RelativeMorphism.const f g i
j : Fin (n + 2)
hj : i.succ.succ ≤ j
⊢ stdSimplex.δ j ≫ h.map = const x
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
⊢ f.map = f.map

Tactic:
]

Goal state after:
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 : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.castSucc.succ
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin n
h : g.MulStruct RelativeMorphism.const f i
j : Fin (n + 2)
hj : j < i.castSucc.succ
⊢ stdSimplex.δ j ≫ h.map = const x
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this : sSetTopAdj.unit.app Δ[0] = SSet.const (TopCat.toSSetObj₀Equiv.symm default)
⊢ SSet.const (TopCat.toSSetObj₀Equiv.symm default) ≫ TopCat.toSSet.map f =
    SSet.const
      ((X.toSSetObjEquiv (op ⦋0⦌)).symm { toFun := fun x ↦ (ConcreteCategory.hom f) default, continuous_toFun := ⋯ })

Tactic:
]

Goal state after:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this : sSetTopAdj.unit.app Δ[0] = SSet.const (TopCat.toSSetObj₀Equiv.symm default)
⊢ SSet.const (TopCat.toSSetObj₀Equiv.symm default) ≫ TopCat.toSSet.map f =
    SSet.const
      ((X.toSSetObjEquiv (op ⦋0⦌)).symm { toFun := fun x ↦ (ConcreteCategory.hom f) default, continuous_toFun := ⋯ })
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 1) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)

Tactic:
]

Goal state after:
⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 1) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X) ∧ Nonempty (ZerothHomotopy ↑X)

Tactic:
]

Goal state after:
X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X) ∧ Nonempty (ZerothHomotopy ↑X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1))) default)) =
    stdSimplexHomeomorphUnitInterval ⟨Pi.single 0 1, ⋯⟩

Tactic:
]

Goal state after:
⊢ stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1))) default)) =
    stdSimplexHomeomorphUnitInterval ⟨Pi.single 0 1, ⋯⟩
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
⊢ Subsingleton (ZerothHomotopy ↑X) ∧ Nonempty (ZerothHomotopy ↑X)

Tactic:
constructor <;> infer_instance

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy

Goal state before:
pp: X : TopCat
inst✝ : PathConnectedSpace ↑X
this : Unique (ZerothHomotopy ↑X) := ⋯.some
⊢ Nonempty (Unique (toSSet.obj X).π₀)

Tactic:
]

Goal state after:
X : TopCat
inst✝ : PathConnectedSpace ↑X
this : Unique (ZerothHomotopy ↑X) := ⋯.some
⊢ Nonempty (Unique (toSSet.obj X).π₀)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: case e_6
⊢ stdSimplex.vertex ((ConcreteCategory.hom (SimplexCategory.δ 1)) 0) = ⟨Pi.single 0 1, ⋯⟩

Tactic:
]

Goal state after:
case e_6
⊢ stdSimplex.vertex ((ConcreteCategory.hom (SimplexCategory.δ 1)) 0) = ⟨Pi.single 0 1, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 0) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
]

Goal state after:
⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 0) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)