[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y
[PROOFSTEP]
rw [inf_comm]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (x ⊔ y)
hyz : IsMaximal y (x ⊔ y)
⊢ IsMaximal (y ⊓ x) y
[PROOFSTEP]
rw [sup_comm] at hxz hyz
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxz : IsMaximal x (y ⊔ x)
hyz : IsMaximal y (y ⊔ x)
⊢ IsMaximal (y ⊓ x) y
[PROOFSTEP]
exact isMaximal_inf_left_of_isMaximal_sup hyz hxz
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
⊢ IsMaximal a y
[PROOFSTEP]
have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : IsMaximal x b
hyb : IsMaximal y b
hb : x ⊔ y = b
⊢ IsMaximal a y
[PROOFSTEP]
substs a b
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hxy : x ≠ y
hxb : IsMaximal x (x ⊔ y)
hyb : IsMaximal y (x ⊔ y)
⊢ IsMaximal (x ⊓ y) y
[PROOFSTEP]
exact isMaximal_inf_right_of_isMaximal_sup hxb hyb
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y a b : X
hm : IsMaximal x a
ha : x ⊔ y = a
hb : x ⊓ y = b
⊢ Iso (x, a) (b, y)
[PROOFSTEP]
substs a b
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
x y : X
hm : IsMaximal x (x ⊔ y)
⊢ Iso (x, x ⊔ y) (x ⊓ y, y)
[PROOFSTEP]
exact second_iso hm
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y ∨ y ≤ x
[PROOFSTEP]
rcases Set.mem_range.1 hx with ⟨i, rfl⟩
[GOAL]
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
i : Fin (s.length + 1)
hx : series s i ∈ s
⊢ series s i ≤ y ∨ y ≤ series s i
[PROOFSTEP]
rcases Set.mem_range.1 hy with ⟨j, rfl⟩
[GOAL]
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ∈ s
j : Fin (s.length + 1)
hy : series s j ∈ s
⊢ series s i ≤ series s j ∨ series s j ≤ series s i
[PROOFSTEP]
rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]
[GOAL]
case intro.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ∈ s
j : Fin (s.length + 1)
hy : series s j ∈ s
⊢ i ≤ j ∨ j ≤ i
[PROOFSTEP]
exact le_total i j
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hl : s₁.length = s₂.length
h :
  ∀ (i : Fin (s₁.length + 1)), series s₁ i = series s₂ (↑(Fin.castIso (_ : Nat.succ s₁.length = Nat.succ s₂.length)) i)
⊢ s₁ = s₂
[PROOFSTEP]
cases s₁
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₂ : CompositionSeries X
length✝ : ℕ
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
hl : { length := length✝, series := series✝, step' := step'✝ }.length = s₂.length
h :
  ∀ (i : Fin ({ length := length✝, series := series✝, step' := step'✝ }.length + 1)),
    series { length := length✝, series := series✝, step' := step'✝ } i =
      series s₂
        (↑(Fin.castIso
              (_ : Nat.succ { length := length✝, series := series✝, step' := step'✝ }.length = Nat.succ s₂.length))
          i)
⊢ { length := length✝, series := series✝, step' := step'✝ } = s₂
[PROOFSTEP]
cases s₂
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝¹ : ℕ
series✝¹ : Fin (length✝¹ + 1) → X
step'✝¹ : ∀ (i : Fin length✝¹), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
length✝ : ℕ
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
hl :
  { length := length✝¹, series := series✝¹, step' := step'✝¹ }.length =
    { length := length✝, series := series✝, step' := step'✝ }.length
h :
  ∀ (i : Fin ({ length := length✝¹, series := series✝¹, step' := step'✝¹ }.length + 1)),
    series { length := length✝¹, series := series✝¹, step' := step'✝¹ } i =
      series { length := length✝, series := series✝, step' := step'✝ }
        (↑(Fin.castIso
              (_ :
                Nat.succ { length := length✝¹, series := series✝¹, step' := step'✝¹ }.length =
                  Nat.succ { length := length✝, series := series✝, step' := step'✝ }.length))
          i)
⊢ { length := length✝¹, series := series✝¹, step' := step'✝¹ } =
    { length := length✝, series := series✝, step' := step'✝ }
[PROOFSTEP]
dsimp at hl h
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝¹ : ℕ
series✝¹ : Fin (length✝¹ + 1) → X
step'✝¹ : ∀ (i : Fin length✝¹), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
length✝ : ℕ
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
hl : length✝¹ = length✝
h : ∀ (i : Fin (length✝¹ + 1)), series✝¹ i = series✝ (↑(Fin.castIso (_ : Nat.succ length✝¹ = Nat.succ length✝)) i)
⊢ { length := length✝¹, series := series✝¹, step' := step'✝¹ } =
    { length := length✝, series := series✝, step' := step'✝ }
[PROOFSTEP]
subst hl
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝ : ℕ
series✝¹ : Fin (length✝ + 1) → X
step'✝¹ : ∀ (i : Fin length✝), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
h : ∀ (i : Fin (length✝ + 1)), series✝¹ i = series✝ (↑(Fin.castIso (_ : Nat.succ length✝ = Nat.succ length✝)) i)
⊢ { length := length✝, series := series✝¹, step' := step'✝¹ } =
    { length := length✝, series := series✝, step' := step'✝ }
[PROOFSTEP]
simpa [Function.funext_iff] using h
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ List.length (toList s) = s.length + 1
[PROOFSTEP]
rw [toList, List.length_ofFn]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ toList s ≠ []
[PROOFSTEP]
rw [← List.length_pos_iff_ne_nil, length_toList]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ 0 < s.length + 1
[PROOFSTEP]
exact Nat.succ_pos _
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : List.ofFn s₁.series = List.ofFn s₂.series
⊢ s₁ = s₂
[PROOFSTEP]
have h₁ : s₁.length = s₂.length :=
  Nat.succ_injective ((List.length_ofFn s₁).symm.trans <| (congr_arg List.length h).trans <| List.length_ofFn s₂)
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : List.ofFn s₁.series = List.ofFn s₂.series
h₁ : s₁.length = s₂.length
⊢ s₁ = s₂
[PROOFSTEP]
have h₂ : ∀ i : Fin s₁.length.succ, s₁ i = s₂ (Fin.castIso (congr_arg Nat.succ h₁) i) :=
  -- Porting note: `List.nthLe_ofFn` has been deprecated but `List.get_ofFn` has a
      --               different type, so we do golf here.congr_fun <|
    List.ofFn_injective <| h.trans <| List.ofFn_congr (congr_arg Nat.succ h₁).symm _
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : List.ofFn s₁.series = List.ofFn s₂.series
h₁ : s₁.length = s₂.length
h₂ :
  ∀ (i : Fin (Nat.succ s₁.length)),
    series s₁ i = series s₂ (↑(Fin.castIso (_ : Nat.succ s₁.length = Nat.succ s₂.length)) i)
