-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ :
  @IsMaximal _ inst _
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁)
    x₁
hsat₂ :
  @IsMaximal _ inst _
    (last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂)
    x₂
hequiv : s₁.Equivalent s₂
hlast :
  @Iso _ inst _
    (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s₁,
      x₁)
    (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s₂,
      x₂)
e : Fin
    s₁.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}).succ ≃
  Fin
    s₂.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}).succ :=
  Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
    (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) finSuccEquivLast
      (Functor.mapEquiv Option
        (Exists.choose (p :=
          fun
            (f :
              Fin
                  (s₁.length (r :=
                    {x : X × X |
                      match (motive := X × X → Prop) x with
                      | (x, y) => @IsMaximal _ inst _ x y})) ≃
                Fin
                  (s₂.length (r :=
                    {x : X × X |
                      match (motive := X × X → Prop) x with
                      | (x, y) => @IsMaximal _ inst _ x y}))) ↦
          ∀
            (i :
              Fin
                (s₁.length (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y}))),
            @Iso _ inst _
              (s₁.toFun (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  i.castSucc,
                s₁.toFun (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  i.succ)
              (s₂.toFun (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  (Fin.castSucc ((f : (a : Fin s₁.length) → Fin s₂.length) i)),
                s₂.toFun (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  (Fin.succ ((f : (a : Fin s₁.length) → Fin s₂.length) i))))
          hequiv)))
    (Equiv.symm finSuccEquivLast)
i :
  Fin
    ((snoc (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁ x₁ hsat₁).length
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
refine_1 :
  @Iso _ inst _
    ((snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₁ x₁ hsat₁).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.castSucc
          (Fin.last
            (s₁.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}) +
              length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                (RelSeries.singleton
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y}
                  x₁)))),
      (snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₁ x₁ hsat₁).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.succ
          (Fin.last
            (s₁.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}) +
              length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y})
                (RelSeries.singleton
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y}
                  x₁)))))
    ((snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₂ x₂ hsat₂).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.castSucc
          ((e : (a : Fin (snoc s₁ x₁ hsat₁).length) → Fin (snoc s₂ x₂ hsat₂).length)
            (Fin.last
              (s₁.length (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y}) +
                length (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  (RelSeries.singleton
                    {x : X × X |
                      match (motive := X × X → Prop) x with
                      | (x, y) => @IsMaximal _ inst _ x y}
                    x₁))))),
      (snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₂ x₂ hsat₂).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.succ
          ((e : (a : Fin (snoc s₁ x₁ hsat₁).length) → Fin (snoc s₂ x₂ hsat₂).length)
            (Fin.last
              (s₁.length (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y}) +
                length (r :=
                  {x : X × X |
                    match (motive := X × X → Prop) x with
                    | (x, y) => @IsMaximal _ inst _ x y})
                  (RelSeries.singleton
                    {x : X × X |
                      match (motive := X × X → Prop) x with
                      | (x, y) => @IsMaximal _ inst _ x y}
                    x₁))))))
refine_2 :
  ∀
    (i :
      Fin
        (s₁.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}) +
          length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            (RelSeries.singleton
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}
              x₁))),
    @Iso _ inst _
      ((snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              s₁ x₁ hsat₁).toFun
          (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          i.castSucc.castSucc,
        (snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              s₁ x₁ hsat₁).toFun
          (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          i.castSucc.succ)
      ((snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              s₂ x₂ hsat₂).toFun
          (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          (Fin.castSucc ((e : (a : Fin (snoc s₁ x₁ hsat₁).length) → Fin (snoc s₂ x₂ hsat₂).length) i.castSucc)),
        (snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              s₂ x₂ hsat₂).toFun
          (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          (Fin.succ ((e : (a : Fin (snoc s₁ x₁ hsat₁).length) → Fin (snoc s₂ x₂ hsat₂).length) i.castSucc)))
⊢ @Iso _ inst _
    ((snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₁ x₁ hsat₁).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i.castSucc,
      (snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₁ x₁ hsat₁).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i.succ)
    ((snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₂ x₂ hsat₂).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.castSucc ((e : (a : Fin (snoc s₁ x₁ hsat₁).length) → Fin (snoc s₂ x₂ hsat₂).length) i)),
      (snoc (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₂ x₂ hsat₂).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.succ ((e : (a : Fin (snoc s₁ x₁ hsat₁).length) → Fin (snoc s₂ x₂ hsat₂).length) i)))

Tactic:
refine Fin.lastCases ?_ ?_ i