mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.σ j ≫ X.δ₀Iter (i + 1) hi = X.δ₀Iter i ⋯

Tactic:
by
  dsimp [σ, δ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_σ ..]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (δ₀Iter (i + 1) hi ≫ σ j)) k = (ConcreteCategory.hom (δ₀Iter i ⋯)) k

Tactic:
ext

Goal state after:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter (i + 1) hi ≫ σ j)) k) = ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
⊢ σ₀Iter 0 ⋯ = 𝟙 ⦋n⦌

Tactic:
ext

Goal state after:
n : ℕ
x✝ : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (σ₀Iter 0 ⋯)) x✝) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) x✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
k : Fin (⦋n + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (σ₀Iter 1 ⋯)) k = (ConcreteCategory.hom (σ 0)) k

Tactic:
ext

Goal state after:
n : ℕ
k : Fin (⦋n + 1⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ₀Iter 1 ⋯)) k) = ↑((ConcreteCategory.hom (σ 0)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
⊢ (ConcreteCategory.hom (σ₀Iter (i + 1) h)) k = (ConcreteCategory.hom (σ₀Iter i ⋯ ≫ σ 0)) k

Tactic:
ext

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ₀Iter (i + 1) h)) k) = ↑((ConcreteCategory.hom (σ₀Iter i ⋯ ≫ σ 0)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
i j : Fin (n.len + 1)
hij : i ≤ j
⊢ (fun i ↦ Fin.rev ((ConcreteCategory.hom f) i.rev)) i ≤ (fun i ↦ Fin.rev ((ConcreteCategory.hom f) i.rev)) j

Tactic:
rw [Fin.rev_le_rev]
    exact f.toOrderHom.monotone (by rwa [Fin.rev_le_rev])

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (δ i ≫ σ₀Iter (j + 1) h)) k = (ConcreteCategory.hom (σ₀Iter j ⋯)) k

Tactic:
ext

Goal state after:
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ i ≫ σ₀Iter (j + 1) h)) k) = ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ image φ = Δ'

Tactic:
ext

Goal state after:
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := ⋯
⊢ (image φ).len = Δ'.len
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
⊢ (ConcreteCategory.hom (σ j ≫ σ₀Iter i hi)) k = (ConcreteCategory.hom (σ₀Iter (i + 1) ⋯)) k

Tactic:
ext

Goal state after:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ j ≫ σ₀Iter i hi)) k) = ↑((ConcreteCategory.hom (σ₀Iter (i + 1) ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic

Goal state before:
pp: X Y : SSet
y : Y _⦋0⦌
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.map x✝ ≫ ↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝¹).const ⦋0⦌ 0).op)) y) =
    (↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y) ≫ Y.map x✝

Tactic:
ext

Goal state after:
X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom
          (X.map x✝¹ ≫ ↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝³).const ⦋0⦌ 0).op)) y) ≫ Y.map x✝¹)).toFun
      x✝
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
⊢ ofSection x ≤ G ↔ x ∈ G.obj X

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
⊢ ofSection x ≤ G → x ∈ G.obj X

case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
⊢ x ∈ G.obj X → ofSection x ≤ G
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, (ConcreteCategory.hom (F.map f)) x = y) ↔ ∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, (ConcreteCategory.hom (F.map f)) x = y) → ∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y

case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y) → ∃ f, (ConcreteCategory.hom (F.map f)) x = y
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ ∃ x_1, (ConcreteCategory.hom (F.map x_1.op)) x = y

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U → ∃ x_1, (ConcreteCategory.hom (F.map x_1.op)) x = y

case mpr
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ x_1, (ConcreteCategory.hom (F.map x_1.op)) x = y) → y ∈ (ofSection x).obj U
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ X.left.map f ≫
      WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
        (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯ =
    WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
        (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
      WidePullback.lift (WidePullback.base fun x ↦ F.hom)
        (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯

Tactic:
ext

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin ((Opposite.unop y).len + 1)
⊢ (X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯) ≫
      WidePullback.π (fun x ↦ F.hom) j✝ =
    (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
        WidePullback.lift (WidePullback.base fun x ↦ F.hom)
          (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯) ≫
      WidePullback.π (fun x ↦ F.hom) j✝

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ ((X.left.map f ≫
        WidePullback.lift (X.hom.app y ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop y) i).op ≫ Arrow.Hom.left G) ⋯) ≫
      WidePullback.base fun x ↦ F.hom) =
    (WidePullback.lift (X.hom.app x ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ⋯ ≫
        WidePullback.lift (WidePullback.base fun x ↦ F.hom)
          (fun i ↦ WidePullback.π (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ⋯) ≫
      WidePullback.base fun x ↦ F.hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ n < d

Tactic:
by
  by_contra!
  obtain ⟨x, hx⟩ := x
  simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d n this] at hx

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F A) = A

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ Arrow.Hom.left (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.left A

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ Arrow.Hom.right (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)) = Arrow.Hom.right A
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
constructor

Goal state after:
case mp
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n → ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) → x ∈ X.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
constructor

Goal state after:
case mp
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) →
    ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))

