-- 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:
i : Fin (0 + 1)
⊢ 𝟙 (mk (0 + 1)) ≫ σ i = σ i ≫ 𝟙 (mk 0)

Tactic:
simp

Result:
no goals

Proof state:
case zero.id
i : Fin (0 + 1)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), 𝟙 (mk (0 + 1)) ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩

Result:
no goals

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

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

Result:
case succ.comp_of.δ.inr.inl
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))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

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

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)
⊢ 𝟙 (mk (n + 1 + 1)) ≫ σ i = σ i ≫ 𝟙 (mk (n + 1))

Tactic:
simp

Result:
no goals

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

Tactic:
simp [h'', reassoc_of% fac]

Result:
no goals

Proof state:
case succ.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)
i✝ : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m

Tactic:
exact factor_δ_σ _ _

Result:
no goals

Proof state:
case zero.of
i : Fin (0 + 1)
x : SimplexCategoryGenRel
f : x ⟶ mk (0 + 1)
h : faces f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h

Result:
case zero.of.δ
i : Fin (0 + 1)
i✝ : Fin (0 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m

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

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

Result:
no goals

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

Tactic:
simp at hf'

Result:
no goals

Proof state:
case succ.id
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)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), 𝟙 (mk (n + 1 + 1)) ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩

Result:
no goals

Proof state:
case succ.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 : SimplexCategoryGenRel
f : x ⟶ mk (n + 1 + 1)
h : faces f
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m

Tactic:
cases h

Result:
case succ.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)
i✝ : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m

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

Tactic:
obtain ⟨k⟩ := hg

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

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

Tactic:
simpa using factor_δ_σ i k

Result:
no goals

Proof state:
case succ.comp_of.δ.inr.inl
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))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩

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

Tactic:
obtain ⟨k⟩ := hg

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

Proof state:
case zero.of.δ
i : Fin (0 + 1)
i✝ : Fin (0 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m

Tactic:
exact factor_δ_σ _ _

Result:
no goals