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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : Augmented Cᵒᵖ
⊢ X.leftOp.rightOp.left = X.left

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i = ↑i + 0
⊢ δ₀Iter 0 h ≫ δ i = δ i ≫ δ₀Iter 0 ⋯

Tactic:
simp

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

Goal state before:
pp: j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ 0 ≤ i

Tactic:
simp

Goal state after:
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)
j' : Fin (n + 1)
hi' : n + i = m
hj' : ↑j = ↑j' + i
⊢ X.σ j ≫ X.δ₀Iter i ⋯ = X.δ₀Iter i hi' ≫ X.σ j'

Tactic:
by
  simp [σ, δ₀Iter, ← Functor.map_comp, ← op_comp,
    SimplexCategory.δ₀Iter_σ' i j j']

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

Goal state before:
pp: case zero
n : ℕ
j : Fin (n + 1)
hi' : n + 0 = n
hj' : ↑j = ↑j + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j ≫ δ₀Iter 0 hi'

Tactic:
simp

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

Goal state before:
pp: i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : ↑j.succ = ↑j' + (i + 1)
⊢ 0 ≤ j.castSucc

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ ↑0 < 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ Fin.castSucc 0

Tactic:
simp

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

Goal state before:
pp: case inr
n : ℕ
k : Fin ⦋n + 1⦌.len
⊢ ↑k.succ - 1 = ↑(Fin.predAbove 0 k.succ)

Tactic:
simp

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

Goal state before:
pp: case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
⊢ ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j

Tactic:
intro j

Goal state after:
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
j : Fin (n + 2)
⊢ j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case zero
n : ℕ
h : n + 0 = n
⊢ σ₀Iter (0 + 1) ⋯ = σ 0 ≫ σ₀Iter 0 h

Tactic:
simp

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
hk' : i ≤ k.castSucc
⊢ ↑k.succ - (j + 1) = ↑k - j

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 2)
hi' : 0 < ↑i
h : n + 0 = n
hi'' : ↑i = ↑i + 0
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i

Tactic:
simp

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

Goal state before:
pp: case neg
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
hk' : j.castSucc < k
⊢ ↑(j.predAbove k) ≤ i

Tactic:
grind [Fin.predAbove]

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

Goal state before:
pp: case zero
n : ℕ
j : Fin (n + 1)
hi : n + 0 = n
hj : ↑j = ↑j + 0
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j

Tactic:
simp

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

Goal state before:
pp: i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ 0 ≤ j'

Tactic:
simp

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
x : X.op _⦋n + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) (opObjEquiv x) =
    opObjEquiv ((ConcreteCategory.hom (SimplicialObject.δ X.op i.rev)) x)

Tactic:
simp

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 1)
x : X.op _⦋n⦌
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) (opObjEquiv x) =
    opObjEquiv ((ConcreteCategory.hom (SimplicialObject.σ X.op i.rev)) x)

Tactic:
simp

Goal state after:
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
U V : Cᵒᵖ
g : U ⟶ V
f : X ⟶ U
⊢ (ConcreteCategory.hom (F.map (f ≫ g))) x = (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map f)) x)

Tactic:
simp

Goal state after:
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
⊢ (ConcreteCategory.hom (F.map (𝟙 X))) x = x

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
hi : n + 0 = n
⊢ δ₀Iter 0 hi ≫ σ₀Iter 0 hi = 𝟙 ⦋n⦌

Tactic:
simp

Goal state after:
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
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (ConcreteCategory.hom (F'.map (𝟙 X))) ((ConcreteCategory.hom (f.app X)) x) = (ConcreteCategory.hom (f.app X)) x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X✝ Y✝ : SimplexCategoryᵒᵖ
g : X✝ ⟶ Y✝
⊢ ∀ (j : Fin ((Opposite.unop Y✝).len + 1)),
    WidePullback.π (fun x ↦ f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) j) ≫ f.hom = WidePullback.base fun x ↦ f.hom

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePullback f✝.right (fun x ↦ f✝.left) fun x ↦ f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
inst✝ : ∀ (n : ℕ), HasWidePullback g.right (fun x ↦ g.left) fun x ↦ g.hom
F : f ⟶ g
n : SimplexCategoryᵒᵖ
j : Fin ((Opposite.unop n).len + 1)
⊢ (WidePullback.π (fun x ↦ f.hom) j ≫ Hom.left F) ≫ g.hom = (WidePullback.base fun x ↦ f.hom) ≫ Hom.right F

Tactic:
simp

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
G : Augmented.toArrow.obj X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin ((Opposite.unop x).len + 1)
⊢ (X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ≫ F.hom = X.hom.app x ≫ Arrow.Hom.right G

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
simp

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ ↑((ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x) ∈ Set.univ ↔ x ∈ ⊤

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

Goal state after:
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), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
j : Fin ((Opposite.unop x).len + 1)
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x ≫ WidePullback.π (fun x ↦ F.hom) j =
    A.left.app x ≫ WidePullback.π (fun x ↦ F.hom) j

Tactic:
simp

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), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : X ⟶ F.augmentedCechNerve
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).right = A.right

Tactic:
simp

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
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (x.len + 1)
t : X.hom.app x = X.hom.app ⦋0⦌ ≫ X.right.map (⦋0⦌.const x j)
⊢ Arrow.Hom.left G ≫ X.hom.app ⦋0⦌ ≫ X.right.map (⦋0⦌.const x j) = Arrow.Hom.left G ≫ X.hom.app x

Tactic:
rw [← t]

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

Goal state before:
pp: X : SSet
n : ℕ
x y : X _⦋n⦌
⊢ { dim := n, simplex := x } = { dim := n, simplex := y } ↔ x = y

Tactic:
simp

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

Goal state before:
pp: case mpr
X : SSet
m : ℕ
x : X _⦋m⦌
inst✝ : Mono (𝟙 ⦋m⦌)
hf : IsIso (𝟙 ⦋m⦌)
⊢ { dim := m, simplex := (ConcreteCategory.hom (X.map (𝟙 ⦋m⦌).op)) x } = { dim := m, simplex := x }

Tactic:
simp

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : X.S
⊢ (fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.inv.app (Opposite.op ⦋s.dim⦌))) s.simplex })
      ((fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋s.dim⦌))) s.simplex }) x✝) =
    x✝

Tactic:
simp

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : Y.S
⊢ (fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋s.dim⦌))) s.simplex })
      ((fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.inv.app (Opposite.op ⦋s.dim⦌))) s.simplex }) x✝) =
    x✝

Tactic:
simp

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
⊢ x ∈ X.nonDegenerate 0

Tactic:
simp

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
⊢ x = (ConcreteCategory.hom (X.map (𝟙 ⦋0⦌).op)) ↑⟨x, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
⊢ x = (ConcreteCategory.hom (X.map (𝟙 ⦋n + 1⦌).op)) ↑⟨x, hx⟩

Tactic:
simp

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

Goal state before:
pp: case pos
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

pp: case neg
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∉ X.nonDegenerate (n + 1)
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
· exact ⟨n + 1, 𝟙 _, inferInstance, ⟨x, hx⟩, by simp⟩

Goal state after:
case neg
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∉ X.nonDegenerate (n + 1)
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : ↑(X.nonDegenerate m)
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) ((ConcreteCategory.hom (X.map f.op)) ↑z) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ i ≫ f).op)) ↑z

Tactic:
simp

Goal state after:
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : ↑(X.nonDegenerate m)
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) ((ConcreteCategory.hom (X.map f.op)) ↑z) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ i).op)) ((ConcreteCategory.hom (X.map f.op)) ↑z)
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) ≫
      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.head fun x ↦ F.hom) ≫ A.right.app x

Tactic:
colimit.ι_desc

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
⊢ (WidePushoutShape.mkCocone (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)) ⋯).ι.app
      none =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x
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:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case e'_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 ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < ⦋0⦌.len + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (⦋0⦌.const ⦋0⦌ 0)) ⟨a, ha⟩) = ↑((SimplexCategory.Hom.toOrderHom (𝟙 ⦋0⦌)) ⟨a, ha⟩)

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
simp

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

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

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

Tactic:
simp

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
j : ℕ
isLt✝ : j < (Opposite.unop n).len + 1
⊢ (WidePullback.lift (WidePullback.base fun x ↦ (Arrow.mk (terminal.from X)).hom)
          (fun i ↦
            WidePullback.π (fun x ↦ (Arrow.mk (terminal.from X)).hom) ((SimplexCategory.Hom.toOrderHom f.unop) i))
          ⋯ ≫
        (wideCospan.limitIsoPi (Fin ((Opposite.unop n).len + 1)) (Arrow.mk (terminal.from X)).left).hom) ≫
      Pi.π (fun x ↦ X) ⟨j, isLt✝⟩ =
    ((wideCospan.limitIsoPi (Fin ((Opposite.unop m).len + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
        Pi.lift fun i ↦ Pi.π (fun x ↦ X) ((SimplexCategory.Hom.toOrderHom f.unop) i)) ≫
      Pi.π (fun x ↦ X) ⟨j, isLt✝⟩

Tactic:
simp

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

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

Goal state after:
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:
simp only [le_antisymm_iff]

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 ∧ N.mk y hy ≤ N.mk x hx ↔
    Subcomplex.ofSimplex x ≤ Subcomplex.ofSimplex y ∧ Subcomplex.ofSimplex y ≤ Subcomplex.ofSimplex x
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x : X.S
⊢ x.toN.subcomplex = x.subcomplex

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 (f.app (op ⦋n⦌))) ((ConcreteCategory.hom (X.map g.op)) y) ∈ Y.degenerate n

Tactic:
exact ⟨m, hm, g, f.app _ y, by rw [NatTrans.naturality_apply]⟩

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

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom
        (X.map
          (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
              δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op))
      e.edge =
    (id x).edge

Tactic:
simp

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (𝟙 { obj := ⦋1⦌, property := ⋯ }).op)) e.edge = e.edge

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a : Fin (n + 1)
⊢ i.succAboveOrderEmb a ∈ {i}ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
hj✝ : j ∈ {0}ᶜ
hj : ¬j = 0
⊢ (fun a ↦ ⟨(succAboveOrderEmb 0) a, ⋯⟩) (j.pred hj) = ⟨j, hj✝⟩

Tactic:
simp

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (𝟙 { obj := ⦋1⦌, property := δ₂_zero_comp_σ₂_one._proof_1 }).op)) e.edge = e.edge

Tactic:
simp

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom
        (X.map
          (σ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_σ₂_one._proof_4 ≫
              δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3).op))
      e.edge =
    (id y).edge

Tactic:
simp

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

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (𝟙 { obj := ⦋0 + 1⦌, property := ⋯ }).op)) e.edge = e.edge

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
⊢ a ∈ {a, b}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b : α
hab : a < b
⊢ b ∈ {a, b}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ a ∈ {a, b, c}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ b ∈ {a, b, c}

Tactic:
simp

Goal state after: