case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ ∃ i, θ = σ i
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
⊢ ∃ i, θ = σ i
rcases eq_σ_comp_of_not_injective θ (by
  by_contra h
  simpa using le_of_mono (mono_iff_injective.mpr h)) with ⟨i, θ', h⟩
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ θ = σ i
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ ∃ i, θ = σ i
use i
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
this : Epi (σ i ≫ θ')
⊢ θ = σ i
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ θ = σ i
haveI : Epi (σ i ≫ θ') := by
  rw [← h]
  infer_instance
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ θ = σ i
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
this : Epi (σ i ≫ θ')
⊢ θ = σ i
haveI := CategoryTheory.epi_of_epi (σ i) θ'
no goals
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ θ = σ i
rw [h, eq_id_of_epi θ', Category.comp_id]
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
h : Function.Injective ↑(Hom.toOrderHom θ)
⊢ False
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
⊢ ¬Function.Injective ↑(Hom.toOrderHom θ)
by_contra h
no goals
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
h : Function.Injective ↑(Hom.toOrderHom θ)
⊢ False
simpa using le_of_mono (mono_iff_injective.mpr h)
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ Epi θ
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ Epi (σ i ≫ θ')
rw [← h]
no goals
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ Epi θ
infer_instance