awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
id : ∀ {n : ℕ}, ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), 𝟙 (mk n) = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ y) (_ : P_σ e) (_ : P_δ m), f = e ≫ m
have comp_δ : ∀ {n n' : ℕ} (f : mk n ⟶ mk n') (j : Fin (n' + 2))
  (h : ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e) (_ : P_δ m), f = e ≫ m),
  ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ δ j = e ≫ m
Tactic: induction f with
  | @id n => use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id_mem _, P_δ.id_mem _; simp
  | @comp_δ n n' f j h =>
    obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
    exact ⟨z, e, m ≫ δ j, he, P_δ.comp_mem _ _ hm (P_δ.δ _), by simp⟩
  | @comp_σ n n' f j h =>
    obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
    cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
id : ∀ {n : ℕ}, ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n) (_ : P_σ e) (_ : P_δ m), 𝟙 (mk n) = e ≫ m
comp_δ :
  ∀ {n n' : ℕ} (f : mk n ⟶ mk n') (j : Fin (n' + 2))
    (h : ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e) (_ : P_δ m), f = e ≫ m),
    ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ δ j = e ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ y) (_ : P_σ e) (_ : P_δ m), f = e ≫ m
have comp_σ : ∀ {n n' : ℕ} (f : mk n ⟶ mk (n' + 1)) (j : Fin (n' + 1))
  (h : ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (_ : P_σ e) (_ : P_δ m), f = e ≫ m),
  ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e) (_ : P_δ m), f ≫ σ j = e ≫ m
Tactic: induction f with
  | @id n => use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id_mem _, P_δ.id_mem _; simp
  | @comp_δ n n' f j h =>
    obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
    exact ⟨z, e, m ≫ δ j, he, P_δ.comp_mem _ _ hm (P_δ.δ _), by simp⟩
  | @comp_σ n n' f j h =>
    obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h
    cases hm with
    | of g hg =>
      rcases hg with ⟨i⟩
      obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i
      exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
    | @id n =>
      exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      cases n' with
      | zero =>
        cases hg
        exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
      | succ n =>
        rcases hg with ⟨i⟩
        obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i
        · exact ⟨_, _, _, he, hf, by simp [h']⟩
        · obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf
          exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono (goal)
Goal:
X Y : SimplexCategoryGenRel
f : X ⟶ Y
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)
have obtain : ∀ (z : SimplexCategoryGenRel) (e : X ⟶ z) (m : z ⟶ Y) (he : P_σ e) (hm : P_δ m) (fac : f = e ≫ m),
  Nonempty (P_σ.MapFactorizationData P_δ f)
Tactic: obtain ⟨z, e, m, he, hm, fac⟩ := exists_P_σ_P_δ_factorization f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m a : ℕ
L : List ℕ
⊢ IsAdmissible m (a :: L) ↔
    a ≤ m ∧
      (∀ (x : 0 < L.length), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L 0 x) ∧
        IsAdmissible (m + 1) L
have nil : IsAdmissible m [a] ↔
  a ≤ m ∧
    (∀ (x : 0 < List.length (α := ℕ) []), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] 0 x) ∧
      IsAdmissible (m + 1) []
Tactic: cases L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m a : ℕ
L : List ℕ
nil :
  IsAdmissible m [a] ↔
    a ≤ m ∧
      (∀ (x : 0 < List.length (α := ℕ) []), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] 0 x) ∧
        IsAdmissible (m + 1) []
⊢ IsAdmissible m (a :: L) ↔
    a ≤ m ∧
      (∀ (x : 0 < L.length), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L 0 x) ∧
        IsAdmissible (m + 1) L
have cons : ∀ (head : ℕ) (tail : List ℕ),
  IsAdmissible m (a :: head :: tail) ↔
    a ≤ m ∧
      (∀ (x : 0 < (head :: tail).length),
          a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 x) ∧
        IsAdmissible (m + 1) (head :: tail)
Tactic: cases L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : ℕ
xs : List ℕ
h :
  ∀ {m : ℕ},
    IsAdmissible m xs ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) xs ∧
        ∀ (k : ℕ) (h : k < xs.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) xs k h ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs) ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) ∧
        ∀ (k : ℕ) (h : k < (y :: xs).length),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + k