⊢ s₁ = s₂
[PROOFSTEP]
cases s₁
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₂ : CompositionSeries X
length✝ : ℕ
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
h : List.ofFn { length := length✝, series := series✝, step' := step'✝ }.series = List.ofFn s₂.series
h₁ : { length := length✝, series := series✝, step' := step'✝ }.length = s₂.length
h₂ :
  ∀ (i : Fin (Nat.succ { length := length✝, series := series✝, step' := step'✝ }.length)),
    series { length := length✝, series := series✝, step' := step'✝ } i =
      series s₂
        (↑(Fin.castIso
              (_ : Nat.succ { length := length✝, series := series✝, step' := step'✝ }.length = Nat.succ s₂.length))
          i)
⊢ { length := length✝, series := series✝, step' := step'✝ } = s₂
[PROOFSTEP]
cases s₂
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝¹ : ℕ
series✝¹ : Fin (length✝¹ + 1) → X
step'✝¹ : ∀ (i : Fin length✝¹), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
length✝ : ℕ
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
h :
  List.ofFn { length := length✝¹, series := series✝¹, step' := step'✝¹ }.series =
    List.ofFn { length := length✝, series := series✝, step' := step'✝ }.series
h₁ :
  { length := length✝¹, series := series✝¹, step' := step'✝¹ }.length =
    { length := length✝, series := series✝, step' := step'✝ }.length
h₂ :
  ∀ (i : Fin (Nat.succ { length := length✝¹, series := series✝¹, step' := step'✝¹ }.length)),
    series { length := length✝¹, series := series✝¹, step' := step'✝¹ } i =
      series { length := length✝, series := series✝, step' := step'✝ }
        (↑(Fin.castIso
              (_ :
                Nat.succ { length := length✝¹, series := series✝¹, step' := step'✝¹ }.length =
                  Nat.succ { length := length✝, series := series✝, step' := step'✝ }.length))
          i)
⊢ { length := length✝¹, series := series✝¹, step' := step'✝¹ } =
    { length := length✝, series := series✝, step' := step'✝ }
[PROOFSTEP]
dsimp at h h₁ h₂
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝¹ : ℕ
series✝¹ : Fin (length✝¹ + 1) → X
step'✝¹ : ∀ (i : Fin length✝¹), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
length✝ : ℕ
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
h : List.ofFn series✝¹ = List.ofFn series✝
h₁ : length✝¹ = length✝
h₂ : ∀ (i : Fin (Nat.succ length✝¹)), series✝¹ i = series✝ (↑(Fin.castIso (_ : Nat.succ length✝¹ = Nat.succ length✝)) i)
⊢ { length := length✝¹, series := series✝¹, step' := step'✝¹ } =
    { length := length✝, series := series✝, step' := step'✝ }
[PROOFSTEP]
subst h₁
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝ : ℕ
series✝¹ : Fin (length✝ + 1) → X
step'✝¹ : ∀ (i : Fin length✝), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
h : List.ofFn series✝¹ = List.ofFn series✝
h₂ : ∀ (i : Fin (Nat.succ length✝)), series✝¹ i = series✝ (↑(Fin.castIso (_ : Nat.succ length✝ = Nat.succ length✝)) i)
⊢ { length := length✝, series := series✝¹, step' := step'✝¹ } =
    { length := length✝, series := series✝, step' := step'✝ }
[PROOFSTEP]
simp only [mk.injEq, heq_eq_eq, true_and]
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝ : ℕ
series✝¹ : Fin (length✝ + 1) → X
step'✝¹ : ∀ (i : Fin length✝), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
h : List.ofFn series✝¹ = List.ofFn series✝
h₂ : ∀ (i : Fin (Nat.succ length✝)), series✝¹ i = series✝ (↑(Fin.castIso (_ : Nat.succ length✝ = Nat.succ length✝)) i)
⊢ series✝¹ = series✝
[PROOFSTEP]
simp only [Fin.castIso_refl] at h₂
[GOAL]
case mk.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
length✝ : ℕ
series✝¹ : Fin (length✝ + 1) → X
step'✝¹ : ∀ (i : Fin length✝), IsMaximal (series✝¹ (Fin.castSucc i)) (series✝¹ (Fin.succ i))
series✝ : Fin (length✝ + 1) → X
step'✝ : ∀ (i : Fin length✝), IsMaximal (series✝ (Fin.castSucc i)) (series✝ (Fin.succ i))
h : List.ofFn series✝¹ = List.ofFn series✝
h₂ : ∀ (i : Fin (Nat.succ length✝)), series✝¹ i = series✝ (↑(OrderIso.refl (Fin (Nat.succ length✝))) i)
⊢ series✝¹ = series✝
[PROOFSTEP]
exact funext h₂
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : ℕ) (h : i < List.length (toList s) - 1),
    IsMaximal (List.get (toList s) { val := i, isLt := (_ : i < List.length (toList s)) })
      (List.get (toList s) { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) })
[PROOFSTEP]
intro i hi
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < List.length (toList s) - 1
⊢ IsMaximal (List.get (toList s) { val := i, isLt := (_ : i < List.length (toList s)) })
    (List.get (toList s) { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) })
[PROOFSTEP]
simp only [toList, List.get_ofFn]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < List.length (toList s) - 1
⊢ IsMaximal
    (series s
      (↑(Fin.castIso (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i, isLt := (_ : i < List.length (toList s)) }))
    (series s
      (↑(Fin.castIso (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) }))
[PROOFSTEP]
rw [length_toList] at hi
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi✝ : i < List.length (toList s) - 1
hi : i < s.length + 1 - 1
⊢ IsMaximal
    (series s
      (↑(Fin.castIso (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i, isLt := (_ : i < List.length (toList s)) }))
    (series s
      (↑(Fin.castIso (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) }))
[PROOFSTEP]
exact s.step ⟨i, hi⟩
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ List.get (toList s) i < List.get (toList s) j
[PROOFSTEP]
dsimp [toList]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ List.get (List.ofFn s.series) i < List.get (List.ofFn s.series) j
[PROOFSTEP]
rw [List.get_ofFn, List.get_ofFn]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ series s (↑(Fin.castIso (_ : List.length (List.ofFn s.series) = s.length + 1)) i) <
    series s (↑(Fin.castIso (_ : List.length (List.ofFn s.series) = s.length + 1)) j)
[PROOFSTEP]
exact s.strictMono h
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
⊢ x ∈ toList s ↔ x ∈ s
[PROOFSTEP]
rw [toList, List.mem_ofFn, mem_def]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : Fin (List.length l - 1 + 1)
⊢ ↑i < List.length l
[PROOFSTEP]
conv_rhs => rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : Fin (List.length l - 1 + 1)
| List.length l
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : Fin (List.length l - 1 + 1)
| List.length l
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : Fin (List.length l - 1 + 1)
| List.length l
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (Nat.succ_le_of_lt (List.length_pos_of_ne_nil hl))]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : Fin (List.length l - 1 + 1)
⊢ ↑i < List.length l - Nat.succ 0 + Nat.succ 0
[PROOFSTEP]
exact i.2
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s)) = s
[PROOFSTEP]
refine' ext_fun _ _
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length = s.length
[PROOFSTEP]
rw [length_ofList, length_toList, Nat.succ_sub_one]
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : Fin ((ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length + 1)),
    series (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))) i =
      series s
        (↑(Fin.castIso
              (_ :
                Nat.succ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length =
                  Nat.succ s.length))
          i)
