-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : 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₂
hsaty₁ :
  @IsMaximal _ inst _
    ((snoc (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s x₁ hsat₁).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
    y₁
hsaty₂ :
  @IsMaximal _ inst _
    ((snoc (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s x₂ hsat₂).last
      (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y}))
    y₂
hr₁ :
  @Iso _ inst _
    (last (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        s,
      x₁)
    (x₂, y₂)
hr₂ :
  @Iso _ inst _ (x₁, y₁)
    (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}) +
        1 +
      1) ≃
  Fin
    (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1 +
      1) :=
  Equiv.swap
    (Fin.last
      (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1))
    (Fin.castSucc
      (Fin.last
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))))
h1 :
  ∀
    {i :
      Fin
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))},
    i.castSucc.castSucc ≠
      Fin.castSucc
        (Fin.last
          (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})))
h2 :
  ∀
    {i :
      Fin
        (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}))},
    i.castSucc.castSucc ≠
      Fin.last
        (s.length (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y}) +
          1)
i :
  Fin
    (((snoc (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y})
              s x₁ hsat₁).snoc
          (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          y₁ hsaty₁).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 | @IsMaximal _ inst _ x.1 x.2}) s x₁ hsat₁).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₁ hsaty₁).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
        (Fin.castSucc
          (Fin.last
            ((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}) +
              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}
                  y₁)))),
      ((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₁ hsat₁).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₁ hsaty₁).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
        (Fin.succ
          (Fin.last
            ((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}) +
              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}
                  y₁)))))
    (((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₂ hsat₂).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₂ hsaty₂).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
        (Fin.castSucc
          ((Equiv.swap (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1))
                (Fin.castSucc (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})))) :
              (a : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length) → Fin ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).length)
            (Fin.last
              ((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}) +
                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}
                    y₁))))),
      ((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₂ hsat₂).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₂ hsaty₂).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
        (Fin.succ
          ((Equiv.swap (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1))
                (Fin.castSucc (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})))) :
              (a : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length) → Fin ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).length)
            (Fin.last
              ((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}) +
                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}
                    y₁))))))
refine_2 :
  ∀
    (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}) +
          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}
              y₁))),
    @Iso _ inst _
      (((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₁ hsat₁).snoc (r :=
              {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₁ hsaty₁).toFun
          (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) i.castSucc.castSucc,
        ((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₁ hsat₁).snoc (r :=
              {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₁ hsaty₁).toFun
          (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) i.castSucc.succ)
      (((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₂ hsat₂).snoc (r :=
              {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₂ hsaty₂).toFun
          (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
          (Fin.castSucc
            ((Equiv.swap (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1))
                  (Fin.castSucc (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})))) :
                (a : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length) → Fin ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).length)
              i.castSucc)),
        ((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₂ hsat₂).snoc (r :=
              {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₂ hsaty₂).toFun
          (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
          (Fin.succ
            ((Equiv.swap (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1))
                  (Fin.castSucc (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})))) :
                (a : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length) → Fin ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).length)
              i.castSucc)))
⊢ @Iso _ inst _
    (((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₁ hsat₁).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₁ hsaty₁).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) i.castSucc,
      ((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₁ hsat₁).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₁ hsaty₁).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) i.succ)
    (((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₂ hsat₂).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₂ hsaty₂).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
        (Fin.castSucc
          ((Equiv.swap (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1))
                (Fin.castSucc (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})))) :
              (a : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length) → Fin ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).length)
            i)),
      ((snoc (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) s x₂ hsat₂).snoc (r :=
            {x : X × X | @IsMaximal _ inst _ x.1 x.2}) y₂ hsaty₂).toFun
        (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})
        (Fin.succ
          ((Equiv.swap (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2}) + 1))
                (Fin.castSucc (Fin.last (s.length (r := {x : X × X | @IsMaximal _ inst _ x.1 x.2})))) :
              (a : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length) → Fin ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).length)
            i)))

Tactic:
refine Fin.lastCases ?_ (fun i => ?_) i