-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
/-- An auxiliary lemma to show that one can always use the simplicial identities to simplify a term
in the form `δ ≫ σ` into either an identity, or a term of the form `σ ≫ δ`. This is the crucial
special case to induct on to get an epi-mono factorization for all morphisms. -/
private lemma switch_δ_σ {n : ℕ} (i : Fin (n + 2)) (i' : Fin (n + 3)) :
    δ i' ≫ σ i = 𝟙 _ ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Proof state:
case inr.inr.intro.intro
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' < i.succ
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'

Tactic:
rw [← Fin.le_castSucc_iff] at h

Result:
case inr.inr.intro.intro
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'

Proof state:
case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.castSucc < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
rw [Fin.castSucc_lt_iff_succ_le] at h

Result:
case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Proof state:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = σ i ≫ δ i'

Tactic:
rw [δ_comp_σ_of_le h]

Result:
no goals

Proof state:
case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain h | rfl := h.lt_or_eq

Result:
case inl.inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h✝ : i.succ ≤ i'
h : i.succ < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

case inl.inr
n : ℕ
i : Fin (n + 2)
h : i.succ ≤ i.succ
⊢ δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.succ ≫ σ i = σ j ≫ δ j'

Proof state:
case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i', rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Result:
case inr.inr.intro
n : ℕ
i i' : Fin (n + 2)
h : i'.castSucc < i.castSucc
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'

Proof state:
case inl.inl.intro.intro
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h✝ : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ δ i'.succ ≫ σ i.castSucc = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i.castSucc = σ j ≫ δ j'

Tactic:
exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_gt h]⟩

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain h | rfl | h := lt_trichotomy i.castSucc i'

Result:
case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.castSucc < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

case inr.inl
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.castSucc ≫ σ i = σ j ≫ δ j'

case inr.inr
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i' < i.castSucc
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Proof state:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h✝ : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ δ i'.succ ≫ σ i.castSucc = σ i ≫ δ i'

Tactic:
rw [δ_comp_σ_of_gt h]

Result:
no goals

Proof state:
case inl.inl.intro
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i.succ < i'.succ
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'

Tactic:
rw [Fin.succ_lt_succ_iff] at h

Result:
case inl.inl.intro
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i < i'
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'

Proof state:
case inr.inl
n : ℕ
i : Fin (n + 2)
⊢ δ i.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
exact Or.inl δ_comp_σ_self

Result:
no goals

Proof state:
case inl.inr
n : ℕ
i : Fin (n + 2)
h : i.succ ≤ i.succ
⊢ δ i.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i.succ ≫ σ i = σ j ≫ δ j'

Tactic:
exact Or.inl δ_comp_σ_succ

Result:
no goals

Proof state:
case inr.inr.intro
n : ℕ
i i' : Fin (n + 2)
h : i'.castSucc < i.castSucc
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
rw [Fin.castSucc_lt_castSucc_iff] at h

Result:
case inr.inr.intro
n : ℕ
i i' : Fin (n + 2)
h : i' < i
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'

Proof state:
case inr.inr.intro.intro
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'

Tactic:
exact Or.inr ⟨i, i', by rw [δ_comp_σ_of_le h]⟩

Result:
no goals

Proof state:
case inl.inl.intro
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i < i'
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Result:
case inl.inl.intro.intro
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h✝ : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ δ i'.succ ≫ σ i.castSucc = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i.castSucc = σ j ≫ δ j'

Proof state:
case inr.inr.intro
n : ℕ
i i' : Fin (n + 2)
h : i' < i
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)

Result:
case inr.inr.intro.intro
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' < i.succ
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'

Proof state:
case inl.inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h✝ : i.succ ≤ i'
h : i.succ < i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
obtain ⟨i', rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)

Result:
case inl.inl.intro
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i.succ < i'.succ
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'