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

Goal state before:
pp: ⊢ (monomorphisms SSet).IsStableUnderCobaseChange

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: K : Type u
inst✝³ : LinearOrder K
inst✝² : SuccOrder K
inst✝¹ : OrderBot K
inst✝ : WellFoundedLT K
⊢ (monomorphisms SSet).IsStableUnderTransfiniteCompositionOfShape K

Tactic:
by

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 j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
k : Fin (n + 1 + 1 + 1)
⊢ j.castSucc.succ ≤ i.succ.castSucc

Tactic:
by

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 j : Fin (n + 1)
hij : j ≤ i
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j)) ≫
      σ Y i.succ =
    σ X i ≫
      ↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ j.castSucc)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
X₁ : Arrow C₁
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
x✝ : Arrow C₃
⊢ {
            app := fun X₂ ↦
              Arrow.homMk (adj₂.homEquiv (pushout.inl ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                (pullback.lift (adj₂.homEquiv (pushout.inr ((F.map X₁.hom).app X₂.left) ((F.obj X₁.left).map X₂.hom)))
                  (adj₂.homEquiv (𝟙 ((F.obj (unop (op X₁)).right).obj ((𝟭 (Arrow C₂)).obj X₂).right))) ⋯)
                ⋯,
            naturality := ⋯ }.app
        ((G.leibnizPullback.obj (op X₁)).obj x✝) ≫
      (G.leibnizPullback.obj (op X₁)).map
        ({
              app := fun X₃ ↦
                Arrow.homMk
                  (pushout.desc (adj₂.homEquiv.symm (𝟙 ((G.leibnizPullback.obj (op X₁)).obj X₃).left))
                    (adj₂.homEquiv.symm
                      (pullback.fst ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                        ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                    ⋯)
                  (adj₂.homEquiv.symm
                    (pullback.snd ((G.obj (op (unop (op X₁)).left)).map X₃.hom)
                      ((G.map (unop (op X₁)).hom.op).app X₃.right)))
                  ⋯,
              naturality := ⋯ }.app
          x✝) =
    𝟙 ((G.leibnizPullback.obj (op X₁)).obj x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj₂ : F ⊣₂ G
inst✝¹ : HasPullbacks C₂
inst✝ : HasPushouts C₃
X₁✝ Y₁✝ : Arrow C₁
x✝ : X₁✝ ⟶ Y₁✝
⊢ (LeibnizAdjunction.adj F G adj₂ X₁✝).unit ≫ whiskerRight (F.leibnizPushout.map x✝) (G.leibnizPullback.obj (op X₁✝)) =
    (LeibnizAdjunction.adj F G adj₂ Y₁✝).unit ≫ (F.leibnizPushout.obj Y₁✝).whiskerLeft (G.leibnizPullback.map x✝.op)

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ ⨆ i, i.subcomplex = ⊤

Tactic:
by

Goal state after:
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 ≤ u

Tactic:
by

Goal state after:
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 (Subcomplex.range φ).ι

Tactic:
by

Goal state after:
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
⊢ φ ≫ s.map = const x

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f : X.op.PtSimplex n (opObjEquiv.symm x)
⊢ ∂Δ[n].ι ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)) = const ⟨x, ⋯⟩ ≫ (Subcomplex.ofSimplex x).ι

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
g : X.PtSimplex n x
⊢ ∂Δ[n].ι ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)) =
    const ⟨opObjEquiv.symm x, ⋯⟩ ≫ (Subcomplex.ofSimplex (opObjEquiv.symm x)).ι

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
x✝ : X.op.PtSimplex n (opObjEquiv.symm x)
⊢ (fun g ↦ { map := yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)), comm := ⋯ })
      ((fun f ↦ { map := yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)), comm := ⋯ }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
x✝ : X.PtSimplex n x
⊢ (fun f ↦ { map := yonedaEquiv.symm (opObjEquiv (yonedaEquiv f.map)), comm := ⋯ })
      ((fun g ↦ { map := yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv g.map)), comm := ⋯ }) x✝) =
    x✝

Tactic:
by

Goal state after:
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)
⊢ stdSimplex.δ i.castSucc ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
by

Goal state after:
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)
⊢ stdSimplex.δ i.succ ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
by

Goal state after:
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:
by

