case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ series s i ∈ eraseTop s
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hx : x ≠ top s
hxs : x ∈ s
⊢ x ∈ eraseTop s
rcases hxs with ⟨i, rfl⟩
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
hi : ↑i < Nat.succ (s.length - 1)
⊢ series s i ∈ eraseTop s
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ series s i ∈ eraseTop s
have hi : (i : ℕ) < (s.length - 1).succ := by
  conv_rhs => rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
  exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [top, s.inj, Fin.ext_iff] using hx)
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
hi : ↑i < Nat.succ (s.length - 1)
⊢ series (eraseTop s) ↑↑(↑Fin.castSucc i) = series s i
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
hi : ↑i < Nat.succ (s.length - 1)
⊢ series s i ∈ eraseTop s
refine' ⟨Fin.castSucc i, _⟩
no goals
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
hi : ↑i < Nat.succ (s.length - 1)
⊢ series (eraseTop s) ↑↑(↑Fin.castSucc i) = series s i
simp [Fin.ext_iff, Nat.mod_eq_of_lt hi]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ ↑i < s.length
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ ↑i < Nat.succ (s.length - 1)
conv_rhs => rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ ↑i < s.length
exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [top, s.inj, Fin.ext_iff] using hx)
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ ↑i ≠ s.length
simpa [top, s.inj, Fin.ext_iff] using hx