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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
x✝ : Fin (⦋n⦌.len + 1)
⊢ x✝ ∈
      Finset.image
        ⇑(Hom.toOrderHom
            (objEquiv
              (objMk
                ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))))
        ⊤ →
    x✝ ∈ S

Tactic:
by

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 : ℕ
⊢ 0 + ↑(Fin.last n) = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x✝ : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : x ∈ (face S).obj (op j)
i : Fin (j.len + 1)
⊢ (Hom.toOrderHom (objEquiv x)) i ∈ Finset.image ⇑(Hom.toOrderHom (objEquiv x)) ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x✝ : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : x ∈ (face S).obj (op j)
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
⊢ ⟨(Hom.toOrderHom (objEquiv x)) i₁, ⋯⟩ ≤ ⟨(Hom.toOrderHom (objEquiv x)) i₂, ⋯⟩

Tactic:
by

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

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

Tactic:
by

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 : ℕ
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = (X.hom ≫ ed.section_).app (op ⦋n⦌)

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x✝ : (face S).toSSet.obj (op j)
x : Δ[n].obj (op 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:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
X✝ X'✝ : SimplexCategory
f : X✝ ⟶ X'✝
g : X'✝ ⟶ ⦋m⦌
⊢ {
        toFun := fun f ↦
          ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))),
            ⋯⟩,
        invFun := fun x ↦
          match x with
          | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
      (f ≫ g) =
    (ConcreteCategory.hom ((face S).toSSet.map f.op))
      ({
          toFun := fun f ↦
            ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))),
              ⋯⟩,
          invFun := fun x ↦
            match x with
            | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }
        g)

Tactic:
by

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

Goal state before:
pp: X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X✝ Y✝ : SimplexCategoryᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ Δ[m].map x✝ ≫ (objEquiv.trans h.homEquiv).toIso.hom = (objEquiv.trans h.homEquiv).toIso.hom ≫ X.map x✝

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.range (stdSimplex.δ i) = face {i}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
d : SimplexCategoryᵒᵖ
x✝ : unop d ⟶ ⦋n⦌
⊢ (fun f ↦ Hom.mk (ULift.orderIso.{u, 0}.toOrderEmbedding.toOrderHom.comp (Functor.toOrderHom f)))
      ((fun f ↦ ⋯.functor) x✝) =
    x✝

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ Δ[n].nonDegenerate d ↔ StrictMono ⇑s

Tactic:
by

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 : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
⊢ h ed j.succ ≫ X.left.δ i.castSucc = ((𝟭 (SimplicialObject C)).obj X.left).δ i ≫ h ed j

Tactic:
by

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

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ Δ[n].nonDegenerate d ↔ Mono (objEquiv s)

Tactic:
by

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

Goal state before:
pp: n d : ℕ
f : ⦋d⦌ ⟶ ⦋n⦌
⊢ objEquiv.symm f ∈ Δ[n].nonDegenerate d ↔ Mono f

Tactic:
by

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

Goal state before:
pp: n d : ℕ
s : Fin (d + 1) ↪o Fin (n + 1)
⊢ objEquiv.symm (Hom.mk s.toOrderHom) ∈ Δ[n].nonDegenerate d

Tactic:
by

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