m : ℕ
⊢ IsAdmissible m (x :: y :: xs) ↔
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (x :: y :: xs) ∧
      ∀ (k : ℕ) (h : k < (x :: y :: xs).length),
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k
have cons_cons : x < y →
  List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) →
    ((x ≤ m ∧
        ∀ (k : ℕ) (h : k < xs.length + 1),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + 1 + k) ↔
      ∀ (k : ℕ) (h : k < xs.length + 1 + 1),
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k)
Tactic: simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
⊢ IsAdmissible m L ↔
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
have nil : ∀ {m : ℕ},
  IsAdmissible m [] ↔
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) [] ∧
      ∀ (k : ℕ) (h : k < List.length (α := ℕ) []),
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k h ≤ m + k
Tactic: induction L using List.twoStepInduction generalizing m with
  | nil => grind
  | singleton _ => simp
  | cons_cons _ _ _ _ IH =>
    simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
    exact fun _ _ => ⟨fun h => by grind,
      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩
Cleared hypotheses: m, L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
nil :
  ∀ {m : ℕ},
    IsAdmissible m [] ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) [] ∧
        ∀ (k : ℕ) (h : k < List.length (α := ℕ) []),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k h ≤ m + k
⊢ IsAdmissible m L ↔
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
have singleton : ∀ (x : ℕ) {m : ℕ},
  IsAdmissible m [x] ↔
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) [x] ∧
      ∀ (k : ℕ) (h : k < [x].length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [x] k h ≤ m + k
Tactic: induction L using List.twoStepInduction generalizing m with
  | nil => grind
  | singleton _ => simp
  | cons_cons _ _ _ _ IH =>
    simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
    exact fun _ _ => ⟨fun h => by grind,
      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩
Cleared hypotheses: m, L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
nil :
  ∀ {m : ℕ},
    IsAdmissible m [] ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) [] ∧
        ∀ (k : ℕ) (h : k < List.length (α := ℕ) []),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k h ≤ m + k
singleton :
  ∀ (x : ℕ) {m : ℕ},
    IsAdmissible m [x] ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) [x] ∧
        ∀ (k : ℕ) (h : k < [x].length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [x] k h ≤ m + k
⊢ IsAdmissible m L ↔
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
have cons_cons : ∀ (x y : ℕ) (xs : List ℕ),
  (∀ {m : ℕ},
      IsAdmissible m xs ↔
        List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) xs ∧
          ∀ (k : ℕ) (h : k < xs.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) xs k h ≤ m + k) →
    ∀
      (IH :
        ∀ (y : ℕ) {m : ℕ},
          IsAdmissible m (y :: xs) ↔
            List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) ∧
              ∀ (k : ℕ) (h : k < (y :: xs).length),
                getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + k)
      {m : ℕ},
      IsAdmissible m (x :: y :: xs) ↔
        List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (x :: y :: xs) ∧
          ∀ (k : ℕ) (h : k < (x :: y :: xs).length),
            getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k
Tactic: induction L using List.twoStepInduction generalizing m with
  | nil => grind
  | singleton _ => simp
  | cons_cons _ _ _ _ IH =>
    simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
    exact fun _ _ => ⟨fun h => by grind,
      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩
Cleared hypotheses: m, L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
⊢ IsAdmissible m L ↔
    List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
have rw : (List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
    ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k) ↔
  List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
    ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
Tactic: rw [isAdmissible_iff_isChain_and_le, List.isChain_iff_pairwise]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
rw :
  (List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k) ↔
    List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
⊢ IsAdmissible m L ↔
    List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
have rw₁ : (List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
    ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k) ↔
  List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
    ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
