-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
/-- An auxiliary lemma that shows there exists a factorization as a P_δ followed by a P_σ for
morphisms of the form `P_δ ≫ σ`. -/
private lemma factor_P_δ_σ {n : ℕ} (i : Fin (n + 1)) {x : SimplexCategoryGenRel}
    (f : x ⟶ mk (n + 1)) (hf : P_δ f) : ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ mk n)
      (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Proof state:
case zero.comp_of.δ
i : Fin (0 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (0 + 2)
j : x ⟶ mk 0
hf : faces.multiplicativeClosure j
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf

Result:
case zero.comp_of.δ.inl.intro
i : Fin (0 + 1)
X Y : SimplexCategoryGenRel
k : Fin (0 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

case zero.comp_of.δ.inr
i : Fin (0 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (0 + 2)
j : x ⟶ mk 0
hf : faces.multiplicativeClosure j
hf' : x.len < (mk 0).len
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (j ≫ δ k) ≫ σ i = e ≫ m

Proof state:
case zero.comp_of.δ.inl.intro
i : Fin (0 + 1)
X Y : SimplexCategoryGenRel
k : Fin (0 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

Tactic:
simpa using factor_δ_σ i k

Result:
no goals

Proof state:
case succ.comp_of.δ
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ hf

Result:
case succ.comp_of.δ.inl.intro
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
hf : faces.multiplicativeClosure (eqToHom ⋯)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (eqToHom ⋯ ≫ δ k) ≫ σ i = e ≫ m

case succ.comp_of.δ.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Proof state:
case succ.comp_of.δ.inr.inr.intro.intro
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf

Result:
case succ.comp_of.δ.inr.inr.intro.intro.intro.intro.intro.intro.intro
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
z : SimplexCategoryGenRel
e : x ⟶ z
m : z ⟶ mk n
he : P_σ e
hm : P_δ m
fac : f ≫ σ j = e ≫ m
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Proof state:
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))
⊢ (f ≫ δ k) ≫ σ i = 𝟙 x ≫ f

Tactic:
simp [h'']

Result:
no goals