case zero
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.zero
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.zero ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))

case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = s.length ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
induction' hn : s.length with n ih generalizing s x
no goals
case zero
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.zero
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.zero ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
exact
  (ne_of_gt (lt_of_le_of_lt hb (lt_of_isMaximal hm))
      (forall_mem_eq_of_length_eq_zero hn s.top_mem s.bot_mem)).elim
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
have h0s : 0 < s.length := hn.symm ▸ Nat.succ_pos _
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : top (eraseTop s) = x
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))

case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
case succ
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
by_cases hetx : s.eraseTop.top = x
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : top (eraseTop s) = x
⊢ bot (eraseTop s) = bot s ∧
    (eraseTop s).length + 1 = Nat.succ n ∧
      ∃ htx, Equivalent s (snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s)))
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : top (eraseTop s) = x
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
use s.eraseTop
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : top (eraseTop s) = x
⊢ Equivalent s s
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : top (eraseTop s) = x
⊢ bot (eraseTop s) = bot s ∧
    (eraseTop s).length + 1 = Nat.succ n ∧
      ∃ htx, Equivalent s (snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s)))
simp [← hetx, hn]
no goals
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : top (eraseTop s) = x
⊢ Equivalent s s
rfl
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
have imxs : IsMaximal (x ⊓ s.eraseTop.top) s.eraseTop.top :=
  isMaximal_of_eq_inf x s.top rfl (Ne.symm hetx) hm (isMaximal_eraseTop_top h0s)
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
this :
  ∃ t,
    bot t = bot (eraseTop s) ∧
      t.length + 1 = n ∧
        ∃ htx, Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
have := ih _ _ imxs (le_inf (by simpa) (le_top_of_mem s.eraseTop.bot_mem)) (by simp [hn])
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
this :
  ∃ t,
    bot t = bot (eraseTop s) ∧
      t.length + 1 = n ∧
        ∃ htx, Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
rcases this with ⟨t, htb, htl, htt, hteqv⟩
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
have hmtx : IsMaximal t.top x :=
  isMaximal_of_eq_inf s.eraseTop.top s.top (by rw [inf_comm, htt]) hetx
    (isMaximal_eraseTop_top h0s) hm
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ bot (snoc t x hmtx) = bot s ∧
    (snoc t x hmtx).length + 1 = Nat.succ n ∧
      ∃ htx, Equivalent s (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ ∃ t, bot t = bot s ∧ t.length + 1 = Nat.succ n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
use snoc t x hmtx
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ Equivalent s (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ bot (snoc t x hmtx) = bot s ∧
    (snoc t x hmtx).length + 1 = Nat.succ n ∧
      ∃ htx, Equivalent s (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
refine' ⟨by simp [htb], by simp [htl], by simp, _⟩
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Equivalent s (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ Equivalent s (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
have : s.Equivalent ((snoc t s.eraseTop.top (htt.symm ▸ imxs)).snoc s.top
    (by simpa using isMaximal_eraseTop_top h0s)) := by
  conv_lhs => rw [eq_snoc_eraseTop h0s]
  exact Equivalent.snoc hteqv (by simpa using (isMaximal_eraseTop_top h0s).iso_refl)
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Equivalent
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
    (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Equivalent s (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
refine' this.trans _
case neg.intro.intro.intro.intro.refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Iso (top t, top (eraseTop s)) (x, top s)

case neg.intro.intro.intro.intro.refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Iso (top (eraseTop s), top s) (top t, x)
case neg.intro.intro.intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Equivalent
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
    (snoc (snoc t x hmtx) (top s) (_ : IsMaximal (top (snoc t x hmtx)) (top s)))
refine' Equivalent.snoc_snoc_swap _ _
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
⊢ bot (eraseTop s) ≤ x
simpa
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
⊢ (eraseTop s).length = n
simp [hn]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
⊢ top (eraseTop s) ⊓ x = top t
rw [inf_comm, htt]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ bot (snoc t x hmtx) = bot s
simp [htb]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ (snoc t x hmtx).length + 1 = Nat.succ n
simp [htl]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ top (snoc t x hmtx) = x
simp
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)
simpa using isMaximal_eraseTop_top h0s
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ Equivalent (snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s)))
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
conv_lhs => rw [eq_snoc_eraseTop h0s]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ Equivalent (snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s)))
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
exact Equivalent.snoc hteqv (by simpa using (isMaximal_eraseTop_top h0s).iso_refl)
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
⊢ Iso (top (eraseTop s), top s) (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))), top s)
simpa using (isMaximal_eraseTop_top h0s).iso_refl
no goals
case neg.intro.intro.intro.intro.refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Iso (top t, top (eraseTop s)) (x, top s)
exact
  iso_symm
    (second_iso_of_eq hm
      (sup_eq_of_isMaximal hm (isMaximal_eraseTop_top h0s) (Ne.symm hetx)) htt.symm)
no goals
case neg.intro.intro.intro.intro.refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ Iso (top (eraseTop s), top s) (top t, x)
exact
  second_iso_of_eq (isMaximal_eraseTop_top h0s)
    (sup_eq_of_isMaximal (isMaximal_eraseTop_top h0s) hm hetx) (by rw [inf_comm, htt])
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s✝ : CompositionSeries X
x✝¹ : X
hm✝ : IsMaximal x✝¹ (top s✝)
hb✝ : bot s✝ ≤ x✝¹
x✝ : ℕ
hn✝ : s✝.length = x✝
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (top s)),
    bot s ≤ x →
      s.length = n →
        ∃ t, bot t = bot s ∧ t.length + 1 = n ∧ ∃ htx, Equivalent s (snoc t (top s) (_ : IsMaximal (top t) (top s)))
s : CompositionSeries X
x : X
hm : IsMaximal x (top s)
hb : bot s ≤ x
hn : s.length = Nat.succ n
h0s : 0 < s.length
hetx : ¬top (eraseTop s) = x
imxs : IsMaximal (x ⊓ top (eraseTop s)) (top (eraseTop s))
t : CompositionSeries X
htb : bot t = bot (eraseTop s)
htl : t.length + 1 = n
htt : top t = x ⊓ top (eraseTop s)
hteqv : Equivalent (eraseTop s) (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))
hmtx : IsMaximal (top t) x
this :
  Equivalent s
    (snoc (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s)))) (top s)
      (_ : IsMaximal (top (snoc t (top (eraseTop s)) (_ : IsMaximal (top t) (top (eraseTop s))))) (top s)))
⊢ top (eraseTop s) ⊓ x = top t
rw [inf_comm, htt]