[PROOFSTEP]
rintro
  ⟨i, hi⟩
      -- Porting note: Was `dsimp [ofList, toList]; rw [List.nthLe_ofFn']`.
[GOAL]
case refine'_2.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length + 1
⊢ series (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))) { val := i, isLt := hi } =
    series s
      (↑(Fin.castIso
            (_ :
              Nat.succ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length =
                Nat.succ s.length))
        { val := i, isLt := hi })
[PROOFSTEP]
simp [ofList, toList, -List.ofFn_succ]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
⊢ toList (ofList l hl hc) = l
[PROOFSTEP]
refine' List.ext_get _ _
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
⊢ List.length (toList (ofList l hl hc)) = List.length l
[PROOFSTEP]
rw [length_toList, length_ofList, tsub_add_cancel_of_le (Nat.succ_le_of_lt <| List.length_pos_of_ne_nil hl)]
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
⊢ ∀ (n : ℕ) (h₁ : n < List.length (toList (ofList l hl hc))) (h₂ : n < List.length l),
    List.get (toList (ofList l hl hc)) { val := n, isLt := h₁ } = List.get l { val := n, isLt := h₂ }
[PROOFSTEP]
intro i hi hi'
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.get (toList (ofList l hl hc)) { val := i, isLt := hi } = List.get l { val := i, isLt := hi' }
[PROOFSTEP]
dsimp [ofList, toList]
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.get (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) { val := i, isLt := hi } =
    List.get l { val := i, isLt := hi' }
[PROOFSTEP]
rw [List.get_ofFn]
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.nthLe l
      ↑(↑(Fin.castIso
              (_ : List.length (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) = List.length l - 1 + 1))
          { val := i, isLt := hi })
      (_ :
        ↑(↑(Fin.castIso
                  (_ :
                    List.length (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) = List.length l - 1 + 1))
              { val := i, isLt := hi }) <
          List.length l) =
    List.get l { val := i, isLt := hi' }
[PROOFSTEP]
rfl
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ toList s₁ ~ toList s₂
[PROOFSTEP]
classical exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup (Finset.ext <| by simp [*])
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ toList s₁ ~ toList s₂
[PROOFSTEP]
exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup (Finset.ext <| by simp [*])
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ ∀ (a : X), a ∈ List.toFinset (toList s₁) ↔ a ∈ List.toFinset (toList s₂)
[PROOFSTEP]
simp [*]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length - 1)
⊢ IsMaximal ((fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) (Fin.castSucc i))
    ((fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) (Fin.succ i))
[PROOFSTEP]
have := s.step ⟨i, lt_of_lt_of_le i.2 tsub_le_self⟩
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length - 1)
this :
  IsMaximal (series s (Fin.castSucc { val := ↑i, isLt := (_ : ↑i < s.length) }))
    (series s (Fin.succ { val := ↑i, isLt := (_ : ↑i < s.length) }))
⊢ IsMaximal ((fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) (Fin.castSucc i))
    ((fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) (Fin.succ i))
[PROOFSTEP]
cases i
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
val✝ : ℕ
isLt✝ : val✝ < s.length - 1
this :
  IsMaximal
    (series s
      (Fin.castSucc
        { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := (_ : ↑{ val := val✝, isLt := isLt✝ } < s.length) }))
    (series s
      (Fin.succ { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := (_ : ↑{ val := val✝, isLt := isLt✝ } < s.length) }))
⊢ IsMaximal
    ((fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) (Fin.castSucc { val := val✝, isLt := isLt✝ }))
    ((fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) (Fin.succ { val := val✝, isLt := isLt✝ }))
[PROOFSTEP]
exact this
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ { val := ↑(Fin.last (eraseTop s).length), isLt := (_ : ↑(Fin.last (eraseTop s).length) < s.length + 1) } =
    { val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ↑{ val := ↑(Fin.last (eraseTop s).length), isLt := (_ : ↑(Fin.last (eraseTop s).length) < s.length + 1) } =
    ↑{ val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }
[PROOFSTEP]
simp only [eraseTop_length, Fin.val_last, Fin.coe_castSucc, Fin.coe_ofNat_eq_mod, Fin.val_mk]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ top (eraseTop s) ≤ top s
[PROOFSTEP]
simp [eraseTop, top, s.strictMono.le_iff_le, Fin.le_iff_val_le_val, tsub_le_self]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hx : x ≠ top s
hxs : x ∈ s
⊢ x ∈ eraseTop s
[PROOFSTEP]
rcases hxs with ⟨i, rfl⟩
[GOAL]
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ series s i ∈ eraseTop s
[PROOFSTEP]
have hi : (i : ℕ) < (s.length - 1).succ :=
  by
  conv_rhs => rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
  exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [top, s.inj, Fin.ext_iff] using hx)
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ ↑i < Nat.succ (s.length - 1)
[PROOFSTEP]
conv_rhs => rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
| Nat.succ (s.length - 1)
[PROOFSTEP]
rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
| Nat.succ (s.length - 1)
[PROOFSTEP]
rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
| Nat.succ (s.length - 1)
[PROOFSTEP]
rw [← Nat.succ_sub (length_pos_of_mem_ne ⟨i, rfl⟩ s.top_mem hx), Nat.succ_sub_one]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ ↑i < s.length
[PROOFSTEP]
exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [top, s.inj, Fin.ext_iff] using hx)
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
⊢ ↑i ≠ s.length
[PROOFSTEP]
simpa [top, s.inj, Fin.ext_iff] using hx
[GOAL]
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
hi : ↑i < Nat.succ (s.length - 1)
⊢ series s i ∈ eraseTop s
[PROOFSTEP]
refine' ⟨Fin.castSucc (n := s.length + 1) i, _⟩
[GOAL]
case intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : series s i ≠ top s
hi : ↑i < Nat.succ (s.length - 1)
⊢ series (eraseTop s) ↑↑(Fin.castSucc i) = series s i
[PROOFSTEP]
simp [Fin.ext_iff, Nat.mod_eq_of_lt hi]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ eraseTop s ↔ x ≠ top s ∧ x ∈ s
[PROOFSTEP]
simp only [mem_def]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ range (eraseTop s).series ↔ x ≠ top s ∧ x ∈ range s.series
[PROOFSTEP]
dsimp only [eraseTop]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) ↔ x ≠ top s ∧ x ∈ range s.series
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) → x ≠ top s ∧ x ∈ range s.series
[PROOFSTEP]
rintro ⟨i, rfl⟩
[GOAL]
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ≠ top s ∧
    (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ∈ range s.series
[PROOFSTEP]
have hi : (i : ℕ) < s.length :=
  by
  conv_rhs => rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
  exact
    i.2
      -- Porting note: Was `simp [top, Fin.ext_iff, ne_of_lt hi]`.
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < s.length
[PROOFSTEP]
conv_rhs => rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
| s.length
[PROOFSTEP]
rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
| s.length
[PROOFSTEP]
rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
| s.length
[PROOFSTEP]
rw [← Nat.succ_sub_one s.length, Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
⊢ ↑i < Nat.succ (s.length - Nat.succ 0)
[PROOFSTEP]
exact
  i.2
    -- Porting note: Was `simp [top, Fin.ext_iff, ne_of_lt hi]`.
[GOAL]
case mp.intro
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
i : Fin (s.length - 1 + 1)
hi : ↑i < s.length
⊢ (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ≠ top s ∧
    (fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }) i ∈ range s.series
[PROOFSTEP]
simp [top, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]
[GOAL]
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ≠ top s ∧ x ∈ range s.series → x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }
[PROOFSTEP]
intro h
[GOAL]
case mpr
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h✝ : 0 < s.length
h : x ≠ top s ∧ x ∈ range s.series
⊢ x ∈ range fun i => series s { val := ↑i, isLt := (_ : ↑i < s.length + 1) }
[PROOFSTEP]
exact mem_eraseTop_of_ne_of_mem h.1 h.2
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ IsMaximal (top (eraseTop s)) (top s)
[PROOFSTEP]
have : s.length - 1 + 1 = s.length := by conv_rhs => rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s.length - 1 + 1 = s.length
[PROOFSTEP]
conv_rhs => rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
| s.length
[PROOFSTEP]
rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
| s.length
[PROOFSTEP]
rw [← Nat.succ_sub_one s.length]; rw [Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
| s.length
[PROOFSTEP]
rw [← Nat.succ_sub_one s.length]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
| Nat.succ s.length - 1
[PROOFSTEP]
rw [Nat.succ_sub h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (top (eraseTop s)) (top s)
[PROOFSTEP]
rw [top_eraseTop, top]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ IsMaximal (series s { val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }) (series s (Fin.last s.length))
[PROOFSTEP]
convert s.step ⟨s.length - 1, Nat.sub_lt h zero_lt_one⟩
[GOAL]
case h.e'_5.h.e'_5
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ Fin.last s.length = Fin.succ { val := s.length - 1, isLt := (_ : s.length - 1 < s.length) }
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h.e'_5.h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
this : s.length - 1 + 1 = s.length
⊢ ↑(Fin.last s.length) = ↑(Fin.succ { val := s.length - 1, isLt := (_ : s.length - 1 < s.length) })
[PROOFSTEP]
simp [this]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : Fin m
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.castSucc (Fin.castAdd n i)) =
    a (Fin.castSucc i)
[PROOFSTEP]
cases i
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
val✝ : ℕ
isLt✝ : val✝ < m
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b
      (Fin.castSucc (Fin.castAdd n { val := val✝, isLt := isLt✝ })) =
    a (Fin.castSucc { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
simp [Matrix.vecAppend_eq_ite, *]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : Fin m
h : a (Fin.last m) = b 0
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.succ (Fin.castAdd n i)) =
    a (Fin.succ i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b
      (Fin.succ (Fin.castAdd n { val := i, isLt := hi })) =
    a (Fin.succ { val := i, isLt := hi })
[PROOFSTEP]
simp only [Matrix.vecAppend_eq_ite, hi, Fin.succ_mk, Function.comp_apply, Fin.castSucc_mk, Fin.val_mk, Fin.castAdd_mk]
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
⊢ (if h : i + 1 < m then a { val := i + 1, isLt := (_ : i + 1 < Nat.succ m) }
    else
      b
        { val := i + 1 - m,
          isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) }) =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
[PROOFSTEP]
split_ifs with h_1
[GOAL]
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : i + 1 < m
⊢ a { val := i + 1, isLt := (_ : i + 1 < Nat.succ m) } = a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
[PROOFSTEP]
rfl
[GOAL]
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
⊢ b
      { val := i + 1 - m,
        isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) } =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
[PROOFSTEP]
have : i + 1 = m := le_antisymm hi (le_of_not_gt h_1)
[GOAL]
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ b
      { val := i + 1 - m,
        isLt := (_ : ↑{ val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (m + n)) } - m < Nat.succ n) } =
    a { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
[PROOFSTEP]
calc
  b ⟨i + 1 - m, by simp [this]⟩ = b 0 := congr_arg b (by simp [Fin.ext_iff, this])
  _ = a (Fin.last _) := h.symm
  _ = _ := congr_arg a (by simp [Fin.ext_iff, this])
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ i + 1 - m < Nat.succ n
[PROOFSTEP]
simp [this]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ { val := i + 1 - m, isLt := (_ : i + 1 - m < Nat.succ n) } = 0
[PROOFSTEP]
simp [Fin.ext_iff, this]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
h : a (Fin.last m) = b 0
i : ℕ
hi : i < m
h_1 : ¬i + 1 < m
this : i + 1 = m
⊢ Fin.last m = { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ m) }
[PROOFSTEP]
simp [Fin.ext_iff, this]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : Fin n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.castSucc (Fin.natAdd m i)) =
    b (Fin.castSucc i)
[PROOFSTEP]
cases i
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
val✝ : ℕ
isLt✝ : val✝ < n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b
      (Fin.castSucc (Fin.natAdd m { val := val✝, isLt := isLt✝ })) =
    b (Fin.castSucc { val := val✝, isLt := isLt✝ })
[PROOFSTEP]
simp only [Matrix.vecAppend_eq_ite, Nat.not_lt_zero, Fin.natAdd_mk, add_lt_iff_neg_left, add_tsub_cancel_left, dif_neg,
  Fin.castSucc_mk, not_false_iff, Fin.val_mk]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : Fin n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b (Fin.succ (Fin.natAdd m i)) =
    b (Fin.succ i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
α : Type u_1
m n : ℕ
a : Fin (Nat.succ m) → α
b : Fin (Nat.succ n) → α
i : ℕ
hi : i < n
⊢ Matrix.vecAppend (_ : Nat.succ (m + n) = m + Nat.succ n) (a ∘ Fin.castSucc) b
      (Fin.succ (Fin.natAdd m { val := i, isLt := hi })) =
    b (Fin.succ { val := i, isLt := hi })
[PROOFSTEP]
simp only [Matrix.vecAppend_eq_ite, add_assoc, Nat.not_lt_zero, Fin.natAdd_mk, add_lt_iff_neg_left,
  add_tsub_cancel_left, Fin.succ_mk, dif_neg, not_false_iff, Fin.val_mk]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin (s₁.length + s₂.length)
⊢ IsMaximal
    (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length) (s₁.series ∘ Fin.castSucc)
      s₂.series (Fin.castSucc i))
    (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length) (s₁.series ∘ Fin.castSucc)
      s₂.series (Fin.succ i))
[PROOFSTEP]
refine' Fin.addCases _ _ i
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin (s₁.length + s₂.length)
⊢ ∀ (i : Fin s₁.length),
    IsMaximal
      (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length)
        (s₁.series ∘ Fin.castSucc) s₂.series (Fin.castSucc (Fin.castAdd s₂.length i)))
      (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length)
        (s₁.series ∘ Fin.castSucc) s₂.series (Fin.succ (Fin.castAdd s₂.length i)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i✝ : Fin (s₁.length + s₂.length)
i : Fin s₁.length
⊢ IsMaximal
    (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length) (s₁.series ∘ Fin.castSucc)
      s₂.series (Fin.castSucc (Fin.castAdd s₂.length i)))
    (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length) (s₁.series ∘ Fin.castSucc)
      s₂.series (Fin.succ (Fin.castAdd s₂.length i)))
[PROOFSTEP]
rw [append_succ_castAdd_aux _ _ _ h, append_castAdd_aux]
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i✝ : Fin (s₁.length + s₂.length)
i : Fin s₁.length
⊢ IsMaximal (series s₁ (Fin.castSucc i)) (series s₁ (Fin.succ i))
[PROOFSTEP]
exact s₁.step i
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin (s₁.length + s₂.length)
⊢ ∀ (i : Fin s₂.length),
    IsMaximal
      (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length)
        (s₁.series ∘ Fin.castSucc) s₂.series (Fin.castSucc (Fin.natAdd s₁.length i)))
      (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length)
        (s₁.series ∘ Fin.castSucc) s₂.series (Fin.succ (Fin.natAdd s₁.length i)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i✝ : Fin (s₁.length + s₂.length)
i : Fin s₂.length
⊢ IsMaximal
    (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length) (s₁.series ∘ Fin.castSucc)
      s₂.series (Fin.castSucc (Fin.natAdd s₁.length i)))
    (Matrix.vecAppend (_ : Nat.succ (s₁.length + s₂.length) = s₁.length + Nat.succ s₂.length) (s₁.series ∘ Fin.castSucc)
      s₂.series (Fin.succ (Fin.natAdd s₁.length i)))
[PROOFSTEP]
rw [append_natAdd_aux, append_succ_natAdd_aux]
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i✝ : Fin (s₁.length + s₂.length)
i : Fin s₂.length
⊢ IsMaximal (series s₂ (Fin.castSucc i)) (series s₂ (Fin.succ i))
[PROOFSTEP]
exact s₂.step i
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin s₁.length
⊢ series (append s₁ s₂ h) (Fin.castSucc (Fin.castAdd s₂.length i)) = series s₁ (Fin.castSucc i)
[PROOFSTEP]
rw [coe_append, append_castAdd_aux _ _ i]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin s₁.length
⊢ series (append s₁ s₂ h) (Fin.succ (Fin.castAdd s₂.length i)) = series s₁ (Fin.succ i)
[PROOFSTEP]
rw [coe_append, append_succ_castAdd_aux _ _ _ h]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin s₂.length
⊢ series (append s₁ s₂ h) (Fin.castSucc (Fin.natAdd s₁.length i)) = series s₂ (Fin.castSucc i)
[PROOFSTEP]
rw [coe_append, append_natAdd_aux _ _ i]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin s₂.length
⊢ series (append s₁ s₂ h) (Fin.succ (Fin.natAdd s₁.length i)) = series s₂ (Fin.succ i)
[PROOFSTEP]
rw [coe_append, append_succ_natAdd_aux _ _ i]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
i : Fin (s.length + 1)
⊢ IsMaximal (Fin.snoc s.series x (Fin.castSucc i)) (Fin.snoc s.series x (Fin.succ i))
[PROOFSTEP]
refine' Fin.lastCases _ _ i
[GOAL]
case 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)
⊢ IsMaximal (Fin.snoc s.series x (Fin.castSucc (Fin.last s.length)))
    (Fin.snoc s.series x (Fin.succ (Fin.last s.length)))
[PROOFSTEP]
rwa [Fin.snoc_castSucc, Fin.succ_last, Fin.snoc_last, ← top]
[GOAL]
case 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)
⊢ ∀ (i : Fin s.length),
    IsMaximal (Fin.snoc s.series x (Fin.castSucc (Fin.castSucc i))) (Fin.snoc s.series x (Fin.succ (Fin.castSucc i)))
[PROOFSTEP]
intro i
[GOAL]
case 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)
i : Fin s.length
⊢ IsMaximal (Fin.snoc s.series x (Fin.castSucc (Fin.castSucc i))) (Fin.snoc s.series x (Fin.succ (Fin.castSucc i)))
[PROOFSTEP]
rw [Fin.snoc_castSucc, ← Fin.castSucc_fin_succ, Fin.snoc_castSucc]
[GOAL]
case 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)
i : Fin s.length
⊢ IsMaximal (series s (Fin.castSucc i)) (series s (Fin.succ i))
[PROOFSTEP]
exact s.step _
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
⊢ bot (snoc s x hsat) = bot s
[PROOFSTEP]
rw [bot, bot, ← snoc_castSucc s x hsat 0, Fin.castSucc_zero' (n := s.length + 1)]
[GOAL]
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
[PROOFSTEP]
simp only [snoc, mem_def]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro ⟨i, rfl⟩
[GOAL]
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
[PROOFSTEP]
refine' Fin.lastCases _ (fun i => _) i
[GOAL]
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
[PROOFSTEP]
right
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
left
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
intro h
[GOAL]
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)
[PROOFSTEP]
rcases h with (⟨i, rfl⟩ | rfl)
[GOAL]
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)
[PROOFSTEP]
use Fin.castSucc i
[GOAL]
case 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)
⊢ Fin.snoc s.series x (Fin.castSucc i) = series s i
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
use Fin.last _
[GOAL]
case h
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
[PROOFSTEP]
simp
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
⊢ s = snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s))
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ x ∈ snoc (eraseTop s) (top s) (_ : IsMaximal (top (eraseTop s)) (top s))
[PROOFSTEP]
simp [mem_snoc, mem_eraseTop h]
[GOAL]
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : 0 < s.length
x : X
⊢ x ∈ s ↔ ¬x = top s ∧ x ∈ s ∨ x = top s
[PROOFSTEP]
by_cases h : x = s.top
[GOAL]
case pos
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h✝ : 0 < s.length
x : X
h : x = top s
⊢ x ∈ s ↔ ¬x = top s ∧ x ∈ s ∨ x = top s
[PROOFSTEP]
simp [*, s.top_mem]
[GOAL]
case neg
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h✝ : 0 < s.length
x : X
h : ¬x = top s
⊢ x ∈ s ↔ ¬x = top s ∧ x ∈ s ∨ x = top s
[PROOFSTEP]
simp [*, s.top_mem]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
⊢ s.length ≠ 0
[PROOFSTEP]
intro hs
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
hs : s.length = 0
⊢ False
[PROOFSTEP]
refine' ne_of_gt (lt_of_isMaximal h) _
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
h : IsMaximal (top (eraseTop s)) (top s)
hs : s.length = 0
⊢ top s = top (eraseTop s)
[PROOFSTEP]
simp [top, Fin.ext_iff, hs]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : Equivalent s₁ s₂
i : Fin s₂.length
⊢ Iso (series s₁ (Fin.castSucc (↑(Exists.choose h).symm i)), series s₁ (Fin.succ (↑(Exists.choose h).symm i)))
    (series s₂ (Fin.castSucc i), series s₂ (Fin.succ i))
[PROOFSTEP]
simpa using h.choose_spec (h.choose.symm i)
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : top s₁ = bot s₂
ht : top t₁ = bot t₂
h₁ : Equivalent s₁ t₁
h₂ : Equivalent s₂ t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm (Equiv.sumCongr (Exists.choose h₁) (Exists.choose h₂))) finSumFinEquiv
⊢ ∀ (i : Fin (CompositionSeries.append s₁ s₂ hs).length),
    Iso
      (series (CompositionSeries.append s₁ s₂ hs) (Fin.castSucc i),
        series (CompositionSeries.append s₁ s₂ hs) (Fin.succ i))
      (series (CompositionSeries.append t₁ t₂ ht) (Fin.castSucc (↑e i)),
        series (CompositionSeries.append t₁ t₂ ht) (Fin.succ (↑e i)))
[PROOFSTEP]
intro i
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : top s₁ = bot s₂
ht : top t₁ = bot t₂
h₁ : Equivalent s₁ t₁
h₂ : Equivalent s₂ t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm (Equiv.sumCongr (Exists.choose h₁) (Exists.choose h₂))) finSumFinEquiv
i : Fin (CompositionSeries.append s₁ s₂ hs).length
⊢ Iso
    (series (CompositionSeries.append s₁ s₂ hs) (Fin.castSucc i),
      series (CompositionSeries.append s₁ s₂ hs) (Fin.succ i))
    (series (CompositionSeries.append t₁ t₂ ht) (Fin.castSucc (↑e i)),
      series (CompositionSeries.append t₁ t₂ ht) (Fin.succ (↑e i)))
[PROOFSTEP]
refine' Fin.addCases _ _ i
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : top s₁ = bot s₂
ht : top t₁ = bot t₂
h₁ : Equivalent s₁ t₁
h₂ : Equivalent s₂ t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm (Equiv.sumCongr (Exists.choose h₁) (Exists.choose h₂))) finSumFinEquiv
i : Fin (CompositionSeries.append s₁ s₂ hs).length
⊢ ∀ (i : Fin s₁.length),
    Iso
      (series (CompositionSeries.append s₁ s₂ hs) (Fin.castSucc (Fin.castAdd s₂.length i)),
        series (CompositionSeries.append s₁ s₂ hs) (Fin.succ (Fin.castAdd s₂.length i)))
      (series (CompositionSeries.append t₁ t₂ ht) (Fin.castSucc (↑e (Fin.castAdd s₂.length i))),
        series (CompositionSeries.append t₁ t₂ ht) (Fin.succ (↑e (Fin.castAdd s₂.length i))))
[PROOFSTEP]
intro i
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : top s₁ = bot s₂
ht : top t₁ = bot t₂
h₁ : Equivalent s₁ t₁
h₂ : Equivalent s₂ t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm (Equiv.sumCongr (Exists.choose h₁) (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (CompositionSeries.append s₁ s₂ hs).length
i : Fin s₁.length
⊢ Iso
    (series (CompositionSeries.append s₁ s₂ hs) (Fin.castSucc (Fin.castAdd s₂.length i)),
      series (CompositionSeries.append s₁ s₂ hs) (Fin.succ (Fin.castAdd s₂.length i)))
    (series (CompositionSeries.append t₁ t₂ ht) (Fin.castSucc (↑e (Fin.castAdd s₂.length i))),
      series (CompositionSeries.append t₁ t₂ ht) (Fin.succ (↑e (Fin.castAdd s₂.length i))))
[PROOFSTEP]
simpa [top, bot] using h₁.choose_spec i
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : top s₁ = bot s₂
ht : top t₁ = bot t₂
h₁ : Equivalent s₁ t₁
h₂ : Equivalent s₂ t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm (Equiv.sumCongr (Exists.choose h₁) (Exists.choose h₂))) finSumFinEquiv
i : Fin (CompositionSeries.append s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso
      (series (CompositionSeries.append s₁ s₂ hs) (Fin.castSucc (Fin.natAdd s₁.length i)),
        series (CompositionSeries.append s₁ s₂ hs) (Fin.succ (Fin.natAdd s₁.length i)))
      (series (CompositionSeries.append t₁ t₂ ht) (Fin.castSucc (↑e (Fin.natAdd s₁.length i))),
        series (CompositionSeries.append t₁ t₂ ht) (Fin.succ (↑e (Fin.natAdd s₁.length i))))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : top s₁ = bot s₂
ht : top t₁ = bot t₂
h₁ : Equivalent s₁ t₁
h₂ : Equivalent s₂ t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm (Equiv.sumCongr (Exists.choose h₁) (Exists.choose h₂))) finSumFinEquiv
i✝ : Fin (CompositionSeries.append s₁ s₂ hs).length
i : Fin s₂.length
⊢ Iso
    (series (CompositionSeries.append s₁ s₂ hs) (Fin.castSucc (Fin.natAdd s₁.length i)),
      series (CompositionSeries.append s₁ s₂ hs) (Fin.succ (Fin.natAdd s₁.length i)))
    (series (CompositionSeries.append t₁ t₂ ht) (Fin.castSucc (↑e (Fin.natAdd s₁.length i))),
      series (CompositionSeries.append t₁ t₂ ht) (Fin.succ (↑e (Fin.natAdd s₁.length i))))
[PROOFSTEP]
simpa [top, bot] using h₂.choose_spec i
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (top s₁) x₁
hsat₂ : IsMaximal (top s₂) x₂
hequiv : Equivalent s₁ s₂
htop : Iso (top s₁, x₁) (top s₂, x₂)
e : Fin (Nat.succ s₁.length) ≃ Fin (Nat.succ s₂.length) :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso (series (snoc s₁ x₁ hsat₁) (Fin.castSucc i), series (snoc s₁ x₁ hsat₁) (Fin.succ i))
    (series (snoc s₂ x₂ hsat₂) (Fin.castSucc (↑e i)), series (snoc s₂ x₂ hsat₂) (Fin.succ (↑e i)))
[PROOFSTEP]
refine' Fin.lastCases _ _ i
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (top s₁) x₁
hsat₂ : IsMaximal (top s₂) x₂
hequiv : Equivalent s₁ s₂
htop : Iso (top s₁, x₁) (top s₂, x₂)
e : Fin (Nat.succ s₁.length) ≃ Fin (Nat.succ s₂.length) :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso
    (series (snoc s₁ x₁ hsat₁) (Fin.castSucc (Fin.last s₁.length)),
      series (snoc s₁ x₁ hsat₁) (Fin.succ (Fin.last s₁.length)))
    (series (snoc s₂ x₂ hsat₂) (Fin.castSucc (↑e (Fin.last s₁.length))),
      series (snoc s₂ x₂ hsat₂) (Fin.succ (↑e (Fin.last s₁.length))))
[PROOFSTEP]
simpa [top] using htop
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (top s₁) x₁
hsat₂ : IsMaximal (top s₂) x₂
hequiv : Equivalent s₁ s₂
htop : Iso (top s₁, x₁) (top s₂, x₂)
e : Fin (Nat.succ s₁.length) ≃ Fin (Nat.succ s₂.length) :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ ∀ (i : Fin s₁.length),
    Iso
      (series (snoc s₁ x₁ hsat₁) (Fin.castSucc (Fin.castSucc i)), series (snoc s₁ x₁ hsat₁) (Fin.succ (Fin.castSucc i)))
      (series (snoc s₂ x₂ hsat₂) (Fin.castSucc (↑e (Fin.castSucc i))),
        series (snoc s₂ x₂ hsat₂) (Fin.succ (↑e (Fin.castSucc i))))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (top s₁) x₁
hsat₂ : IsMaximal (top s₂) x₂
hequiv : Equivalent s₁ s₂
htop : Iso (top s₁, x₁) (top s₂, x₂)
e : Fin (Nat.succ s₁.length) ≃ Fin (Nat.succ s₂.length) :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i✝ : Fin (snoc s₁ x₁ hsat₁).length
i : Fin s₁.length
⊢ Iso (series (snoc s₁ x₁ hsat₁) (Fin.castSucc (Fin.castSucc i)), series (snoc s₁ x₁ hsat₁) (Fin.succ (Fin.castSucc i)))
    (series (snoc s₂ x₂ hsat₂) (Fin.castSucc (↑e (Fin.castSucc i))),
      series (snoc s₂ x₂ hsat₂) (Fin.succ (↑e (Fin.castSucc i))))
[PROOFSTEP]
simpa [Fin.succ_castSucc] using hequiv.choose_spec i
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : Equivalent s₁ s₂
⊢ s₁.length = s₂.length
[PROOFSTEP]
simpa using Fintype.card_congr h.choose
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
x✝ : Fin s.length
⊢ Fin.castSucc (Fin.castSucc x✝) < Fin.castSucc (Fin.last s.length)
[PROOFSTEP]
simp [Fin.castSucc_lt_last]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
x✝ : Fin s.length
⊢ Fin.castSucc (Fin.castSucc x✝) < Fin.last (s.length + 1)
[PROOFSTEP]
simp [Fin.castSucc_lt_last]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
⊢ ∀ (i : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length),
    Iso
      (series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.castSucc i),
        series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.succ i))
      (series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂) (Fin.castSucc (↑e i)),
        series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂) (Fin.succ (↑e i)))
[PROOFSTEP]
intro i
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
⊢ Iso
    (series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.castSucc i), series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.succ i))
    (series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂) (Fin.castSucc (↑e i)),
      series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂) (Fin.succ (↑e i)))
[PROOFSTEP]
dsimp only []
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
⊢ Iso
    (series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.castSucc i), series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.succ i))
    (series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.castSucc (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))) i)),
      series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.succ (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))) i)))
[PROOFSTEP]
refine' Fin.lastCases _ (fun i => _) i
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
⊢ Iso
    (series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.castSucc (Fin.last (snoc s x₁ hsat₁).length)),
      series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.succ (Fin.last (snoc s x₁ hsat₁).length)))
    (series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.castSucc
          (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length)))
            (Fin.last (snoc s x₁ hsat₁).length))),
      series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.succ
          (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length)))
            (Fin.last (snoc s x₁ hsat₁).length))))
[PROOFSTEP]
erw [Equiv.swap_apply_left, snoc_castSucc, snoc_last, Fin.succ_last, snoc_last, snoc_castSucc, snoc_castSucc,
  Fin.succ_castSucc, snoc_castSucc, Fin.succ_last, snoc_last]
[GOAL]
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
⊢ Iso (x₁, y₁) (series s (Fin.last s.length), x₂)
[PROOFSTEP]
exact hr₂
[GOAL]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i✝ : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
i : Fin (snoc s x₁ hsat₁).length
⊢ Iso
    (series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.castSucc (Fin.castSucc i)),
      series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.succ (Fin.castSucc i)))
    (series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.castSucc (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))) (Fin.castSucc i))),
      series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.succ (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))) (Fin.castSucc i))))
[PROOFSTEP]
refine' Fin.lastCases _ (fun i => _) i
[GOAL]
case refine'_2.refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i✝ : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
i : Fin (snoc s x₁ hsat₁).length
⊢ Iso
    (series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.castSucc (Fin.castSucc (Fin.last s.length))),
      series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.succ (Fin.castSucc (Fin.last s.length))))
    (series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.castSucc
          (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length)))
            (Fin.castSucc (Fin.last s.length)))),
      series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.succ
          (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length)))
            (Fin.castSucc (Fin.last s.length)))))
[PROOFSTEP]
erw [Equiv.swap_apply_right, snoc_castSucc, snoc_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc,
  Fin.succ_last, snoc_last, snoc_last, Fin.succ_last, snoc_last]
[GOAL]
case refine'_2.refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i✝ : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
i : Fin (snoc s x₁ hsat₁).length
⊢ Iso (series s (Fin.last s.length), x₁) (x₂, y₂)
[PROOFSTEP]
exact hr₁
[GOAL]
case refine'_2.refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i✝¹ : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
i✝ : Fin (snoc s x₁ hsat₁).length
i : Fin s.length
⊢ Iso
    (series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.castSucc (Fin.castSucc (Fin.castSucc i))),
      series (snoc (snoc s x₁ hsat₁) y₁ hsaty₁) (Fin.succ (Fin.castSucc (Fin.castSucc i))))
    (series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.castSucc
          (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))) (Fin.castSucc (Fin.castSucc i)))),
      series (snoc (snoc s x₂ hsat₂) y₂ hsaty₂)
        (Fin.succ
          (↑(Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))) (Fin.castSucc (Fin.castSucc i)))))
[PROOFSTEP]
erw [Equiv.swap_apply_of_ne_of_ne h2 h1, snoc_castSucc, snoc_castSucc, snoc_castSucc, snoc_castSucc, Fin.succ_castSucc,
  snoc_castSucc, Fin.succ_castSucc, snoc_castSucc, snoc_castSucc, snoc_castSucc]
[GOAL]
case refine'_2.refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (top s) x₁
hsat₂ : IsMaximal (top s) x₂
hsaty₁ : IsMaximal (top (snoc s x₁ hsat₁)) y₁
hsaty₂ : IsMaximal (top (snoc s x₂ hsat₂)) y₂
hr₁ : Iso (top s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (top s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) :=
  Equiv.swap (Fin.last (s.length + 1)) (Fin.castSucc (Fin.last s.length))
h1 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.castSucc (Fin.last s.length)
h2 : ∀ {i : Fin s.length}, Fin.castSucc (Fin.castSucc i) ≠ Fin.last (s.length + 1)
i✝¹ : Fin (snoc (snoc s x₁ hsat₁) y₁ hsaty₁).length
i✝ : Fin (snoc s x₁ hsat₁).length
i : Fin s.length
⊢ Iso (series s (Fin.castSucc i), series s (Fin.succ i)) (series s (Fin.castSucc i), series s (Fin.succ i))
[PROOFSTEP]
exact (s.step i).iso_refl
[GOAL]
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
[PROOFSTEP]
have : s₁.bot = s₁.top := congr_arg s₁ (Fin.ext (by simp [hs₁]))
[GOAL]
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)
[PROOFSTEP]
simp [hs₁]
[GOAL]
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
[PROOFSTEP]
have : Fin.last s₂.length = (0 : Fin s₂.length.succ) := s₂.injective (hb.symm.trans (this.trans ht)).symm
[GOAL]
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
[PROOFSTEP]
rw [Fin.ext_iff] at this
[GOAL]
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
[PROOFSTEP]
simpa
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
⊢ ¬0 < s₂.length → ¬0 < s₁.length
[PROOFSTEP]
simp only [pos_iff_ne_zero, Ne.def, not_iff_not, Classical.not_not]
[GOAL]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
⊢ s₂.length = 0 → s₁.length = 0
[PROOFSTEP]
exact length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb.symm ht.symm
[GOAL]
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₂
[PROOFSTEP]
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⟩
[GOAL]
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₂
[PROOFSTEP]
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⟩
[GOAL]
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₂
[PROOFSTEP]
ext
[GOAL]
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₂
[PROOFSTEP]
simp [*]
[GOAL]
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)))
[PROOFSTEP]
induction' hn : s.length with n ih generalizing s x
[GOAL]
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)))
[PROOFSTEP]
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
[GOAL]
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)))
[PROOFSTEP]
have h0s : 0 < s.length := hn.symm ▸ Nat.succ_pos _
[GOAL]
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)))
[PROOFSTEP]
by_cases hetx : s.eraseTop.top = x
[GOAL]
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)))
[PROOFSTEP]
use s.eraseTop
[GOAL]
case h
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)))
[PROOFSTEP]
simp [← hetx, hn]
  -- Porting note: `rfl` is required.
[GOAL]
case h
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
[PROOFSTEP]
rfl
[GOAL]
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)))
[PROOFSTEP]
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)
[GOAL]
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)))
[PROOFSTEP]
have := ih _ _ imxs (le_inf (by simpa) (le_top_of_mem s.eraseTop.bot_mem)) (by simp [hn])
[GOAL]
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
[PROOFSTEP]
simpa
[GOAL]
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
[PROOFSTEP]
simp [hn]
[GOAL]
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)))
[PROOFSTEP]
rcases this with ⟨t, htb, htl, htt, hteqv⟩
[GOAL]
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)))
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
rw [inf_comm, htt]
[GOAL]
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)))
[PROOFSTEP]
use snoc t x hmtx
[GOAL]
case h
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)))
[PROOFSTEP]
refine' ⟨by simp [htb], by simp [htl], by simp, _⟩
[GOAL]
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
[PROOFSTEP]
simp [htb]
[GOAL]
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
[PROOFSTEP]
simp [htl]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
case h
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)))
[PROOFSTEP]
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)
[GOAL]
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)
[PROOFSTEP]
simpa using isMaximal_eraseTop_top h0s
[GOAL]
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)))
[PROOFSTEP]
conv_lhs => rw [eq_snoc_eraseTop h0s]
[GOAL]
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
| s
[PROOFSTEP]
rw [eq_snoc_eraseTop h0s]
[GOAL]
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
| s
[PROOFSTEP]
rw [eq_snoc_eraseTop h0s]
[GOAL]
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
| s
[PROOFSTEP]
rw [eq_snoc_eraseTop h0s]
[GOAL]
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)))
[PROOFSTEP]
exact Equivalent.snoc hteqv (by simpa using (isMaximal_eraseTop_top h0s).iso_refl)
[GOAL]
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)
[PROOFSTEP]
simpa using (isMaximal_eraseTop_top h0s).iso_refl
[GOAL]
case h
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)))
[PROOFSTEP]
refine' this.trans _
[GOAL]
case h
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)))
[PROOFSTEP]
refine' Equivalent.snoc_snoc_swap _ _
[GOAL]
case h.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)
[PROOFSTEP]
exact iso_symm (second_iso_of_eq hm (sup_eq_of_isMaximal hm (isMaximal_eraseTop_top h0s) (Ne.symm hetx)) htt.symm)
[GOAL]
case h.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)
[PROOFSTEP]
exact
  second_iso_of_eq (isMaximal_eraseTop_top h0s) (sup_eq_of_isMaximal (isMaximal_eraseTop_top h0s) hm hetx)
    (by rw [inf_comm, htt])
[GOAL]
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
[PROOFSTEP]
rw [inf_comm, htt]
[GOAL]
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₂
[PROOFSTEP]
induction' hle : s₁.length with n ih generalizing s₁ s₂
[GOAL]
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₂
[PROOFSTEP]
rw [eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb ht hle]
[GOAL]
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₂
[PROOFSTEP]
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 _)
[GOAL]
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₂
[PROOFSTEP]
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⟩
[GOAL]
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₂
[PROOFSTEP]
have := ih t s₂.eraseTop (by simp [htb, ← hb]) htt (Nat.succ_inj'.1 (htl.trans hle))
[GOAL]
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₂)
[PROOFSTEP]
simp [htb, ← hb]
[GOAL]
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₂
[PROOFSTEP]
refine' hteq.trans _
[GOAL]
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₂
[PROOFSTEP]
conv_rhs => rw [eq_snoc_eraseTop h0s₂]
[GOAL]
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₂)
| s₂
[PROOFSTEP]
rw [eq_snoc_eraseTop h0s₂]
[GOAL]
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₂)
| s₂
[PROOFSTEP]
rw [eq_snoc_eraseTop h0s₂]
[GOAL]
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₂)
| s₂
[PROOFSTEP]
rw [eq_snoc_eraseTop h0s₂]
[GOAL]
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₂)))
[PROOFSTEP]
simp only [ht]
[GOAL]
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₂)))
[PROOFSTEP]
exact Equivalent.snoc this (by simp [htt, (isMaximal_eraseTop_top h0s₂).iso_refl])
[GOAL]
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₂)
[PROOFSTEP]
simp [htt, (isMaximal_eraseTop_top h0s₂).iso_refl]