Tactic: rw [isAdmissible_iff_isChain_and_le, List.isChain_iff_pairwise]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m a : ℕ
L : List ℕ
h : IsAdmissible m (a :: L)
⊢ IsAdmissible (m + 1) L
have nil : ∀ (h : IsAdmissible m [a]), IsAdmissible (m + 1) []
Tactic: cases L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m a : ℕ
L : List ℕ
h : IsAdmissible m (a :: L)
nil : ∀ (h : IsAdmissible m [a]), IsAdmissible (m + 1) []
⊢ IsAdmissible (m + 1) L
have cons : ∀ (head : ℕ) (tail : List ℕ) (h : IsAdmissible m (a :: head :: tail)), IsAdmissible (m + 1) (head :: tail)
Tactic: cases L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m a : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
ha : a ≤ m
ha' : ∀ (x : 0 < L.length), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L 0 x
⊢ IsAdmissible m (a :: L)
have nil : ∀ (hL : IsAdmissible (m + 1) [])
  (ha' : ∀ (x : 0 < List.length (α := ℕ) []), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] 0 x),
  IsAdmissible m [a]
Tactic: cases L
Cleared hypotheses: L, hL, ha'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m a : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
ha : a ≤ m
ha' : ∀ (x : 0 < L.length), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L 0 x
nil :
  ∀ (hL : IsAdmissible (m + 1) [])
    (ha' :
      ∀ (x : 0 < List.length (α := ℕ) []), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] 0 x),
    IsAdmissible m [a]
⊢ IsAdmissible m (a :: L)
have cons₁ : ∀ (head : ℕ) (tail : List ℕ) (hL : IsAdmissible (m + 1) (head :: tail))
  (ha' :
    ∀ (x : 0 < (head :: tail).length),
      a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 x),
  IsAdmissible m (a :: head :: tail)
Tactic: cases L
Cleared hypotheses: L, hL, ha'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
a : ℕ
L : List ℕ
⊢ (simplicialInsert a L).length = L.length + 1
have nil : ∀ (a : ℕ), (simplicialInsert a []).length = List.length (α := ℕ) [] + 1
Tactic: induction L generalizing a
Cleared hypotheses: a, L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
a : ℕ
L : List ℕ
nil : ∀ (a : ℕ), (simplicialInsert a []).length = List.length (α := ℕ) [] + 1
⊢ (simplicialInsert a L).length = L.length + 1
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ (a : ℕ), (simplicialInsert a tail).length = tail.length + 1) →
    ∀ (a : ℕ), (simplicialInsert a (head :: tail)).length = (head :: tail).length + 1
Tactic: induction L generalizing a
Cleared hypotheses: a, L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
a : ℕ
L : List ℕ
h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j L)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j (a :: L))
have cons : ∀ (h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j []))
  (hL : IsAdmissible (m + 1) [a]), IsAdmissible m (simplicialInsert j [a])
Tactic: cases L
Cleared hypotheses: L, h_rec, hL
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
a : ℕ
L : List ℕ
h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j L)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j ≤ m
cons :
  ∀ (h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j []))
    (hL : IsAdmissible (m + 1) [a]), IsAdmissible m (simplicialInsert j [a])
⊢ IsAdmissible m (simplicialInsert j (a :: L))
have cons₁ : ∀ (head : ℕ) (tail : List ℕ)
  (h_rec :
    ∀ (m : ℕ) (hL : IsAdmissible (m + 1) (head :: tail)) (j : ℕ) (hj : j ≤ m),
      IsAdmissible m (simplicialInsert j (head :: tail)))
  (hL : IsAdmissible (m + 1) (a :: head :: tail)), IsAdmissible m (simplicialInsert j (a :: head :: tail))
Tactic: cases L
Cleared hypotheses: L, h_rec, hL
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j L)
have nil : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j [])
Tactic: induction L generalizing j m with
  | nil => exact IsAdmissible.singleton hj
  | cons a L h_rec => cases L <;> grind
Cleared hypotheses: m, L, hL, j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j ≤ m
nil : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j [])
⊢ IsAdmissible m (simplicialInsert j L)
have cons : ∀ (a : ℕ) (L : List ℕ)
  (h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j L)) (m : ℕ)
  (hL : IsAdmissible (m + 1) (a :: L)) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j (a :: L))
Tactic: induction L generalizing j m with
  | nil => exact IsAdmissible.singleton hj
  | cons a L h_rec => cases L <;> grind
Cleared hypotheses: m, L, hL, j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + List.length (α := ℕ) [] = m₂
⊢ standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯
have nil : ∀ (h : m₃ + L₁.length = m₁) (h' : m₃ + List.length (α := ℕ) [] = m₃),
  standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) sorry
Tactic: obtain rfl : m₃ = m₂ := by grind
Cleared hypotheses: m₂, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₂
⊢ standardσ L₁ h ≫ standardσ t ⋯ ≫ σ (↑a : Fin (m₃ + 1)) = standardσ (t ++ L₁) ⋯ ≫ σ (↑a : Fin (m₃ + 1))
have cons : ∀ (h : m₃ + t.length + 1 + L₁.length = m₁) (h' : m₃ + (t.length + 1) = m₃ + t.length + 1),
  standardσ L₁ h ≫ standardσ t sorry ≫ σ (↑a : Fin (m₃ + 1)) = standardσ (t ++ L₁) sorry ≫ σ (↑a : Fin (m₃ + 1))
Tactic: obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind
Cleared hypotheses: m₂, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L₁ L₂ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + L₂.length = m₂
⊢ standardσ L₁ h ≫ standardσ L₂ h' = standardσ (L₂ ++ L₁) ⋯
have nil : ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + List.length (α := ℕ) [] = m₂),
  standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) sorry
Tactic: induction L₂ generalizing L₁ m₁ m₂ m₃ with
  | nil =>
    obtain rfl : m₃ = m₂ := by grind
    simp
  | cons a t H =>
    dsimp at h' ⊢
    obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind
    simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1)
      (by grind) (by grind))]
Cleared hypotheses: L₁, L₂, m₁, m₂, m₃, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L₁ L₂ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + L₂.length = m₂
nil :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + List.length (α := ℕ) [] = m₂),
    standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯
⊢ standardσ L₁ h ≫ standardσ L₂ h' = standardσ (L₂ ++ L₁) ⋯
have cons : ∀ (a : ℕ) (t : List ℕ)
  (H :
    ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
      standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) sorry)
  (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + (a :: t).length = m₂),
  standardσ L₁ h ≫ standardσ (a :: t) h' = standardσ (a :: t ++ L₁) sorry
Tactic: induction L₂ generalizing L₁ m₁ m₂ m₃ with
  | nil =>
    obtain rfl : m₃ = m₂ := by grind
    simp
  | cons a t H =>
    dsimp at h' ⊢
    obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind
    simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1)
      (by grind) (by grind))]
Cleared hypotheses: L₁, L₂, m₁, m₂, m₃, h, h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
Goal:
L : List ℕ
j head : ℕ
tail : List ℕ
tail_ih : ∀ (hj : ∀ k ∈ tail, j ≤ k), simplicialEvalσ tail j = j
hj : ∀ k ∈ head :: tail, j ≤ k
⊢ simplicialEvalσ (head :: tail) j = j
have hj₁ : j ≤ head ∧ ∀ x ∈ tail, j ≤ x
Tactic: simp only [List.forall_mem_cons] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L : List ℕ
j : ℕ
hj : ∀ k ∈ L, j ≤ k
⊢ simplicialEvalσ L j = j
have nil : ∀ (hj : ∀ (k : ℕ), Membership.mem (γ := List ℕ) [] k → j ≤ k), simplicialEvalσ [] j = j
Tactic: induction L with | nil => grind | cons _ _ _ => simp only [List.forall_mem_cons] at hj; grind
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L : List ℕ
j : ℕ
hj : ∀ k ∈ L, j ≤ k
nil : ∀ (hj : ∀ (k : ℕ), Membership.mem (γ := List ℕ) [] k → j ≤ k), simplicialEvalσ [] j = j
⊢ simplicialEvalσ L j = j
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ (hj : ∀ k ∈ tail, j ≤ k), simplicialEvalσ tail j = j) →
    ∀ (hj : ∀ k ∈ head :: tail, j ≤ k), simplicialEvalσ (head :: tail) j = j
Tactic: induction L with | nil => grind | cons _ _ _ => simp only [List.forall_mem_cons] at hj; grind
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L : List ℕ
⊢ Monotone (simplicialEvalσ L)
have nil : Monotone (simplicialEvalσ [])
Tactic: induction L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L : List ℕ
nil : Monotone (simplicialEvalσ [])
⊢ Monotone (simplicialEvalσ L)
have cons : ∀ (head : ℕ) (tail : List ℕ), Monotone (simplicialEvalσ tail) → Monotone (simplicialEvalσ (head :: tail))
Tactic: induction L
Cleared hypotheses: L