Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case e'_2.e'_6.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 2) a) = a

pp: case e'_2.e'_7.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1) j) = j

pp: case e'_3.e'_6.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1 + 1) (j + 1)) = j + 1

pp: case e'_3.e'_7.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1) a) = a

Tactic:
<;>

Goal state after:
case e'_2.e'_6.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 2) a) = a

case e'_2.e'_7.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1) j) = j

case e'_3.e'_6.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1 + 1) (j + 1)) = j + 1

case e'_3.e'_7.e'_2
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ ↑(Fin.ofNat (m + 1) a) = a