awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
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
comp_δ :
  ∀ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (he : P_σ e) (hm : P_δ m),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk (n' + 1)) (_ : P_σ e_1) (_ : P_δ m_1),
      (e ≫ m) ≫ δ j = e_1 ≫ m_1
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (_ : P_σ e) (_ : P_δ m), f ≫ δ j = e ≫ m

Tactic:
obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 2)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk n'
he : P_σ e
hm : P_δ m
⊢ (e ≫ m) ≫ δ j = e ≫ m ≫ δ j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 2)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk n'
he : P_σ e
hm : P_δ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk (n' + 1)) (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ δ j = e_1 ≫ m_1

Tactic:
exact ⟨z, e, m ≫ δ j, he, P_δ.comp_mem _ _ hm (P_δ.δ _), by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
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
comp_σ :
  ∀ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk (n' + 1)) (he : P_σ e) (hm : P_δ m),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
      (e ≫ m) ≫ σ j = e_1 ≫ m_1
⊢ ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e) (_ : P_δ m), f ≫ σ j = e ≫ m

Tactic:
obtain ⟨z, e, m, ⟨he, hm, rfl⟩⟩ := h

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hg : faces m
comp_σ :
  ∀ ⦃X Y : SimplexCategoryGenRel⦄ (i : Fin (n' + 2)) (e : mk n ⟶ mk n') (he : P_σ e),
    ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1

Tactic:
rcases hg with ⟨i⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
comp_σ :
  ∀ (w : SimplexCategoryGenRel) (w_1 : mk n' ⟶ w) (w_2 : w ⟶ mk n') (he₁ : P_σ w_1) (hm₁ : P_δ w_2)
    (h₁ : δ i ≫ σ j = w_1 ≫ w_2),
    ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m
⊢ ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
obtain ⟨_, _, _, ⟨he₁, hm₁, h₁⟩⟩ := factor_δ_σ j i

Premises used: _private.0.SimplexCategoryGenRel.factor_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
w : SimplexCategoryGenRel
w_1 : mk n' ⟶ w
w_2 : w ⟶ mk n'
he₁ : P_σ w_1
hm₁ : P_δ w_2
h₁ : δ i ≫ σ j = w_1 ≫ w_2
⊢ (e ≫ δ i) ≫ σ j = (e ≫ w_1) ≫ w_2

Tactic:
simp [← h₁]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
w : SimplexCategoryGenRel
w_1 : mk n' ⟶ w
w_2 : w ⟶ mk n'
he₁ : P_σ w_1
hm₁ : P_δ w_2
h₁ : δ i ≫ σ j = w_1 ≫ w_2
⊢ ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
        by simp [← h₁]⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
e : mk n ⟶ mk (n' + 1)
he : P_σ e
⊢ (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = (e ≫ σ j) ≫ 𝟙 (mk n')

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
e : mk n ⟶ mk (n' + 1)
he : P_σ e
⊢ ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨mk n', e ≫ σ j, 𝟙 _, P_σ.comp_mem _ _ he (P_σ.σ _), P_δ.id_mem _, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y_1 : SimplexCategoryGenRel
f : z ⟶ y_1
hf : faces.multiplicativeClosure f
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
g : y_1 ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)
hg : faces g
comp_σ :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 2)) (f : z ⟶ mk 0) (hf : faces.multiplicativeClosure f),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
cases hg
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
i : Fin (HAdd.hAdd (α := ℕ) 0 2)
f : z ⟶ mk 0
hf : faces.multiplicativeClosure f
⊢ (e ≫ f ≫ δ i) ≫ σ j = e ≫ f

Tactic:
simp [switch_δ_σ₀]

Premises used: _private.0.SimplexCategoryGenRel.switch_δ_σ₀
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
i : Fin (HAdd.hAdd (α := ℕ) 0 2)
f : z ⟶ mk 0
hf : faces.multiplicativeClosure f
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
y_1 : SimplexCategoryGenRel
f : z ⟶ y_1
hf : faces.multiplicativeClosure f
n : ℕ
j : Fin (n + 1 + 1)
g : y_1 ⟶ mk (n + 1 + 1)
hg : faces g
comp_σ :
  ∀ ⦃X Y : SimplexCategoryGenRel⦄ (i : Fin (n + 1 + 2)) (f : z ⟶ mk (n + 1)) (hf : faces.multiplicativeClosure f),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
rcases hg with ⟨i⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
comp_σ :
  ∀ (h' : δ i ≫ σ j = 𝟙 (mk (n + 1))),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
comp_σ₁ :
  ∀ (j' : Fin (n + 1)) (j'' : Fin (n + 2)) (h' : δ i ≫ σ j = σ j' ≫ δ j''),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
obtain h' | ⟨j', j'', h'⟩ := switch_δ_σ j i

Premises used: _private.0.SimplexCategoryGenRel.switch_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : δ i ≫ σ j = 𝟙 (mk (n + 1))
⊢ (e ≫ f ≫ δ i) ≫ σ j = e ≫ f

Tactic:
simp [h']
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : δ i ≫ σ j = 𝟙 (mk (n + 1))
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, _, he, hf, by simp [h']⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
comp_σ :
  ∀ (w : SimplexCategoryGenRel) (w_1 : z ⟶ w) (m₁ : w ⟶ mk n) (he₁ : P_σ w_1) (hm₁ : P_δ m₁) (h₁ : f ≫ σ j' = w_1 ≫ m₁),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
obtain ⟨_, _, m₁, ⟨he₁, hm₁, h₁⟩⟩ := factor_P_δ_σ j' f hf

Premises used: _private.0.SimplexCategoryGenRel.factor_P_δ_σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
w : SimplexCategoryGenRel
w_1 : z ⟶ w
m₁ : w ⟶ mk n
he₁ : P_σ w_1
hm₁ : P_δ m₁
h₁ : f ≫ σ j' = w_1 ≫ m₁
⊢ (e ≫ f ≫ δ i) ≫ σ j = (e ≫ w_1) ≫ m₁ ≫ δ j''

Tactic:
simp [← reassoc_of% h₁, h']
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n_1 : ℕ
z : SimplexCategoryGenRel
e : mk n_1 ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
w : SimplexCategoryGenRel
w_1 : z ⟶ w
m₁ : w ⟶ mk n
he₁ : P_σ w_1
hm₁ : P_δ m₁
h₁ : f ≫ σ j' = w_1 ≫ m₁
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n_1 ⟶ z_1) (m : z_1 ⟶ mk (n + 1)) (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
            by simp [← reassoc_of% h₁, h']⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y_1 : SimplexCategoryGenRel
f : z ⟶ y_1
hf : faces.multiplicativeClosure f
g : y_1 ⟶ mk (n' + 1)
hg : faces g
comp_σ :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (g : y_1 ⟶ mk (HAdd.hAdd (α := ℕ) 0 1)) (hg : faces g),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk 0) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
comp_σ₁ :
  ∀ (n_1 : ℕ) (j : Fin (n_1 + 1 + 1)) (g : y_1 ⟶ mk (n_1 + 1 + 1)) (hg : faces g),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk (n_1 + 1)) (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
    (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
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']⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk (n' + 1)
he : P_σ e
hm : P_δ m
comp_σ :
  ∀ (hg : faces m),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
      (e ≫ m) ≫ σ j = e_1 ≫ m_1
comp_σ₁ :
  ∀ (e : mk n ⟶ mk (n' + 1)) (he : P_σ e),
    ∃ (z : SimplexCategoryGenRel) (e_1 : mk n ⟶ z) (m : z ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = e_1 ≫ m
comp_σ₂ :
  ∀ {y : SimplexCategoryGenRel} (f : z ⟶ y) (hf : faces.multiplicativeClosure f) (g : y ⟶ mk (n' + 1)) (hg : faces g),
    ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m),
      (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m
⊢ ∃ (z_1 : SimplexCategoryGenRel) (e_1 : mk n ⟶ z_1) (m_1 : z_1 ⟶ mk n') (_ : P_σ e_1) (_ : P_δ m_1),
    (e ≫ m) ≫ σ j = e_1 ≫ m_1

Tactic:
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']⟩

Premises used: id
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
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
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
⊢ ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ y) (_ : P_σ e) (_ : P_δ m), f = 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']⟩

Premises used: id, SimplexCategoryGenRel.P_σ, SimplexCategoryGenRel.P_δ, CategoryTheory.MorphismProperty.id_mem, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
X Y : SimplexCategoryGenRel
f : X ⟶ Y
obtain :
  ∀ (z : SimplexCategoryGenRel) (e : X ⟶ z) (m : z ⟶ Y) (he : P_σ e) (hm : P_δ m) (fac : f = e ≫ m),
    Nonempty (P_σ.MapFactorizationData P_δ f)
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)

Tactic:
obtain ⟨z, e, m, he, hm, fac⟩ := exists_P_σ_P_δ_factorization f

Premises used: SimplexCategoryGenRel.exists_P_σ_P_δ_factorization
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
X Y : SimplexCategoryGenRel
f : X ⟶ Y
z : SimplexCategoryGenRel
e : X ⟶ z
m : z ⟶ Y
he : P_σ e
hm : P_δ m
fac : f = e ≫ m
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)

Tactic:
⟨⟨z, e, m, fac.symm, he, hm⟩⟩

Premises used: CategoryTheory.MorphismProperty.MapFactorizationData.mk, Nonempty.intro, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
Goal:
X Y : SimplexCategoryGenRel
f : X ⟶ Y
z : SimplexCategoryGenRel
e : X ⟶ z
m : z ⟶ Y
he : P_σ e
hm : P_δ m
fac : f = e ≫ m
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)

Tactic:
exact ⟨⟨z, e, m, fac.symm, he, hm⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
⊢ IsAdmissible m [a] ↔ a ≤ m

Tactic:
⟨fun | .singleton h => h, .singleton⟩

Premises used: LE.le, _private.0.SimplexCategoryGenRel.isAdmissible_singleton_iff.match_1, SimplexCategoryGenRel.IsAdmissible.singleton, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a b : ℕ
L : List ℕ
⊢ a < b ∧ IsAdmissible (m + 1) (b :: L) ∧ a ≤ m → IsAdmissible m (a :: b :: L)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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) []
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)
⊢ 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

Tactic:
cases L
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
⊢ 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:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a 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:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
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:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
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:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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 : ℕ
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)
⊢ 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:
simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]

Premises used: List.length_cons, and_congr_right_iff, and_comm, List.isChain_cons_cons, and_assoc, SimplexCategoryGenRel.isAdmissible_cons_cons_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : ℕ
xs : List ℕ
h_1 :
  ∀ {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 : ℕ
h_2 : x < y
h_3 : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs)
h :
  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:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : ℕ
xs : List ℕ
h_1 :
  ∀ {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 : ℕ
h_2 : x < y
h_3 : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs)
h :
  ∀ (k : ℕ) (h : k < xs.length + 1 + 1),
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k
⊢ 0 < xs.length + 1 + 1

Tactic:
grind