X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
hs : s.length = 0
⊢ False
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
⊢ s.length ≠ 0
intro hs
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
hs : s.length = 0
⊢ top s = top (eraseTop s)
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
hs : s.length = 0
⊢ False
refine' ne_of_gt (lt_of_isMaximal h) _
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
hs : s.length = 0
⊢ top s = top (eraseTop s)
simp [top, Fin.ext_iff, hs]