-- Mathlib/Order/JordanHolder.lean
theorem snoc {s₁ s₂ : CompositionSeries X} {x₁ x₂ : X} {hsat₁ : IsMaximal s₁.last x₁}
    {hsat₂ : IsMaximal s₂.last x₂} (hequiv : Equivalent s₁ s₂)
    (hlast : Iso (s₁.last, x₁) (s₂.last, x₂)) : Equivalent (s₁.snoc x₁ hsat₁) (s₂.snoc x₂ hsat₂) :=
  let e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
    calc
      Fin (s₁.length + 1) ≃ Option (Fin s₁.length) := finSuccEquivLast
      _ ≃ Option (Fin s₂.length) := Functor.mapEquiv Option hequiv.choose
      _ ≃ Fin (s₂.length + 1) := finSuccEquivLast.symm
  ⟨e, fun i => by
    refine Fin.lastCases ?_ ?_ i
    · simpa [e, apply_last] using hlast
    · intro i
      simpa [e, Fin.succ_castSucc] using hequiv.choose_spec i⟩

Proof state:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso
    ((snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length)).castSucc,
      (snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length)).succ)
    ((snoc s₂ x₂ hsat₂).toFun (e (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length))).castSucc,
      (snoc s₂ x₂ hsat₂).toFun (e (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length))).succ)

Tactic:
simpa [e, apply_last] using hlast

Result:
no goals

Proof state:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i✝ : Fin (snoc s₁ x₁ hsat₁).length
i : Fin (s₁.length + (RelSeries.singleton IsMaximal x₁).length)
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
    ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)

Tactic:
simpa [e, Fin.succ_castSucc] using hequiv.choose_spec i

Result:
no goals

Proof state:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ ∀ (i : Fin (s₁.length + (RelSeries.singleton IsMaximal x₁).length)),
    Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
      ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)

Tactic:
intro i

Result:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i✝ : Fin (snoc s₁ x₁ hsat₁).length
i : Fin (s₁.length + (RelSeries.singleton IsMaximal x₁).length)
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
    ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc, (snoc s₁ x₁ hsat₁).toFun i.succ)
    ((snoc s₂ x₂ hsat₂).toFun (e i).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i).succ)

Tactic:
refine Fin.lastCases ?_ ?_ i

Result:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso
    ((snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length)).castSucc,
      (snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length)).succ)
    ((snoc s₂ x₂ hsat₂).toFun (e (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length))).castSucc,
      (snoc s₂ x₂ hsat₂).toFun (e (Fin.last (s₁.length + (RelSeries.singleton IsMaximal x₁).length))).succ)

case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ ∀ (i : Fin (s₁.length + (RelSeries.singleton IsMaximal x₁).length)),
    Iso ((snoc s₁ x₁ hsat₁).toFun i.castSucc.castSucc, (snoc s₁ x₁ hsat₁).toFun i.castSucc.succ)
      ((snoc s₂ x₂ hsat₂).toFun (e i.castSucc).castSucc, (snoc s₂ x₂ hsat₂).toFun (e i.castSucc).succ)