exact isInitSeg_initSeg
case intro.inr.inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) (s.erase (s.min' ?m.16021)).card

α : Type u_1
inst✝¹ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
s✝ t : Finset α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : s.card > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) s.card
⊢ s.Nonempty
no goals