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

Goal state before:
pp: case left
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X✝))

pp: case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
·

Goal state after:
case left
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
·

Goal state after:
case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂.refine_1
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.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x

pp: case h₂.refine_2
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.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x

Tactic:
·

Goal state after:
case h₂.refine_1
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.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂.refine_2
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.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x

Tactic:
·

Goal state after:
case h₂.refine_2
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.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x
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.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x = A.right.app x

Tactic:
refine WidePushout.hom_ext _ _ _ (fun j => ?_) ?_
      · dsimp
        simp only [Category.assoc, ← NatTrans.naturality A.right, Arrow.augmentedCechConerve_right,
          SimplexCategory.len_mk, Arrow.cechConerve_map, colimit.ι_desc,
          WidePushoutShape.mkCocone_ι_app, colimit.ι_desc_assoc]
        rfl
      · dsimp
        rw [colimit.ι_desc]
        exact congr_app A.w x

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.left (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.left A

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 (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = 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.left (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.left A
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

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

pp: case inr
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
⊢ x.dim < y.dim

Tactic:
·

Goal state after:
case inl
X : SSet
x y : X.N
h : x < y
h' : x.dim < y.dim
⊢ x.dim < y.dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case inr
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
⊢ x.dim < y.dim

Tactic:
·

Goal state after:
case inr
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
⊢ x.dim < y.dim
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 (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = 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 (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)) = Arrow.Hom.right A
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case id
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i : WidePullbackShape ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.id 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 }) =
    (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 (WidePullbackShape.Hom.id i)

pp: case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.term j✝) ≫
      Option.casesOn none (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn (some j✝) (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
        fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)

Tactic:
·

Goal state after:
case id
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i : WidePullbackShape ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.id 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 }) =
    (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 (WidePullbackShape.Hom.id i)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

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

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.term j✝) ≫
      Option.casesOn none (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn (some j✝) (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
        fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)

Tactic:
·

Goal state after:
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).map (WidePullbackShape.Hom.term j✝) ≫
      Option.casesOn none (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
        limit.π (Discrete.functor fun x ↦ X) { as := i }) =
    (Option.casesOn (some j✝) (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
        fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i }) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

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

Tactic:
·

Goal state after:
case a
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ x ≤ y
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

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

Tactic:
·

Goal state after:
case a
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ y ≤ x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

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

Tactic:
·

Goal state after:
X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst✝ : IsIso f
⊢ B ≤ (B.preimage f).image f
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
A B : X.Subcomplex
h : ∀ (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

pp: case refine_2
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⦌)
⊢ ↑x ∈ B.obj (Opposite.op ⦋n⦌)

Tactic:
·

Goal state after:
case refine_1
X : SSet
A B : X.Subcomplex
h : ∀ (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.Finite

Goal state before:
pp: case pos
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
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x

pp: case neg
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
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x

Tactic:
·

Goal state after:
case pos
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
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: case neg
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
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x

Tactic:
·

Goal state after:
case neg
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
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨i, x⟩ => N.mk ↑x ⋯)
        a =
      x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

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

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

Tactic:
·

Goal state after:
case pos
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : (Finset.image φ ⊤).Nonempty
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d
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 φ ⊤).Nonempty
⊢ ∃ 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 φ ⊤).Nonempty
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_2
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⦌)
⊢ ↑x ∈ B.obj (Opposite.op ⦋n⦌)

Tactic:
·

Goal state after:
case refine_2
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⦌)
⊢ ↑x ∈ B.obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

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

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

Goal state after:
case mp
X : SSet
x y : X.op.N
⊢ (∃ f,
      (ConcreteCategory.hom (X.map f.op)) (mk (opObjEquiv y.simplex) ⋯).simplex =
        (mk (opObjEquiv x.simplex) ⋯).simplex) →
    ∃ f, (ConcreteCategory.hom (X.op.map f.op)) y.simplex = x.simplex
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:
·

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

pp: case neg
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₁) ((SimplexCategory.Hom.toOrderHom hf.section_) y) = y

Tactic:
·

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

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

Goal state before:
pp: case neg
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₁) ((SimplexCategory.Hom.toOrderHom hf.section_) y) = y

Tactic:
·

Goal state after:
case neg
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₁) ((SimplexCategory.Hom.toOrderHom hf.section_) y) = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: case mk
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
⊢ Finite (X _⦋n⦌)

Tactic:
have hφ : Function.Surjective φ := fun x ↦ by
    obtain ⟨m, f, hf, y, rfl⟩ := X.exists_nonDegenerate x
    have := SimplexCategory.le_of_epi f
    exact ⟨⟨⟨m, by lia⟩, f, y⟩, rfl⟩

Goal state after:
case mk
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
hφ : Function.Surjective φ
⊢ Finite (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy

pp: X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

Tactic:
·

Goal state after:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

Tactic:
·

Goal state after:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y
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)
⊢ (N.mk ↑y ⋯).subcomplex ≤ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex

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

Tactic:
·

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