X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁0 : s₁.length = 0
this : ∀ (x : X), x ∈ s₁ ↔ x = top s₁
⊢ s₁ = s₂
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁0 : s₁.length = 0
⊢ s₁ = s₂
have : ∀ x, x ∈ s₁ ↔ x = s₁.top := fun x =>
  ⟨fun hx => forall_mem_eq_of_length_eq_zero hs₁0 hx s₁.top_mem, fun hx => hx.symm ▸ s₁.top_mem⟩
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = top s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = top s₂
⊢ s₁ = s₂
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁0 : s₁.length = 0
this : ∀ (x : X), x ∈ s₁ ↔ x = top s₁
⊢ s₁ = s₂
have : ∀ x, x ∈ s₂ ↔ x = s₂.top := fun x =>
  ⟨fun hx =>
    forall_mem_eq_of_length_eq_zero
      (length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb ht hs₁0) hx s₂.top_mem,
    fun hx => hx.symm ▸ s₂.top_mem⟩
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = top s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = top s₂
x✝ : X
⊢ x✝ ∈ s₁ ↔ x✝ ∈ s₂
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = top s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = top s₂
⊢ s₁ = s₂
ext
no goals
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hs₁0 : s₁.length = 0
this✝ : ∀ (x : X), x ∈ s₁ ↔ x = top s₁
this : ∀ (x : X), x ∈ s₂ ↔ x = top s₂
x✝ : X
⊢ x✝ ∈ s₁ ↔ x✝ ∈ s₂
simp [*]