case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ x ∈ snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s))
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s = snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s))
ext x
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ ¬x = top s ∧ x ∈ s ∨ x = top s
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ x ∈ snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s))
simp [mem_snoc, mem_eraseTop h]
no goals
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ ¬x = top s ∧ x ∈ s ∨ x = top s
by_cases h : x = s.top <;> simp [*, s.top_mem]