case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
i : Fin (s.length + 1)
hx : series s i ∈ s
⊢ series s i ≤ y ∨ y ≤ series s i
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y ∨ y ≤ x
rcases Set.mem_range.1 hx with ⟨i, rfl⟩
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ∈ s
j : Fin (s.length + 1)
hy : series s j ∈ s
⊢ series s i ≤ series s j ∨ series s j ≤ series s i
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
i : Fin (s.length + 1)
hx : series s i ∈ s
⊢ series s i ≤ y ∨ y ≤ series s i
rcases Set.mem_range.1 hy with ⟨j, rfl⟩
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ∈ s
j : Fin (s.length + 1)
hy : series s j ∈ s
⊢ i ≤ j ∨ j ≤ i
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ∈ s
j : Fin (s.length + 1)
hy : series s j ∈ s
⊢ series s i ≤ series s j ∨ series s j ≤ series s i
rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]
no goals
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ∈ s
j : Fin (s.length + 1)
hy : series s j ∈ s
⊢ i ≤ j ∨ j ≤ i
exact le_total i j