X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ range (eraseTop s).series ↔ x ≠ top s ∧ x ∈ range s.series
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ eraseTop s ↔ x ≠ top s ∧ x ∈ s
simp only [mem_def]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) ↔ x ≠ top s ∧ x ∈ range s.series
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ range (eraseTop s).series ↔ x ≠ top s ∧ x ∈ range s.series
dsimp only [eraseTop]
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) → x ≠ top s ∧ x ∈ range s.series

case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ top s ∧ x ∈ range s.series → x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) ↔ x ≠ top s ∧ x ∈ range s.series
constructor
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ≠ top s ∧
    (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ∈ range s.series
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) → x ≠ top s ∧ x ∈ range s.series
rintro ⟨i, rfl⟩
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
hi : ↑i < s.length
⊢ (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ≠ top s ∧
    (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ∈ range s.series
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ≠ top s ∧
    (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ∈ range s.series
have hi : (i : ℕ) < s.length := by
  conv_rhs => rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
  exact i.2
no goals
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
hi : ↑i < s.length
⊢ (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ≠ top s ∧
    (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ∈ range s.series
simp [top, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < Nat.succ (s.length - Nat.succ 0)
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < s.length
conv_rhs => rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < Nat.succ (s.length - Nat.succ 0)
exact i.2
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h✝ : 0 < s.length
h : x ≠ top s ∧ x ∈ range s.series
⊢ x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ top s ∧ x ∈ range s.series → x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }
intro h
no goals
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h✝ : 0 < s.length
h : x ≠ top s ∧ x ∈ range s.series
⊢ x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }
exact mem_eraseTop_of_ne_of_mem h.1 h.2