case mpr
X : SSet
n : ℕ
x : X.op _⦋n⦌
m : ℕ
x✝ : m < n
⊢ (∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))) →
    ∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n + 1⦌
⊢ x ∈ X.degenerate (n + 1) ↔ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

Tactic:
constructor

Goal state after:
case mp
X : SSet
n : ℕ
x : X _⦋n + 1⦌
⊢ x ∈ X.degenerate (n + 1) → x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

case mpr
X : SSet
n : ℕ
x : X _⦋n + 1⦌
⊢ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i)) → x ∈ X.degenerate (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst✝ : Mono f
⊢ { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } = { dim := n, simplex := x } ↔ IsIso f

Tactic:
constructor

Goal state after:
case mp
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst✝ : Mono f
⊢ { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } = { dim := n, simplex := x } → IsIso f

case mpr
X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst✝ : Mono f
⊢ IsIso f → { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } = { dim := n, simplex := x }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
x y : X.S
⊢ (∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) ↔ Nonempty (equivElements y ⟶ equivElements x)

Tactic:
constructor

Goal state after:
case mp
X : SSet
x y : X.S
⊢ (∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) → Nonempty (equivElements y ⟶ equivElements x)

case mpr
X : SSet
x y : X.S
⊢ Nonempty (equivElements y ⟶ equivElements x) → ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
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
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ WidePushout.desc (WidePushout.head fun x ↦ F.hom)
        (fun i ↦ WidePushout.ι (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f) i)) ⋯ ≫
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ =
    WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
      X.right.map f

Tactic:
ext

Goal state after:
case a
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
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j✝ ≫
      WidePushout.desc (WidePushout.head fun x ↦ F.hom)
          (fun i ↦ WidePushout.ι (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f) i)) ⋯ ≫
        WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ =
    WidePushout.ι (fun x ↦ F.hom) j✝ ≫
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
        X.right.map f

case a
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
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ (WidePushout.head fun x ↦ F.hom) ≫
      WidePushout.desc (WidePushout.head fun x ↦ F.hom)
          (fun i ↦ WidePushout.ι (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f) i)) ⋯ ≫
        WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ =
    (WidePushout.head fun x ↦ F.hom) ≫
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
        X.right.map f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

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

Tactic:
constructor

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✝))

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 ≫
      WidePushout.desc (A.left ≫ X.hom.app x)
        (fun i ↦ (WidePushout.ι (fun x ↦ F.hom) 0 ≫ A.right.app ⦋0⦌) ≫ X.right.map (⦋0⦌.const x i)) ⋯ =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x

Tactic:
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]

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) ((SimplexCategory.Hom.toOrderHom (⦋0⦌.const x j)) 0) ≫ A.right.app x =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x
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
A : F ⟶ Augmented.toArrow.obj X
⊢ equivalenceLeftToRight F X (equivalenceRightToLeft F X A) = A

Tactic:
ext

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

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.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₂
hf₁ : SplitEpi f₁
⊢ y₁ = y₂

Tactic:
ext

Goal state after:
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₂
hf₁ : SplitEpi f₁
⊢ ↑y₁ = ↑y₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: 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

Tactic:
constructor

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

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.SimplexCategory.Truncated

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this : 0 < n
⊢ (inclusion n).Initial

Tactic:
constructor

Goal state after:
n : ℕ
inst✝ : NeZero n
this : 0 < n
⊢ ∀ (d : SimplexCategory), IsConnected (CostructuredArrow (inclusion n) d)
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:
constructor

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

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

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

Tactic:
constructor

Goal state after:
case mp
X : SSet
A B : X.Subcomplex
⊢ A ≤ B → ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)

case mpr
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)) → A ≤ B
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
⊢ A.toSSet.degenerate n = ⊤ ↔ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

Tactic:
constructor

Goal state after:
case mp
X : SSet
A : X.Subcomplex
n : ℕ
⊢ A.toSSet.degenerate n = ⊤ → X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

case mpr
X : SSet
A : X.Subcomplex
n : ℕ
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌) → A.toSSet.degenerate n = ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
constructor

Goal state after:
case mp
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n → x ∈ X.degenerate n

case mpr
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n → (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f : X ⟶ Y
⊢ (id x).map f = id ((ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) x)

Tactic:
ext

Goal state after:
X Y : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f : X ⟶ Y
⊢ ((id x).map f).edge = (id ((ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) x)).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f g : Edge x y
⊢ f = g

Tactic:
ext

Goal state after:
X Y : Truncated 2
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f g : Edge x y
⊢ f.edge = g.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) ↔ s.obj i.castSucc = s.obj i.succ

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) → s.obj i.castSucc = s.obj i.succ

case mpr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s.obj i.castSucc = s.obj i.succ → s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).degenerate (n + 1) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ

Tactic:
SSet.degenerate_eq_iUnion_range_σ,

Goal state after:
case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) ↔
    ¬∀ (i : Fin (Opposite.unop (Opposite.op ⦋n + 1⦌)).len), s.obj i.castSucc < s.obj i.succ