-- 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:
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✝¹ : mk n' ⟶ w✝²
w✝ : w✝² ⟶ mk n'
he₁ : P_σ w✝¹
hm₁ : P_δ w✝
h₁ : δ i ≫ σ j = w✝¹ ≫ w✝
⊢ (e ≫ δ i) ≫ σ j = (e ≫ w✝¹) ≫ w✝

Tactic:
simp [← h₁]

Result:
no goals

Proof state:
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
j : Fin (0 + 1)
i✝ : Fin (0 + 2)
f : z ⟶ mk 0
hf : faces.multiplicativeClosure f
⊢ (e ≫ f ≫ δ i✝) ≫ σ j = e ≫ f

Tactic:
simp [switch_δ_σ₀]

Result:
no goals

Proof state:
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

Tactic:
exact ⟨_, _, _, he, hf, by simp [h']⟩

Result:
no goals

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

Tactic:
rcases hg with ⟨i⟩

Result:
case comp_σ.intro.intro.intro.intro.intro.of.δ
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
⊢ ∃ z e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m

Proof state:
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

Result:
no goals

Proof state:
case comp_σ.intro.intro.intro.intro.intro.comp_of.zero
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y✝ : SimplexCategoryGenRel
f : z ⟶ y✝
hf : faces.multiplicativeClosure f
j : Fin (0 + 1)
g : y✝ ⟶ mk (0 + 1)
hg : faces g
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
cases hg

Result:
case comp_σ.intro.intro.intro.intro.intro.comp_of.zero.δ
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
j : Fin (0 + 1)
i✝ : Fin (0 + 2)
f : z ⟶ mk 0
hf : faces.multiplicativeClosure f
⊢ ∃ 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.of.δ.intro.intro.intro.intro.intro
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✝¹ : mk n' ⟶ w✝²
w✝ : w✝² ⟶ mk n'
he₁ : P_σ w✝¹
hm₁ : P_δ w✝
h₁ : δ i ≫ σ j = w✝¹ ≫ w✝
⊢ ∃ z e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, _, P_σ.comp_mem _ _ he he₁, hm₁,
  by simp [← h₁]⟩

Result:
no goals

Proof state:
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

Tactic:
exact ⟨_, _, m₁ ≫ δ j'', P_σ.comp_mem _ _ he he₁, P_δ.comp_mem _ _ hm₁ (P_δ.δ _),
  by simp [← reassoc_of% h₁, h']⟩

Result:
no goals

Proof state:
case id
x y : SimplexCategoryGenRel
n : ℕ
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), 𝟙 (mk n) = e ≫ m

Tactic:
use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id_mem _, P_δ.id_mem _

Result:
case h
x y : SimplexCategoryGenRel
n : ℕ
⊢ 𝟙 (mk n) = 𝟙 (mk n) ≫ 𝟙 (mk n)

Proof state:
case comp_σ.intro.intro.intro.intro.intro.of.δ
x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
X Y : SimplexCategoryGenRel
i : Fin (n' + 2)
e : mk n ⟶ mk n'
he : P_σ e
⊢ ∃ z e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m

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

Result:
case comp_σ.intro.intro.intro.intro.intro.of.δ.intro.intro.intro.intro.intro
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✝¹ : mk n' ⟶ w✝²
w✝ : w✝² ⟶ mk n'
he₁ : P_σ w✝¹
hm₁ : P_δ w✝
h₁ : δ i ≫ σ j = w✝¹ ≫ w✝
⊢ ∃ z e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ δ i) ≫ σ j = e_1 ≫ m

Proof state:
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

Result:
no goals

Proof state:
case comp_δ
x y : SimplexCategoryGenRel
n n' : ℕ
f : mk n ⟶ mk n'
j : Fin (n' + 2)
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' + 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

Proof state:
case comp_σ.intro.intro.intro.intro.intro.comp_of.zero.δ
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
j : Fin (0 + 1)
i✝ : Fin (0 + 2)
f : z ⟶ mk 0
hf : faces.multiplicativeClosure f
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i✝) ≫ σ j = e_1 ≫ m

Tactic:
exact ⟨_, _, _, he, hf, by simp [switch_δ_σ₀]⟩

Result:
no goals

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
y✝ : SimplexCategoryGenRel
f : z ⟶ y✝
hf : faces.multiplicativeClosure f
n : ℕ
j : Fin (n + 1 + 1)
g : y✝ ⟶ mk (n + 1 + 1)
hg : faces g
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
rcases hg with ⟨i⟩

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

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
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₁
⊢ (e ≫ f ≫ δ i) ≫ σ j = (e ≫ w✝) ≫ m₁ ≫ δ j''

Tactic:
simp [← reassoc_of% h₁, h']

Result:
no goals

Proof state:
case h
x y : SimplexCategoryGenRel
n : ℕ
⊢ 𝟙 (mk n) = 𝟙 (mk n) ≫ 𝟙 (mk n)

Tactic:
simp

Result:
no goals