case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ ∃ i, θ = δ i
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
⊢ ∃ i, θ = δ i
rcases eq_comp_δ_of_not_surjective θ (by
  by_contra h
  simpa using le_of_epi (epi_iff_surjective.mpr h)) with ⟨i, θ', h⟩
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ θ = δ i
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ ∃ i, θ = δ i
use i
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ θ = δ i
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ θ = δ i
haveI : Mono (θ' ≫ δ i) := by
  rw [← h]
  infer_instance
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ θ = δ i
haveI := CategoryTheory.mono_of_mono θ' (δ i)
no goals
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i
rw [h, eq_id_of_mono θ', Category.id_comp]
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
h : Function.Surjective ↑(Hom.toOrderHom θ)
⊢ False
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
⊢ ¬Function.Surjective ↑(Hom.toOrderHom θ)
by_contra h
no goals
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
h : Function.Surjective ↑(Hom.toOrderHom θ)
⊢ False
simpa using le_of_epi (epi_iff_surjective.mpr h)
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ Mono θ
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ Mono (θ' ≫ δ i)
rw [← h]
no goals
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ Mono θ
infer_instance