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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X _⦋0⦌
⊢ (ofSimplex x).ι = const x

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.N
⊢ x = y ↔ x.toS = y.toS

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
y : X.obj m
⊢ y ∈ (ofSimplex x).obj m ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) x = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: 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
⊢ Function.LeftInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ (ConcreteCategory.hom (X.map f.op)) x = (ConcreteCategory.hom (X.map f.op)) x

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.N
h : x ≤ y
⊢ x.dim ≤ y.dim

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ ofSimplex ((ConcreteCategory.hom (X.map f.op)) x) ≤ ofSimplex x

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
this : IsSplitEpi f
⊢ (ConcreteCategory.hom (X.map (section_ f).op)) ((ConcreteCategory.hom (X.map f.op)) x) = x

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
⊢ ofSimplex ((ConcreteCategory.hom (X.map f.op)) x) = ofSimplex x

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ range f = ⊤ ↔ Epi f

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
p : Y ⟶ X
U✝ V✝ : SimplexCategoryᵒᵖ
f : U✝ ⟶ V✝
⊢ ⇑(ConcreteCategory.hom (p.app U✝)) ⁻¹' ⇑(ConcreteCategory.hom (X.map f)) ⁻¹' A.obj V✝ ⊆
    ⇑(ConcreteCategory.hom (Y.map f)) ⁻¹' ⇑(ConcreteCategory.hom (p.app V✝)) ⁻¹' A.obj V✝

Tactic:
by

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

Goal state before:
pp: X Y : SSet
ι : Type u_1
A : ι → X.Subcomplex
p : Y ⟶ X
⊢ (⨆ i, A i).preimage p = ⨆ i, (A i).preimage p

Tactic:
by

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

Goal state before:
pp: X Y : SSet
ι : Type u_1
A : ι → X.Subcomplex
p : Y ⟶ X
⊢ (⨅ i, A i).preimage p = ⨅ i, (A i).preimage p

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom (X.map (factorThruImage f).op)) ((ConcreteCategory.hom (X.map (image.ι f).op)) y) = ↑x

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
⊢ A.preimage A.ι = ⊤

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
Z : Y.Subcomplex
⊢ A.image f ≤ Z ↔ A ≤ Z.preimage f

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ ⊤.image f = range f

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
⊢ A.image (𝟙 X) = A

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
Z : SSet
g : Y ⟶ Z
⊢ A.image (f ≫ g) = (A.image f).image g

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
Z : SSet
g : Y ⟶ Z
⊢ range (f ≫ g) = (range f).image g

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
x : X _⦋d⦌
hx : x ∈ X.nonDegenerate d
y : X _⦋d⦌
hy : y ∈ X.nonDegenerate d
h : mk ↑⟨x, hx⟩ ⋯ < mk ↑⟨y, hy⟩ ⋯
w✝ : Mono (𝟙 ⦋(mk ↑⟨x, hx⟩ ⋯).dim⦌)
hf : (ConcreteCategory.hom (X.map (𝟙 ⦋(mk ↑⟨x, hx⟩ ⋯).dim⦌).op)) (mk ↑⟨y, hy⟩ ⋯).simplex = (mk ↑⟨x, hx⟩ ⋯).simplex
⊢ y = x

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: 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
⊢ Function.RightInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ (wideCospan ι X).obj none)

Tactic:
by

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

Goal state before:
pp: X Y : SSet
ι : Type u_1
S : ι → X.Subcomplex
f : X ⟶ Y
⊢ (⨆ i, S i).image f = ⨆ i, (S i).image f

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (range f).preimage f ≤ ⊤

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ ⊤ ≤ (range f).preimage f

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.N
h : x < y
⊢ x.dim < y.dim

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ A.image f ≤ range f

Tactic:
by

Goal state after:
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₂
⊢ (ConcreteCategory.hom (X.map (g hf₁ f₂).op)) y₂ = ↑y₁

