X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (top (eraseTop s)) (top s)
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ IsMaximal (top (eraseTop s)) (top s)
have : s.length - 1 + 1 = s.length := by
  conv_rhs => rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (series s { val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }) (series s (Fin.last s.length))
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (top (eraseTop s)) (top s)
rw [top_eraseTop, top]
case h.e'_5.h.e'_5
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ Fin.last s.length = Fin.succ { val := s.length - 1, isLt := (_ : s.length - 1 < s.length) }
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (series s { val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }) (series s (Fin.last s.length))
convert s.step ⟨s.length - 1, Nat.sub_lt h zero_lt_one⟩
case h.e'_5.h.e'_5.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ ↑(Fin.last s.length) = ↑(Fin.succ { val := s.length - 1, isLt := (_ : s.length - 1 < s.length) })
case h.e'_5.h.e'_5
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ Fin.last s.length = Fin.succ { val := s.length - 1, isLt := (_ : s.length - 1 < s.length) }
ext
no goals
case h.e'_5.h.e'_5.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ ↑(Fin.last s.length) = ↑(Fin.succ { val := s.length - 1, isLt := (_ : s.length - 1 < s.length) })
simp [this]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s.length - 1 + 1 = s.length
conv_rhs => rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]