Goal state before:
pp: n d : ℕ
x✝ : ↑(Δ[n].nonDegenerate d)
⊢ (fun s ↦ ⟨objEquiv.symm (Hom.mk s.toOrderHom), ⋯⟩) ((fun s ↦ OrderEmbedding.ofStrictMono ⇑↑s ⋯) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
⊢ Mono (objEquiv x)

Tactic:
by

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

Goal state before:
pp: n i : ℕ
hi : n + 1 ≤ i
⊢ Δ[n].degenerate i = ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : { x // x ≠ i }
x : Fin (n + 1 + 1)
hx : x ≠ i
⊢ x ∈ {i}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : ↥{i}ᶜ
x : Fin (n + 2)
hx : x ∈ {i}ᶜ
⊢ x ≠ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ (RelEmbedding.trans (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb) x✝¹ =
    (RelEmbedding.trans (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb) x✝

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ l ∈ Set.range j.succAbove

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ l ∈ Set.range j.succAbove

Tactic:
by
        grind [Fin.range_succAbove, mem_compl, Fin.succAbove]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : j.succAbove m ∈ {i, j}ᶜ
⊢ m ∈ Set.range (i.castPred ⋯).succAbove

Tactic:
by

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 : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑k + (↑i + 1) = n + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : j.succAbove m ∈ {i, j}ᶜ
k : Fin n
hk : (i.castPred ⋯).succAbove k = m
⊢ (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) k = ⟨j.succAbove m, hl⟩

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
⊢ Fin n ≃ ↥{i, j}ᶜ

Tactic:
by

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 : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑k + 1 + ↑i = n + 1

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
⊢ i ≤ j

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ (facePairComplIso i j h).hom ≫ (face {i, j}ᶜ).ι = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ face {i, j}ᶜ ≤ face {i}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso i).inv = (facePairComplIso i j h).inv ≫ stdSimplex.δ (j.pred ⋯)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ face {i, j}ᶜ ≤ face {j}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso j).inv = (facePairComplIso i j h).inv ≫ stdSimplex.δ (i.castPred ⋯)

Tactic:
by

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

Goal state before:
pp: ⊢ (faceSingletonIso 0).hom ≫ (face {0}).ι = stdSimplex.δ 1

Tactic:
by

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

Goal state before:
pp: ⊢ (faceSingletonIso 1).hom ≫ (face {1}).ι = stdSimplex.δ 0

Tactic:
by

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 : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑k + 1 + (↑i + 1) = n + 1 + 1

Tactic:
by

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

Goal state before:
pp: n m : ℕ
x✝ : { x // x ∈ Δ[n].nonDegenerate m }
x : Δ[n] _⦋m⦌
hx : Function.Injective ⇑(Hom.toOrderHom (objEquiv x))
⊢ Function.Injective ⇑(Hom.toOrderHom (objEquiv x))

Tactic:
by

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

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 : Fin (n + 1)
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ

Tactic:
by

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 : Fin (n + 2)
j : Fin (n + 1)
hij : ↑j.succ ≤ ↑i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j.succ + l = ↑i
⊢ ↑i = ↑j + 1 + l

Tactic:
by

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 : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ l, ↑i = ↑j + 1 + l

Tactic:
by

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 : 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
⊢ l + 1 < ↑k + 2

Tactic:
by

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

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 : 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
⊢ l + 2 < ↑k + 1 + 2

Tactic:
by

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 : 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
⊢ ↑k + 1 + ↑j.castSucc = n + 1

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ Function.Bijective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩

Tactic:
by

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

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
⊢ j ∈ ↑(nonDegenerateEquiv' x) ↔ ∃ i, ↑x i = j

Tactic:
by

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

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
i : Fin (d + 1)
⊢ i ∈ univ

Tactic:
by

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 : 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
⊢ ↑k + ↑j.castSucc = n

Tactic:
by

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))
x✝¹ x✝ : Fin (d + 1)
h : (fun i ↦ ⟨↑x i, ⋯⟩) x✝¹ = (fun i ↦ ⟨↑x i, ⋯⟩) x✝
⊢ (Hom.toOrderHom (objEquiv ↑x)) x✝¹ = (Hom.toOrderHom (objEquiv ↑x)) x✝

Tactic:
by

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

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Bijective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
by

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 : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
⊢ h ed j.castSucc ≫ X.left.δ i.succ = ((𝟭 (SimplicialObject C)).obj X.left).δ i ≫ h ed j

Tactic:
by

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

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ ∀ {a b : Fin (d + 1)},
    (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: n d : ℕ
S : ↑{S | #S = d + 1}
i : Fin (d + 1)
⊢ ↑(nonDegenerateEquiv'.symm S) i ∈ ↑S

Tactic:
by

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

Goal state before:
pp: n d : ℕ
S : ↑{S | #S = d + 1}
A : Δ[n].Subcomplex
⊢ ↑(nonDegenerateEquiv'.symm S) ∈ A.obj (op ⦋d⦌) ↔ face ↑S ≤ A

Tactic:
by

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

Goal state before:
pp: n : SimplexCategory
d : SimplexCategoryᵒᵖ
⊢ Finite ((stdSimplex.obj n).obj d)

Tactic:
by

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

Goal state before:
pp: n : SimplexCategory
⊢ (stdSimplex.obj n).Finite

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ (Subcomplex.ofSimplex x).toSSet.Finite

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
hm : #S = 0
⊢ S = ∅

Tactic:
by

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
⊢ ↑k + (↑j + 1) = n + 1

Tactic:
by

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
⊢ ↑k + 1 + ↑j = n + 1

Tactic:
by

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

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

Tactic:
by

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
⊢ h ed j ≫ X.left.σ i.castSucc = ((𝟭 (SimplicialObject C)).obj X.left).σ i ≫ h ed j.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
⊢ (face S).toSSet.HasDimensionLT d

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Subcomplex.ofSimplex (objEquiv.symm (𝟙 ⦋n⦌)) ≤ ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
f : unop x✝¹ ⟶ ⦋n⦌
x✝ : objEquiv.symm f ∈ ⊤.obj x✝¹
⊢ (ConcreteCategory.hom (Δ[n].map f.op)) (objEquiv.symm (𝟙 ⦋n⦌)) = objEquiv.symm f

Tactic:
by

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 : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ l < ↑k + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x : Δ[n].obj x✝¹
x✝ : x ∈ ⊤.obj x✝¹
⊢ x ∈ (Subcomplex.ofSimplex (objEquiv.symm (𝟙 ⦋n⦌))).obj x✝¹

Tactic:
by

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 : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ ↑k + ↑j.castSucc = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ Δ[n].nonDegenerate n

Tactic:
by

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 : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ l + 1 < ↑k + 1 + 1

Tactic:
by

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 : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ ↑k + 1 + ↑j = n + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h : objEquiv.symm f ∈ Δ[n].nonDegenerate n
⊢ Mono f

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Δ[n].nonDegenerate n = {objEquiv.symm (𝟙 (unop (op ⦋n⦌)))}

Tactic:
by

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 : j ≤ i
⊢ h ed j ≫ X.left.σ i.succ = ((𝟭 (SimplicialObject C)).obj X.left).σ i ≫ h ed j.castSucc

Tactic:
generalize hk : j.rev = k
    obtain ⟨l, hl⟩ := Nat.le.dest (Fin.le_def.1 hij)
    dsimp
    rw [h_eq_assoc _ _ k, h_eq _ _ (k + 1),
      X.left.σ_δ₀Iter'_assoc _ _ ⟨l, by grind⟩
        (by grind),
      ← ed.s_comp_σ_assoc,
      X.left.σ₀Iter_σ' j i.succ ⟨l + 1, by grind⟩ (by grind)]
    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 : j ≤ i
⊢ h ed j ≫ X.left.σ i.succ = ((𝟭 (SimplicialObject C)).obj X.left).σ i ≫ h ed j.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, k with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ i₂ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
by

Goal state after: