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

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

Tactic:
by

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

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

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

Tactic:
by

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)
⊢ n + i = m

Tactic:
by

Goal state after:
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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n : ℕ
⊢ F.map (H.h 0) ≫ (((whiskering C D).obj F).obj Y).δ 0 = (((whiskering C D).obj F).map g).app (op ⦋n⦌)

Tactic:
by

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)
⊢ ↑j = ↑j' + i

Tactic:
by

Goal state after:
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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n : ℕ
⊢ F.map (H.h (Fin.last n)) ≫ (((whiskering C D).obj F).obj Y).δ (Fin.last (n + 1)) =
    (((whiskering C D).obj F).map f).app (op ⦋n⦌)

Tactic:
by

Goal state after:
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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hij : i ≤ j.castSucc
⊢ F.map (H.h j.succ) ≫ (((whiskering C D).obj F).obj Y).δ i.castSucc =
    (((whiskering C D).obj F).obj X).δ i ≫ F.map (H.h j)

Tactic:
by

Goal state after:
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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
j : Fin (n✝ + 1)
⊢ F.map (H.h j.succ) ≫ (((whiskering C D).obj F).obj Y).δ j.castSucc.succ =
    F.map (H.h j.castSucc) ≫ (((whiskering C D).obj F).obj Y).δ j.castSucc.succ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
hi : n + i = m
j : Fin (⦋m⦌.len + 1)
⊢ ↑j - i < ⦋n⦌.len + 1

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
hi : n + i = m
x✝² x✝¹ : Fin (⦋m⦌.len + 1)
x✝ : x✝² ≤ x✝¹
⊢ (fun j ↦ if ↑j < i then 0 else ⟨↑j - i, ⋯⟩) x✝² ≤ (fun j ↦ if ↑j < i then 0 else ⟨↑j - i, ⋯⟩) x✝¹

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

Tactic:
by

Goal state after:
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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
i : Fin (n✝ + 2)
j : Fin (n✝ + 1)
hji : j.castSucc < i
⊢ F.map (H.h j.castSucc) ≫ (((whiskering C D).obj F).obj Y).δ i.succ =
    (((whiskering C D).obj F).obj X).δ i ≫ F.map (H.h j)

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : i ≤ ↑j
⊢ ¬↑j < i

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : i ≤ ↑j
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = ↑j - i

Tactic:
by

Goal state after:
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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
i j : Fin (n✝ + 1)
hij : i ≤ j
⊢ F.map (H.h j) ≫ (((whiskering C D).obj F).obj Y).σ i.castSucc =
    (((whiskering C D).obj F).obj X).σ i ≫ F.map (H.h j.succ)

Tactic:
by

Goal state after:
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
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
n✝ : ℕ
i j : Fin (n✝ + 1)
hji : j ≤ i
⊢ F.map (H.h j) ≫ (((whiskering C D).obj F).obj Y).σ i.succ =
    (((whiskering C D).obj F).obj X).σ i ≫ F.map (H.h j.castSucc)

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i hi)) j) = 0

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
⊢ ∃ θ', θ = σ i ≫ θ'

Tactic:
by

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

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

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

Goal state before:
pp: n : ℕ
⊢ σ₀Iter 1 ⋯ = σ 0

Tactic:
by

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

Goal state after:
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:
by
    simpa using H.h_castSucc_comp_δ_succ_of_lt i j hji =≫ p.app _

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Tactic:
by

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

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

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

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

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

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = σ i ≫ θ'

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n m : ℕ
h : n + 0 = m
⊢ n = m

Tactic:
by

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

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

Goal state before:
pp: i : ℕ
hi' : ∀ {n m : ℕ} (h : n + i = m), σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h
n m : ℕ
h : n + (i + 1) = m
⊢ n + 1 + i = m

Tactic:
by

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

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

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

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
⊢ ∃ θ', θ = θ' ≫ δ i

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ rev.map (δ i) = δ i.rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ rev.map (σ i) = σ i.rev

Tactic:
by

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ rev.map (rev.map f) = f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = θ' ≫ δ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ¬Function.Injective ⇑(Hom.toOrderHom θ)

Tactic:
by

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

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi (σ i ≫ θ')

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X Y : SimplicialObject C
f : X ⟶ Y
n : SimplexCategoryᵒᵖ
⊢ (opFunctor.map f).app n = opObjIso.hom ≫ f.app n ≫ opObjIso.inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n m : SimplexCategoryᵒᵖ
f : n ⟶ m
⊢ (opFunctor.obj X).map f = opObjIso.hom ≫ X.map (SimplexCategory.rev.map f.unop).op ≫ opObjIso.inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ (opFunctor.obj X).δ i = opObjIso.hom ≫ X.δ i.rev ≫ opObjIso.inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ (opFunctor.obj X).σ i = opObjIso.hom ≫ X.σ i.rev ≫ opObjIso.inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : SimplexCategoryᵒᵖ
⊢ (opFunctorCompOpFunctorIso.hom.app X).app n = opObjIso.hom ≫ opObjIso.hom

Tactic:
by

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

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
⊢ ∃ i, θ = σ i

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : SimplexCategoryᵒᵖ
⊢ (opFunctorCompOpFunctorIso.inv.app X).app n = opObjIso.inv ≫ opObjIso.inv

Tactic:
by

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

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ¬Function.Surjective ⇑(Hom.toOrderHom θ)

Tactic:
by

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

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
⊢ Mono (θ' ≫ δ i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ∃ i, θ = δ i

Tactic:
by

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

Goal state before:
pp: Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi' : Δ ≠ Δ'
⊢ Δ'.len < Δ.len

Tactic:
by

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

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

Tactic:
by

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)
hk : j ≤ ↑k
hk' : k.castSucc < i
⊢ j = ↑k

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ factorThruImage φ = e

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Function.Injective δ

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Function.Injective σ

Tactic:
by

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)
hk : ↑k < j
hk' : k.castSucc < i
⊢ k.castSucc < i

Tactic:
by

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
⊢ δ i ≫ σ₀Iter (j + 1) h = σ₀Iter j ⋯

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + 0 = n
hi' : 0 < ↑i
hi'' : ↑i = ↑i' + 0
⊢ n = m

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
hi' : 0 < ↑i
i' : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i = ↑i' + 0
⊢ i = i'

Tactic:
by

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 : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ m + 1 + j = n

Tactic:
by

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 : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ j < ↑i

Tactic:
by

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 : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ ↑i = ↑i'.succ + j

Tactic:
by

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 : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ Fin.castSucc 0 < i'

Tactic:
by

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

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

Tactic:
by

Goal state after:
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)
hk : i < ↑k
⊢ j.castSucc < k

Tactic:
by

Goal state after:
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)
hk : ↑k ≤ i
hk' : k ≤ j.castSucc
⊢ k ≤ j.castSucc

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter (i + 1) ⋯

Tactic:
by

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

Goal state before:
pp: n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + 0 = m
hj : ↑j = ↑j' + 0
⊢ n = m

Tactic:
by

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

Goal state before:
pp: n : ℕ
j' j : Fin (n + 1)
hi : n + 0 = n
hj : ↑j = ↑j' + 0
⊢ j = j'

Tactic:
by

Goal state after: