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

Goal state before:
pp: case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx✝⟩
⊢ IsIso f

Tactic:
]

Goal state after:
case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx✝⟩
⊢ IsIso f
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.N
h : ∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.dim ≤ y.dim

Tactic:
]

Goal state after:
X : SSet
x y : X.N
h : ∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.dim ≤ y.dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx✝⟩
hf : ¬IsIso f
h : n ≤ m
⊢ ⦋n⦌.len = ⦋m⦌.len

Tactic:
]

Goal state after:
case mk
X : SSet
n : ℕ
x : X _⦋n⦌
hx✝ : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑⟨x, hx✝⟩
hf : ¬IsIso f
h : n ≤ m
⊢ ⦋n⦌.len = ⦋m⦌.len
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (∀ (x : SimplexCategoryᵒᵖ), (range f).obj x = ⊤.obj x) ↔ ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ (∀ (x : SimplexCategoryᵒᵖ), (range f).obj x = ⊤.obj x) ↔ ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : Epi f
⊢ Epi f

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝ : Epi f
⊢ Epi f
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
]

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
⊢ ↑x = ↑x

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
]

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
this : IsIso (factorThruImage f)
⊢ Mono (factorThruImage f ≫ image.ι f)

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
this : IsIso (factorThruImage f)
⊢ Mono (factorThruImage f ≫ image.ι f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ range f ≤ range f

Tactic:
]

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

Goal state before:
pp: case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x ∈
    (ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)).obj (Opposite.op ⦋n⦌)

Tactic:
]

Goal state after:
case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x ∈
    (ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)).obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h : ∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) (mk ↑⟨x₂, hx₂⟩ ⋯).simplex = (mk ↑⟨x₁, hx₁⟩ ⋯).simplex
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯

Tactic:
]

Goal state after:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h : ∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) (mk ↑⟨x₂, hx₂⟩ ⋯).simplex = (mk ↑⟨x₁, hx₁⟩ ⋯).simplex
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
]

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

Goal state before:
pp: case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x ∈ ((ofSimplex x).image f).obj (Opposite.op ⦋n⦌)

Tactic:
]

Goal state after:
case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x ∈ ((ofSimplex x).image f).obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.ι ≫ f) ≤ range (A.ι ≫ f)

Tactic:
]

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

Goal state before:
pp: case a
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ y.subcomplex ≤ y.subcomplex

Tactic:
]

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.toImage f) = ⊤

Tactic:
]

Goal state after:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.toImage f) = ⊤
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
]

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ S ≤ ((fun S ↦ S.image f) T).preimage f

Tactic:
]

Goal state after:
X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ S ≤ ((fun S ↦ S.image f) T).preimage f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this :
  (ConcreteCategory.hom (X.map (factorThruImage (g hf₁ f₂)).op))
      ((ConcreteCategory.hom (X.map (image.ι (g hf₁ f₂)).op)) y₂) =
    ↑y₁
⊢ IsIso (factorThruImage (g hf₁ f₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ T.image f ≤ (fun S ↦ S.image f) T

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
]

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

Goal state before:
pp: X : SSet
⊢ ∀ (i : (p : ℕ) × ↑(X.nonDegenerate p)), Subcomplex.ofSimplex ↑i.snd ≤ ⨆ s, s.subcomplex

Tactic:
]

Goal state after:
X : SSet
⊢ ∀ (i : (p : ℕ) × ↑(X.nonDegenerate p)), Subcomplex.ofSimplex ↑i.snd ≤ ⨆ s, s.subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
⊢ B.preimage f = ⊤ ↔ B.preimage f = ⊤

Tactic:
]

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

Goal state before:
pp: X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
⊢ B.preimage f ≤ B.preimage f

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j : ι
⊢ WidePullback.π (fun x ↦ terminal.from X) j = WidePullback.π (fun x ↦ terminal.from X) j

Tactic:
]

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

Goal state before:
pp: X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op ⦋n⦌) → ↑x ∈ B.obj (Opposite.op ⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
]

Goal state after:
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op ⦋n⦌) → ↑x ∈ B.obj (Opposite.op ⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
]

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this : IsIso (factorThruImage (g hf₁ f₂))
⊢ Mono (factorThruImage (g hf₁ f₂) ≫ image.ι (g hf₁ f₂))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : ℕ
x y : ↑(X.nonDegenerate n)
h :
  ∃ (h : ((fun x ↦ N.mk ↑x ⋯) x).dim = ((fun x ↦ N.mk ↑x ⋯) y).dim),
    (((fun x ↦ N.mk ↑x ⋯) x).cast h).simplex = ((fun x ↦ N.mk ↑x ⋯) y).simplex