Tactic:
by

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
i j : WidePullbackShape ι
f : i ⟶ j
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map f ≫
      Option.casesOn j (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn i (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map f

Tactic:
by

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

Goal state before:
pp: X : SSet
x₁ x₂ : X.N
h : x₁ ≤ x₂
h' : x₂ ≤ x₁
⊢ x₁ = x₂

Tactic:
by

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

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

Tactic:
by

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)
j : WidePullbackShape ι
⊢ (Pi.lift fun j ↦ s.π.app (some j)) ≫
      { 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
        none =
    s.π.app none

Tactic:
by

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

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

Tactic:
by

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:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.N
⊢ x = y → x.subcomplex = y.subcomplex

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
s : X.N
d : ℕ
hd : s.dim = d
⊢ (s.cast hd).simplex ∈ X.nonDegenerate (s.cast hd).dim

Tactic:
by

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

Goal state before:
pp: X : SSet
s : X.N
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ ⨆ s, s.subcomplex ≤ ⊤

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Monotone fun S ↦ S.image f

Tactic:
by

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
⊢ f = Pi.lift fun j ↦ s.π.app (some j)

Tactic:
by

Goal state after:
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₂
⊢ IsIso (factorThruImage (g hf₁ f₂))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
s : X _⦋d⦌
hs : s ∈ X.nonDegenerate d
⊢ Subcomplex.ofSimplex ↑⟨d, ⟨s, hs⟩⟩.snd ≤ (mk s hs).subcomplex

Tactic:
by

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
⊢ HasWidePullback (Arrow.mk (terminal.from X)).right (fun x ↦ (Arrow.mk (terminal.from X)).left) fun x ↦
    (Arrow.mk (terminal.from X)).hom

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ ⊤ ≤ ⨆ s, s.subcomplex

Tactic:
by

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 : ι
⊢ (limitIsoPi ι X).hom ≫ Pi.π (fun x ↦ X) j = WidePullback.π (fun x ↦ terminal.from X) j

Tactic:
by

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
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
⊢ (Arrow.mk (terminal.from X)).cechNerve.map f ≫
      (wideCospan.limitIsoPi (Fin ((Opposite.unop n).len + 1)) (Arrow.mk (terminal.from X)).left).hom =
    (wideCospan.limitIsoPi (Fin ((Opposite.unop m).len + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
      (cechNerveTerminalFrom X).map f

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst✝ : IsIso f
n : SimplexCategoryᵒᵖ
y : Y.obj n
hy : y ∈ B.obj n
⊢ (ConcreteCategory.hom ((inv f).app n)) y ∈ (B.preimage f).obj n ∧
    (ConcreteCategory.hom (f.app n)) ((ConcreteCategory.hom ((inv f).app n)) y) = y

Tactic:
by

Goal state after:
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₂
⊢ Mono (g hf₁ f₂)

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst✝ : IsIso f
⊢ (B.preimage f).image f = B

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, Finite ↑(X.nonDegenerate i)
this✝ : ∀ (i : Fin d), Finite ↑(X.nonDegenerate ↑i)
x : X.N
hj : ¬x.dim < d
this : x.simplex ∈ X.nonDegenerate x.dim
⊢ d ≤ x.dim

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, Finite ↑(X.nonDegenerate i)
⊢ Finite X.N

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
d : ℕ
hd : (Finset.image φ ⊤).max = ↑d
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.image φ ⊤
⊢ x✝¹ < d + 1

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
hx : (ConcreteCategory.hom (inv (f.app x✝))) x ∈ A.obj x✝
⊢ (ConcreteCategory.hom ((inv f).app x✝)) x ∈ A.obj x✝ ∧
    (ConcreteCategory.hom (f.app x✝)) ((ConcreteCategory.hom ((inv f).app x✝)) x) = x

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
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₂
hf₁ : SplitEpi f₁
⊢ g hf₁ f₂ = 𝟙 ⦋m⦌

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
⊢ (∃ x_1 ∈ A.obj x✝, (ConcreteCategory.hom (f.app x✝)) x_1 = x) → (ConcreteCategory.hom (inv (f.app x✝))) x ∈ A.obj x✝

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
⊢ A.preimage (inv f) = A.image f

Tactic:
by

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

Goal state before:
pp: X : SSet
A B : X.Subcomplex
⊢ A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y : SSet
A : Y.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
⊢ A.image (inv f) = A.preimage f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X.op.N
⊢ opObjEquiv x.simplex ∈ X.nonDegenerate x.dim

Tactic:
by

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

Goal state before:
pp: X : SSet
y : X.N
⊢ opObjEquiv.symm y.simplex ∈ X.op.nonDegenerate y.dim

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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₂
⊢ y₁ = y₂

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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)
this : ∃ hf₁, (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
⊢ (SimplexCategory.Hom.toOrderHom f₁) x = (SimplexCategory.Hom.toOrderHom f₂) x

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.op.N
f : ⦋(mk (opObjEquiv x.simplex) ⋯).dim⦌ ⟶ ⦋(mk (opObjEquiv y.simplex) ⋯).dim⦌
hf : (ConcreteCategory.hom (X.map f.op)) (mk (opObjEquiv y.simplex) ⋯).simplex = (mk (opObjEquiv x.simplex) ⋯).simplex
⊢ (ConcreteCategory.hom (X.op.map (SimplexCategory.rev.map f).op)) y.simplex = x.simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
d : ℕ
hd : ∀ s ∈ Finset.image φ ⊤, s < d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ φ (N.mk x hx) ∈ Finset.image φ ⊤

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
⊢ ∃ d, X.HasDimensionLT d

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.op.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : (ConcreteCategory.hom (X.op.map f.op)) y.simplex = x.simplex
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.rev.map f).op)) (mk (opObjEquiv y.simplex) ⋯).simplex =
    (mk (opObjEquiv x.simplex) ⋯).simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋↑m⦌) × ↑(X.nonDegenerate ↑m) → X _⦋n⦌ :=
  fun x ↦
    match x with
    | ⟨m, ⟨f, x⟩⟩ => (ConcreteCategory.hom (X.map f.op)) ↑x
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
y : ↑(X.nonDegenerate m)
this : m ≤ n
⊢ m < n + 1

Tactic:
by

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

Goal state before:
pp: case mpr
X : SSet
x y : X.op.N
⊢ (∃ f, (ConcreteCategory.hom (X.op.map f.op)) y.simplex = x.simplex) →
    ∃ f,
      (ConcreteCategory.hom (X.map f.op)) (mk (opObjEquiv y.simplex) ⋯).simplex = (mk (opObjEquiv x.simplex) ⋯).simplex

Tactic:
· rintro ⟨f, hf⟩
      exact ⟨SimplexCategory.rev.map f, by simp [op_map, ← hf]⟩

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

Goal state before:
pp: X : SSet
x y : X.op.N
⊢ { toFun := fun x ↦ mk (opObjEquiv x.simplex) ⋯, invFun := fun y ↦ mk (opObjEquiv.symm y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        x ≤
      { toFun := fun x ↦ mk (opObjEquiv x.simplex) ⋯, invFun := fun y ↦ mk (opObjEquiv.symm y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        y ↔
    x ≤ y

Tactic:
by

Goal state after: