-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
theorem exists_P_σ_P_δ_factorization {x y : SimplexCategoryGenRel} (f : x ⟶ y) :
    ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ y)
        (_ : P_σ e) (_ : P_δ m), f = e ≫ m

Proof state:
case comp_σ.intro.intro.intro.intro.intro.comp_of.succ.δ
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ 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
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

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

Result:
case comp_σ.intro.intro.intro.intro.intro.comp_of.succ.δ.inl
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ 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 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

case comp_σ.intro.intro.intro.intro.intro.comp_of.succ.δ.inr.intro.intro
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ 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''
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

Proof state:
case comp_σ.intro.intro.intro.intro.intro.id
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
e : mk n ⟶ mk (n' + 1)
he : P_σ e
⊢ ∃ z e_1 m, ∃ (_ : 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⟩

Result:
no goals

Proof state:
case comp_δ.intro.intro.intro.intro.intro
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 e_1 m_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⟩

Result:
no goals

Proof state:
case comp_σ
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk (n' + 1)
j : Fin (n' + 1)
h : ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ j = e ≫ m

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

Result:
case comp_σ.intro.intro.intro.intro.intro
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
⊢ ∃ z_1 e_1 m_1, ∃ (_ : P_σ e_1) (_ : P_δ m_1), (e ≫ m) ≫ σ j = e_1 ≫ m_1

Proof state:
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ 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']

Result:
no goals

Proof state:
case comp_σ.intro.intro.intro.intro.intro.comp_of.succ.δ.inr.intro.intro
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ 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''
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m

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

Result:
case comp_σ.intro.intro.intro.intro.intro.comp_of.succ.δ.inr.intro.intro.intro.intro.intro.intro.intro
x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ 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✝ : z ⟶ w✝¹
m₁ : w✝¹ ⟶ mk n
he₁ : P_σ w✝
hm₁ : P_δ m₁
h₁ : f ≫ σ j' = w✝ ≫ m₁
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i) ≫ σ j = e_1 ≫ m