Goal state after:
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)
j : Fin (n + 2)
hj : j < i.castSucc
⊢ i ≠ 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
s : Cocone X.functorN
x : X.N
⊢ x.subcomplex.ι ≫ desc s = s.ι.app x

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x✝ : X.N
⊢ SemiSimplexCategory.toSimplexCategory.map (SemiSimplexCategory.homOfMono (monoOfLE ⋯)) =
    SemiSimplexCategory.toSimplexCategory.map (𝟙 ⦋x✝.dim⦌ₛ)

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
X✝ Y✝ Z✝ : X.N
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ SemiSimplexCategory.toSimplexCategory.map (SemiSimplexCategory.homOfMono (monoOfLE ⋯)) =
    SemiSimplexCategory.toSimplexCategory.map
      (SemiSimplexCategory.homOfMono (monoOfLE ⋯) ≫ SemiSimplexCategory.homOfMono (monoOfLE ⋯))

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
X✝ Y✝ : X.N
x✝ : X✝ ⟶ Y✝
⊢ X.functorN'.map x✝ ≫ (Nonsingular.iso Y✝.simplex ⋯).hom = (Nonsingular.iso X✝.simplex ⋯).hom ≫ X.functorN.map x✝

Tactic:
by

Goal state after:
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
⊢ m = desc s

Tactic:
by

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

Goal state before:
pp: 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
⊢ j ≤ i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u
inst✝ : PartialOrder X
x✝² x✝¹ : NonemptyFiniteChains X
x✝ : x✝².finset = x✝¹.finset
⊢ x✝² = x✝¹

Tactic:
by

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

Tactic:
by

Goal state after:
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)
j : Fin (n + 2)
hj : i.succ < j
⊢ i ≠ Fin.last n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
⊢ ∀ (a b : ↥(Finset.image (⇑f) s.finset)), a ≤ b ∨ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
s : NonemptyFiniteChains X
f : X →o Y
y : Y
⊢ y ∈ (s.map f).finset ↔ ∃ x ∈ s.finset, f x = y

Tactic:
by

Goal state after:
Module: Mathlib.Order.NonemptyFiniteChains

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PartialOrder X
inst✝ : PartialOrder Y
f : X →o Y
a b : NonemptyFiniteChains X
h : a ≤ b
x : Y
hx : x ∈ ((fun s ↦ s.map f) a).finset
⊢ x ∈ ((fun s ↦ s.map f) b).finset

Tactic:
by

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

Goal state before:
pp: 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
⊢ i.castSucc < j

Tactic:
by

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

Tactic:
by

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'
⊢ stdSimplex.δ i.castSucc ≫ r.map = f'.map

Tactic:
by

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'
⊢ stdSimplex.δ i.succ ≫ r.map = g'.map

Tactic:
by

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
⊢ stdSimplex.δ j ≫ r.map = const x

Tactic:
by

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
⊢ stdSimplex.δ j ≫ r.map = const x

Tactic:
by

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
⊢ stdSimplex.δ j.castSucc.castSucc ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = f.op.map

Tactic:
by

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
⊢ stdSimplex.δ j.castSucc.succ ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = fg.op.map

Tactic:
by

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
⊢ stdSimplex.δ j.succ.succ ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = g.op.map

Tactic:
by

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
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ i.succ.succ < k.rev

Tactic:
by

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
k : Fin (n + 2)
hk : k < j.castSucc.castSucc
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = const (opObjEquiv.symm x)

Tactic:
by

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
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ k.rev < i.castSucc.castSucc

Tactic:
by

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
k : Fin (n + 2)
hk : j.succ.succ < k
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv.symm (yonedaEquiv h.map)) = const (opObjEquiv.symm x)

Tactic:
by

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
⊢ stdSimplex.δ j.castSucc.castSucc ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = g.map

Tactic:
by

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
⊢ stdSimplex.δ j.castSucc.succ ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = fg.map

Tactic:
by

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
⊢ stdSimplex.δ j.succ.succ ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = f.map

Tactic:
by

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
⊢ i.succ.succ < k.rev

Tactic:
by

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
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = const x

Tactic:
by

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 : j.succ.succ < k
⊢ k.rev < i.castSucc.castSucc

Tactic:
by

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 : j.succ.succ < k
⊢ stdSimplex.δ k ≫ yonedaEquiv.symm (opObjEquiv (yonedaEquiv h.map)) = const x

Tactic:
by

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 : f.RelStruct g i.castSucc
j : Fin (n + 2)
hj : i.succ.succ < j
⊢ i.castSucc.succ < i.succ.succ

Tactic:
by

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

