case zero
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.zero
⊢ Equivalent s₁ s₂

case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
⊢ Equivalent 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₂
⊢ Equivalent s₁ s₂
induction' hle : s₁.length with n ih generalizing s₁ s₂
no goals
case zero
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.zero
⊢ Equivalent s₁ s₂
rw [eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb ht hle]
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
⊢ Equivalent s₁ s₂
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
⊢ Equivalent s₁ s₂
have h0s₂ : 0 < s₂.length :=
  length_pos_of_bot_eq_bot_of_top_eq_top_of_length_pos hb ht (hle.symm ▸ Nat.succ_pos _)
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
⊢ Equivalent s₁ s₂
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
⊢ Equivalent s₁ s₂
rcases exists_top_eq_snoc_equivalant s₁ s₂.eraseTop.top
    (ht.symm ▸ isMaximal_eraseTop_top h0s₂)
    (hb.symm ▸ s₂.bot_eraseTop ▸ bot_le_of_mem (top_mem _)) with
  ⟨t, htb, htl, htt, hteq⟩
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent s₁ s₂
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
⊢ Equivalent s₁ s₂
have := ih t s₂.eraseTop (by simp [htb, ← hb]) htt (Nat.succ_inj'.1 (htl.trans hle))
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁))) s₂
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent s₁ s₂
refine' hteq.trans _
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
    (snoc (eraseTop s₂) (top s₂) (_ : IsMaximal (top (eraseTop s₂)) (top s₂)))
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁))) s₂
conv_rhs => rw [eq_snoc_eraseTop h0s₂]
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent (snoc t (top s₂) (_ : IsMaximal (top t) (top s₂)))
    (snoc (eraseTop s₂) (top s₂) (_ : IsMaximal (top (eraseTop s₂)) (top s₂)))
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
    (snoc (eraseTop s₂) (top s₂) (_ : IsMaximal (top (eraseTop s₂)) (top s₂)))
simp only [ht]
no goals
case succ.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁✝ s₂✝ : CompositionSeries X
hb✝ : bot s₁✝ = bot s₂✝
ht✝ : top s₁✝ = top s₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Equivalent (snoc t (top s₂) (_ : IsMaximal (top t) (top s₂)))
    (snoc (eraseTop s₂) (top s₂) (_ : IsMaximal (top (eraseTop s₂)) (top s₂)))
exact Equivalent.snoc this (by simp [htt, (isMaximal_eraseTop_top h0s₂).iso_refl])
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₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
⊢ bot t = bot (eraseTop s₂)
simp [htb, ← hb]
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₂✝
x✝ : ℕ
hle✝ : s₁✝.length = x✝
n : ℕ
ih : ∀ (s₁ s₂ : CompositionSeries X), bot s₁ = bot s₂ → top s₁ = top s₂ → s₁.length = n → Equivalent s₁ s₂
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
hle : s₁.length = Nat.succ n
h0s₂ : 0 < s₂.length
t : CompositionSeries X
htb : bot t = bot s₁
htl : t.length + 1 = s₁.length
htt : top t = top (eraseTop s₂)
hteq : Equivalent s₁ (snoc t (top s₁) (_ : IsMaximal (top t) (top s₁)))
this : Equivalent t (eraseTop s₂)
⊢ Iso (top t, top s₂) (top (eraseTop s₂), top s₂)
simp [htt, (isMaximal_eraseTop_top h0s₂).iso_refl]