X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
⊢ y ∈ range (Fin.snoc s.series x) ↔ y ∈ range s.series ∨ y = x
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
⊢ y ∈ snoc s x hsat ↔ y ∈ s ∨ y = x
simp only [snoc, mem_def]
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
⊢ y ∈ range (Fin.snoc s.series x) → y ∈ range s.series ∨ y = x

case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
⊢ y ∈ range s.series ∨ y = x → y ∈ range (Fin.snoc s.series x)
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
⊢ y ∈ range (Fin.snoc s.series x) ↔ y ∈ range s.series ∨ y = x
constructor
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1 + 1)
⊢ Fin.snoc s.series x i ∈ range s.series ∨ Fin.snoc s.series x i = x
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
⊢ y ∈ range (Fin.snoc s.series x) → y ∈ range s.series ∨ y = x
rintro ⟨i, rfl⟩
case mp.intro.refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1 + 1)
⊢ Fin.snoc s.series x (Fin.last (s.length + 1)) ∈ range s.series ∨ Fin.snoc s.series x (Fin.last (s.length + 1)) = x

case mp.intro.refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i✝ : Fin (s.length + 1 + 1)
i : Fin (s.length + 1)
⊢ Fin.snoc s.series x (↑Fin.castSucc i) ∈ range s.series ∨ Fin.snoc s.series x (↑Fin.castSucc i) = x
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1 + 1)
⊢ Fin.snoc s.series x i ∈ range s.series ∨ Fin.snoc s.series x i = x
refine' Fin.lastCases _ (fun i => _) i
case mp.intro.refine'_1.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1 + 1)
⊢ Fin.snoc s.series x (Fin.last (s.length + 1)) = x
case mp.intro.refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1 + 1)
⊢ Fin.snoc s.series x (Fin.last (s.length + 1)) ∈ range s.series ∨ Fin.snoc s.series x (Fin.last (s.length + 1)) = x
right
no goals
case mp.intro.refine'_1.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1 + 1)
⊢ Fin.snoc s.series x (Fin.last (s.length + 1)) = x
simp
case mp.intro.refine'_2.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i✝ : Fin (s.length + 1 + 1)
i : Fin (s.length + 1)
⊢ Fin.snoc s.series x (↑Fin.castSucc i) ∈ range s.series
case mp.intro.refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i✝ : Fin (s.length + 1 + 1)
i : Fin (s.length + 1)
⊢ Fin.snoc s.series x (↑Fin.castSucc i) ∈ range s.series ∨ Fin.snoc s.series x (↑Fin.castSucc i) = x
left
no goals
case mp.intro.refine'_2.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i✝ : Fin (s.length + 1 + 1)
i : Fin (s.length + 1)
⊢ Fin.snoc s.series x (↑Fin.castSucc i) ∈ range s.series
simp
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
h : y ∈ range s.series ∨ y = x
⊢ y ∈ range (Fin.snoc s.series x)
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
⊢ y ∈ range s.series ∨ y = x → y ∈ range (Fin.snoc s.series x)
intro h
case mpr.inl.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1)
⊢ series s i ∈ range (Fin.snoc s.series x)

case mpr.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hsat : IsMaximal (top s) y
⊢ y ∈ range (Fin.snoc s.series y)
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hsat : IsMaximal (top s) x
h : y ∈ range s.series ∨ y = x
⊢ y ∈ range (Fin.snoc s.series x)
rcases h with (⟨i, rfl⟩ | rfl)
case mpr.inl.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1)
⊢ Fin.snoc s.series x (↑Fin.castSucc i) = series s i
case mpr.inl.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1)
⊢ series s i ∈ range (Fin.snoc s.series x)
use Fin.castSucc i
no goals
case mpr.inl.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1)
⊢ Fin.snoc s.series x (↑Fin.castSucc i) = series s i
simp
case mpr.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hsat : IsMaximal (top s) y
⊢ Fin.snoc s.series y (Fin.last (s.length + 1)) = y
case mpr.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hsat : IsMaximal (top s) y
⊢ y ∈ range (Fin.snoc s.series y)
use Fin.last _
no goals
case mpr.inr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hsat : IsMaximal (top s) y
⊢ Fin.snoc s.series y (Fin.last (s.length + 1)) = y
simp