Tactic:
by

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 : f.RelStruct g i.succ
⊢ stdSimplex.δ i.castSucc.succ ≫ h.map = f.map

Tactic:
by

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 : f.RelStruct g i.succ
j : Fin (n + 2)
hj : j < i.castSucc.castSucc
⊢ i.castSucc.castSucc < i.succ.castSucc

Tactic:
by

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.succ.castSucc
⊢ stdSimplex.δ j ≫ h.map = const x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.TopologicalSimplex

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.TopologicalSimplex

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularSet

Goal state before:
pp: S : SSet
m : SimplexCategoryᵒᵖ
a : S.obj m
⊢ ((ConcreteCategory.hom ((sSetTopAdj.unit.app S).app m)) a).down =
    SSet.toTopSimplex.inv.app (Opposite.unop m) ≫ SSet.toTop.map (SSet.yonedaEquiv.symm a)

Tactic:
by

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ ⇑m.toTopHomeo ∘ ⇑(ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) =
    stdSimplex.map ⇑(ConcreteCategory.hom f) ∘ ⇑n.toTopHomeo

Tactic:
by

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ ⇑m.toTopHomeo.symm ∘ stdSimplex.map ⇑(ConcreteCategory.hom f) =
    ⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) ∘ ⇑n.toTopHomeo.symm

Tactic:
by

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

Goal state before:
pp: X : TopCat
x : ↑X
⊢ Continuous fun x_1 ↦ x

Tactic:
by

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

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))), ↑X)
⊢ (fun x ↦ { toFun := fun x_1 ↦ x, continuous_toFun := ⋯ }) ((fun f ↦ f.toFun default) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: X : TopCat
n m : SimplexCategory
f : n ⟶ m
g : C(↑(stdSimplex ℝ (Fin (m.len + 1))), ↑X)
⊢ Continuous (stdSimplex.map ⇑(ConcreteCategory.hom f))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : TopCat
x✝ : C(↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))), ↑X)
⊢ (fun f ↦ (Hom.hom f).comp ↑stdSimplexHomeomorphI) ((fun f ↦ ofHom (f.comp ↑stdSimplexHomeomorphI.symm)) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: X : TopCat
x✝ : I ⟶ X
⊢ (fun f ↦ ofHom (f.comp ↑stdSimplexHomeomorphI.symm)) ((fun f ↦ (Hom.hom f).comp ↑stdSimplexHomeomorphI) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: X : TopCat
s : toSSet.obj X _⦋1⦌
⊢ (CategoryTheory.ConcreteCategory.hom (toSSetObj₁Equiv s)) 0 =
    toSSetObj₀Equiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1)) s)

Tactic:
by

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

Goal state before:
pp: X : TopCat
s : toSSet.obj X _⦋1⦌
⊢ (CategoryTheory.ConcreteCategory.hom (toSSetObj₁Equiv s)) 1 =
    toSSetObj₀Equiv ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 0)) s)

Tactic:
by

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

Goal state before:
pp: X : TopCat
f : I ⟶ X
⊢ toSSetObj₀Equiv
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1))
        (toSSetObj₁Equiv.symm f)) =
    toSSetObj₀Equiv (toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) 0))

Tactic:
by

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

Goal state before:
pp: X : TopCat
f : I ⟶ X
⊢ toSSetObj₀Equiv
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 0))
        (toSSetObj₁Equiv.symm f)) =
    toSSetObj₀Equiv (toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) 1))

Tactic:
by

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

Goal state before:
pp: X : TopCat
x y : ↑X
x✝ : SSet.Edge (toSSetObj₀Equiv.symm x) (toSSetObj₀Equiv.symm y)
⊢ (fun p ↦ SSet.Edge.mk (toSSetObj₁Equiv.symm p.hom) ⋯ ⋯)
      ((fun e ↦ { hom := toSSetObj₁Equiv e.edge, hom₀ := ⋯, hom₁ := ⋯ }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : TopCat
x y : ↑X
x✝ : X.Path x y
⊢ (fun e ↦ { hom := toSSetObj₁Equiv e.edge, hom₀ := ⋯, hom₁ := ⋯ })
      ((fun p ↦ SSet.Edge.mk (toSSetObj₁Equiv.symm p.hom) ⋯ ⋯) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
⊢ (singularChainComplexFunctor C).Additive

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SingularHomology.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
n : ℕ
inst✝ : HasPullbacks C
X : C
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ Mono (((singularChainComplexFunctor C).obj X).map f)

Tactic:
by

Goal state after: