mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ P.p ≫ (-f.f) ≫ Q.p = -f.f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ P.p ≫ f.f ≫ Q.p = f.f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ f ≫ g.f = f ≫ h.f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ f ≫ g.f = f ≫ h.f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g.f ≫ f = h.f ≫ f

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g.f ≫ f = h.f ≫ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌

Tactic:
by
  rcases i with ⟨i, hi⟩
  ext ⟨j, hj⟩
  dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
  simp only [Fin.lt_def, Fin.dite_val, Fin.ite_val, Fin.val_pred]
  split_ifs
  any_goals simp
  all_goals lia

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g.unop.op ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map (⦋0⦌.const (unop j) 0 ≫ g.unop).op ≫ f = X.map (⦋0⦌.const (unop i) 0).op ≫ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Mono f
⊢ x.len ≤ y.len

Tactic:
simpa using

Goal state after:
x y : SimplexCategory
f : x ⟶ y
inst✝ : Mono f
⊢ x.len ≤ y.len
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ y.len ≤ x.len

Tactic:
simpa using

Goal state after:
x y : SimplexCategory
f : x ⟶ y
inst✝ : Epi f
⊢ y.len ≤ x.len
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n : ℕ
⊢ (H.h 0 ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.δ 0 = (g ≫ p).app (op ⦋n⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n : ℕ
⊢ H.h 0 ≫ p.app (op ⦋n + 1⦌) ≫ Y'.δ 0 = g.app (op ⦋n⦌) ≫ p.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n : ℕ
⊢ (H.h (Fin.last n) ≫ p.app (op ⦋n + 1⦌)) ≫ Y'.δ (Fin.last (n + 1)) = (f ≫ p).app (op ⦋n⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n : ℕ
⊢ H.h (Fin.last n) ≫ p.app (op ⦋n + 1⦌) ≫ Y'.δ (Fin.last (n + 1)) = f.app (op ⦋n⦌) ≫ p.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hij : i ≤ j.castSucc
⊢ (H.h j.succ ≫ p.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y'.δ i.castSucc = X.δ i ≫ H.h j ≫ p.app (op ⦋n✝ + 1⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hij : i ≤ j.castSucc
⊢ H.h j.succ ≫ p.app (op ⦋n✝ + 1 + 1⦌) ≫ Y'.δ i.castSucc = X.δ i ≫ H.h j ≫ p.app (op ⦋n✝ + 1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ (H.h j.succ ≫ p.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y'.δ j.castSucc.succ =
    (H.h j.castSucc ≫ p.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y'.δ j.castSucc.succ

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ H.h j.succ ≫ p.app (op ⦋n✝ + 1 + 1⦌) ≫ Y'.δ j.castSucc.succ =
    H.h j.castSucc ≫ p.app (op ⦋n✝ + 1 + 1⦌) ≫ Y'.δ j.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hji : j.castSucc < i
⊢ (H.h j.castSucc ≫ p.app (op ⦋n✝ + 1 + 1⦌)) ≫ Y'.δ i.succ = X.δ i ≫ H.h j ≫ p.app (op ⦋n✝ + 1⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hji : j.castSucc < i
⊢ H.h j.castSucc ≫ p.app (op ⦋n✝ + 1 + 1⦌) ≫ Y'.δ i.succ = X.δ i ≫ H.h j ≫ p.app (op ⦋n✝ + 1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ (H.h j ≫ p.app (op ⦋n✝ + 1⦌)) ≫ Y'.σ i.castSucc = X.σ i ≫ H.h j.succ ≫ p.app (op ⦋n✝ + 1 + 1⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ H.h j ≫ p.app (op ⦋n✝ + 1⦌) ≫ Y'.σ i.castSucc = X.σ i ≫ H.h j.succ ≫ p.app (op ⦋n✝ + 1 + 1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i j : Fin (n✝ + 1)
hji : j ≤ i
⊢ (H.h j ≫ p.app (op ⦋n✝ + 1⦌)) ≫ Y'.σ i.succ = X.σ i ≫ H.h j.castSucc ≫ p.app (op ⦋n✝ + 1 + 1⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
Y' : SimplicialObject C
p : Y ⟶ Y'
n✝ : ℕ
i j : Fin (n✝ + 1)
hji : j ≤ i
⊢ H.h j ≫ p.app (op ⦋n✝ + 1⦌) ≫ Y'.σ i.succ = X.σ i ≫ H.h j.castSucc ≫ p.app (op ⦋n✝ + 1 + 1⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n : ℕ
⊢ (p.app (op ⦋n⦌) ≫ H.h 0) ≫ Y.δ 0 = (p ≫ g).app (op ⦋n⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n : ℕ
⊢ p.app (op ⦋n⦌) ≫ H.h 0 ≫ Y.δ 0 = p.app (op ⦋n⦌) ≫ g.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n : ℕ
⊢ (p.app (op ⦋n⦌) ≫ H.h (Fin.last n)) ≫ Y.δ (Fin.last (n + 1)) = (p ≫ f).app (op ⦋n⦌)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n : ℕ
⊢ p.app (op ⦋n⦌) ≫ H.h (Fin.last n) ≫ Y.δ (Fin.last (n + 1)) = p.app (op ⦋n⦌) ≫ f.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hij : i ≤ j.castSucc
⊢ (p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ) ≫ Y.δ i.castSucc = X'.δ i ≫ p.app (op ⦋n✝⦌) ≫ H.h j

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hij : i ≤ j.castSucc
⊢ p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ ≫ Y.δ i.castSucc = p.app (op ⦋n✝ + 1⦌) ≫ X.δ i ≫ H.h j
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ (p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ) ≫ Y.δ j.castSucc.succ =
    (p.app (op ⦋n✝ + 1⦌) ≫ H.h j.castSucc) ≫ Y.δ j.castSucc.succ

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ ≫ Y.δ j.castSucc.succ = p.app (op ⦋n✝ + 1⦌) ≫ H.h j.castSucc ≫ Y.δ j.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hji : j.castSucc < i
⊢ (p.app (op ⦋n✝ + 1⦌) ≫ H.h j.castSucc) ≫ Y.δ i.succ = X'.δ i ≫ p.app (op ⦋n✝⦌) ≫ H.h j

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hji : j.castSucc < i
⊢ p.app (op ⦋n✝ + 1⦌) ≫ H.h j.castSucc ≫ Y.δ i.succ = p.app (op ⦋n✝ + 1⦌) ≫ X.δ i ≫ H.h j
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ (p.app (op ⦋n✝⦌) ≫ H.h j) ≫ Y.σ i.castSucc = X'.σ i ≫ p.app (op ⦋n✝ + 1⦌) ≫ H.h j.succ

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ p.app (op ⦋n✝⦌) ≫ H.h j ≫ Y.σ i.castSucc = p.app (op ⦋n✝⦌) ≫ X.σ i ≫ H.h j.succ
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)
hj : j ≠ i
⊢ i.succAbove (((Fin.last n).predAbove i).predAbove j) = j

Tactic:
cases i using Fin.lastCases

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

case h.cast
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
x : Fin (Δ.len + 1)
j : Fin (n + 2)
i✝ : Fin (n + 1)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i✝.castSucc
hj : j ≠ i✝.castSucc
⊢ i✝.castSucc.succAbove (((Fin.last n).predAbove i✝.castSucc).predAbove j) = j
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i j : Fin (n✝ + 1)
hji : j ≤ i
⊢ (p.app (op ⦋n✝⦌) ≫ H.h j) ≫ Y.σ i.succ = X'.σ i ≫ p.app (op ⦋n✝ + 1⦌) ≫ H.h j.castSucc

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n✝ : ℕ
i j : Fin (n✝ + 1)
hji : j ≤ i
⊢ p.app (op ⦋n✝⦌) ≫ H.h j ≫ Y.σ i.succ = p.app (op ⦋n✝⦌) ≫ X.σ i ≫ H.h j.castSucc
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
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) ((ConcreteCategory.hom (δ i)) k)) =
    ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)

Tactic:
σ₀Iter_coe_eq_of_ge j ..,

Goal state after:
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
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) ((ConcreteCategory.hom (δ i)) k)) = ↑k - j
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 : X ⟶ F.augmentedCechNerve
this :
  ((𝟭 (SimplicialObject C)).map G.left ≫ F.augmentedCechNerve.hom).app (Opposite.op ⦋0⦌) =
    (X.hom ≫ (const C).map G.right).app (Opposite.op ⦋0⦌)
⊢ (𝟭 C).map (G.left.app (Opposite.op ⦋0⦌) ≫ WidePullback.π (fun x ↦ F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right

Tactic:
simpa using

Goal state after:
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 : X ⟶ F.augmentedCechNerve
this :
  ((𝟭 (SimplicialObject C)).map G.left ≫ F.augmentedCechNerve.hom).app (Opposite.op ⦋0⦌) =
    (X.hom ≫ (const C).map G.right).app (Opposite.op ⦋0⦌)
⊢ (G.left.app (Opposite.op ⦋0⦌) ≫ WidePullback.base fun x ↦ F.hom) = X.hom.app (Opposite.op ⦋0⦌) ≫ G.right
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), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : X ⟶ F.augmentedCechNerve
x : SimplexCategoryᵒᵖ
⊢ ((equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left.app x ≫ WidePullback.base fun x ↦ F.hom) =
    A.left.app x ≫ WidePullback.base fun x ↦ F.hom

Tactic:
simpa using

Goal state after:
case h₁.refine_2
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ᵒᵖ
⊢ X.hom.app x ≫ A.right = A.left.app x ≫ WidePullback.base fun x ↦ F.hom
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:
· dsimp
        rw [colimit.ι_desc]
        exact congr_app A.w x

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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

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

Tactic:
simpa using

Goal state after:
X : SSet
x : X.op.N
⊢ x.simplex ∈ X.op.nonDegenerate x.dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

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

Tactic:
simpa using

Goal state after:
X : SSet
y : X.N
⊢ y.simplex ∈ X.nonDegenerate y.dim
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:
simpa using

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.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)
hf₁ : SplitEpi f₁
hf₁' : (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
⊢ (SimplexCategory.Hom.toOrderHom f₁) x = (SimplexCategory.Hom.toOrderHom f₂) x

Tactic:
simpa using

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₂
x : Fin (⦋n⦌.len + 1)
hf₁ : SplitEpi f₁
hf₁' : (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
⊢ (SimplexCategory.Hom.toOrderHom f₁) x = (SimplexCategory.Hom.toOrderHom f₂) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : SimplexCategoryᵒᵖ
⊢ Finite (X.obj n)

Tactic:
obtain ⟨n⟩ := n
  induction n using SimplexCategory.rec with | _ n
  let φ : (Σ (m : Fin (n + 1)) (f : ⦋n⦌ ⟶ ⦋m.1⦌),
    X.nonDegenerate m.1) → X _⦋n⦌ := fun ⟨m, f, x⟩ ↦ X.map f.op x.1
  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⟩
  exact Finite.of_surjective _ hφ

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)
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
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
⊢ y₂ ≤ y₁

Tactic:
simpa using

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₂✝
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
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
⊢ y₂ ≤ y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
x✝ : (i : ι) × (A i).toSSet.N
i : ι
s : (A i).toSSet.N
⊢ (ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex ∈
    (⨆ i, A i).toSSet.nonDegenerate s.dim

Tactic:
simpa using

Goal state after:
X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
x✝ : (i : ι) × (A i).toSSet.N
i : ι
s : (A i).toSSet.N
⊢ s.simplex ∈ (A i).toSSet.nonDegenerate s.dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X _⦋m⦌
hx : (ConcreteCategory.hom (X.map f.op)) y ∈ A.obj (op ⦋n⦌)
this : IsSplitEpi f
⊢ y ∈ A.obj (op ⦋m⦌)

Tactic:
simpa using

Goal state after:
case mpr
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X _⦋m⦌
hx : (ConcreteCategory.hom (X.map f.op)) y ∈ A.obj (op ⦋n⦌)
this : IsSplitEpi f
⊢ y ∈ A.obj (op ⦋m⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
x : A.toSSet _⦋n⦌
⊢ x ∈ A.toSSet.degenerate n ↔ x ∈ ⊤

Tactic:
simpa using

Goal state after:
case mpr
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
x : A.toSSet _⦋n⦌
⊢ ↑x ∈ X.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
n : ℕ
⊢ ⇑(ConcreteCategory.hom (f.app (op ⦋n⦌))) '' X.degenerate n ⊆ Y.degenerate n

Tactic:
simpa using

Goal state after:
X Y : SSet
f : X ⟶ Y
n : ℕ
⊢ X.degenerate n ⊆ (fun a ↦ (ConcreteCategory.hom (f.app (op ⦋n⦌))) a) ⁻¹' Y.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
simpa using

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

Goal state before:
pp: case zero
X : Type u_1
inst✝ : PartialOrder X
s : nerve X _⦋0⦌
⊢ s ∈ (nerve X).nonDegenerate 0 ↔ StrictMono s.obj

Tactic:
simpa using

Goal state after:
case zero
X : Type u_1
inst✝ : PartialOrder X
s : nerve X _⦋0⦌
⊢ StrictMono s.obj
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
h : (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) a = (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) b
⊢ i.succAboveOrderEmb a = i.succAboveOrderEmb b

Tactic:
simpa using

Goal state after:
n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
h : (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) a = (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) b
⊢ a = b
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
⊢ (Equiv.ofBijective (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) ⋯) a ≤
      (Equiv.ofBijective (fun a ↦ ⟨i.succAboveOrderEmb a, ⋯⟩) ⋯) b ↔
    a ≤ b

Tactic:
by
    simp only [Equiv.ofBijective_apply, Subtype.mk_le_mk, OrderEmbedding.le_iff_le]

Goal state after: