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))))

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))))
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)))
refine' Fin.lastCases _ _ i
no goals
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))))
simpa [top] using htop
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))))
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))))
intro i
no goals
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))))
simpa [Fin.succ_castSucc] using hequiv.choose_spec i