⊢ x = y

Tactic:
]

Goal state after:
X : SSet
inst✝ : X.Finite
n : ℕ
x y : ↑(X.nonDegenerate n)
h :
  ∃ (h : ((fun x ↦ N.mk ↑x ⋯) x).dim = ((fun x ↦ N.mk ↑x ⋯) y).dim),
    (((fun x ↦ N.mk ↑x ⋯) x).cast h).simplex = ((fun x ↦ N.mk ↑x ⋯) y).simplex
⊢ x = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: case neg
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
]

Goal state after:
case neg
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : Finset.image φ ⊤ = ∅
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case pos
X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
y : Fin (m + 1)
hy : y = (SimplexCategory.Hom.toOrderHom f₁) x
⊢ (SimplexCategory.Hom.toOrderHom f₁) x = (SimplexCategory.Hom.toOrderHom f₁) x

Tactic:
]

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) ((ConcreteCategory.hom (X.map f.op)) y.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex ↔
    (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
]

Goal state after:
X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) ((ConcreteCategory.hom (X.map f.op)) y.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex ↔
    (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite (Y _⦋i⦌)

Tactic:
]

Goal state after:
X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : ∀ (k : SimplexCategoryᵒᵖ), Epi (f.app k)
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite (Y _⦋i⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case a
X : SSet
x✝¹ x✝ : X.N
h : x✝¹.subcomplex = x✝.subcomplex
⊢ x✝.subcomplex ≤ x✝.subcomplex

Tactic:
]

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this : IsSplitEpi f
⊢ Mono (X.map f.op)

Tactic:
]

Goal state after:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this : IsSplitEpi f
⊢ Mono (X.map f.op)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, s⟩ => N.mk ((ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex) ⋯)
        a =
      N.mk ↑⟨⟨s, h₁⟩, h₂✝⟩ ⋯

Tactic:
]

Goal state after:
X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, s⟩ => N.mk ((ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex) ⋯)
        a =
      N.mk ↑⟨⟨s, h₁⟩, h₂✝⟩ ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))) ↔
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
]

Goal state after:
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))) ↔
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ↑⟨s, hi⟩ ∈ X.nonDegenerate d

Tactic:
]

Goal state after:
X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ↑⟨s, hi⟩ ∈ X.nonDegenerate d
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: X : SSet
x : X.S
y₁ y₂ : X.N
h₁ : y₁.subcomplex = x.subcomplex
h₂ : y₂.subcomplex = x.subcomplex
⊢ x.subcomplex = x.subcomplex

Tactic:
]

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

Goal state before:
pp: X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : y.subcomplex = { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex
⊢ y = N.mk ↑z ⋯

Tactic:
]

Goal state after:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : y.subcomplex = { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex
⊢ y = N.mk ↑z ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr.mk
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
a : A.toSSet _⦋m⦌
ha : ↑a ∈ X.nonDegenerate m
hx : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ A.obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ B.obj (op ⦋n⦌)

Tactic:
]

Goal state after:
case mpr.mk
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
a : A.toSSet _⦋m⦌
ha : ↑a ∈ X.nonDegenerate m
hx : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ A.obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom (↾fun x ↦ ⟨(ConcreteCategory.hom (X.map f.op)) ↑x, ⋯⟩)) a) ∈ B.obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : y.subcomplex = { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex
⊢ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex = (N.mk ↑z ⋯).subcomplex

Tactic:
]

Goal state after:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : y.subcomplex = { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex
⊢ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.subcomplex = (N.mk ↑z ⋯).subcomplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
⊢ ∀ (n : ℕ), X.nonDegenerate n ⊆ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)

Tactic:
]

Goal state after:
X : SSet
⊢ ∀ (n : ℕ), X.nonDegenerate n ⊆ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X Y : SSet
n : ℕ
f : X ⟶ Y
m : ℕ
hm : m < n
g : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
⊢ (ConcreteCategory.hom (Y.map g.op)) ((ConcreteCategory.hom (f.app (op ⦋m⦌))) y) =
    (ConcreteCategory.hom (Y.map g.op)) ((ConcreteCategory.hom (f.app (op ⦋m⦌))) y)

Tactic:
]

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

Goal state before:
pp: X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔
    ↑((ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x) ∈ Y.degenerate n

Tactic:
]

Goal state after:
X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔
    ↑((ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x) ∈ Y.degenerate n