X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
this : bot s₁ = top s₁
⊢ s₂.length = 0
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
⊢ s₂.length = 0
have : s₁.bot = s₁.top := congr_arg s₁ (Fin.ext (by simp [hs₁]))
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
this✝ : bot s₁ = top s₁
this : Fin.last s₂.length = 0
⊢ s₂.length = 0
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
this : bot s₁ = top s₁
⊢ s₂.length = 0
have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
  s₂.injective (hb.symm.trans (this.trans ht)).symm
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
this✝ : bot s₁ = top s₁
this : ↑(Fin.last s₂.length) = ↑0
⊢ s₂.length = 0
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
this✝ : bot s₁ = top s₁
this : Fin.last s₂.length = 0
⊢ s₂.length = 0
rw [Fin.ext_iff] at this
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
this✝ : bot s₁ = top s₁
this : ↑(Fin.last s₂.length) = ↑0
⊢ s₂.length = 0
simpa
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁ : s₁.length = 0
⊢ ↑0 = ↑(Fin.last s₁.length)
simp [hs₁]