-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      s₂
ht :
  last (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      t₁ =
    head (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin
    (s₁.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      s₂.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})) ≃
  Fin
    (t₁.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      t₂.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})) :=
  Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
    (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Equiv.symm finSumFinEquiv)
      ((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
                    (t₁.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)
                (t₁.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 t₁.length) i)),
                  t₁.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 t₁.length) i))))
            h₁).sumCongr
        (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
                  (t₂.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)
              (t₂.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 t₂.length) i)),
                t₂.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 t₂.length) i))))
          h₂)))
    finSumFinEquiv
i_1 :
  Fin
    ((smash (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y})
          s₁ s₂ hs).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 _
    ((smash (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₁ s₂ hs).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.castSucc
          (Fin.natAdd
            (s₁.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}))
            i)),
      (smash (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            s₁ s₂ hs).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.succ
          (Fin.natAdd
            (s₁.length (r :=
              {x : X × X |
                match (motive := X × X → Prop) x with
                | (x, y) => @IsMaximal _ inst _ x y}))
            i)))
    ((smash (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            t₁ t₂ ht).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.castSucc
          ((e : (a : Fin (smash s₁ s₂ hs).length) → Fin (smash t₁ t₂ ht).length)
            (Fin.natAdd
              (s₁.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}))
              i))),
      (smash (r :=
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => @IsMaximal _ inst _ x y})
            t₁ t₂ ht).toFun
        (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        (Fin.succ
          ((e : (a : Fin (smash s₁ s₂ hs).length) → Fin (smash t₁ t₂ ht).length)
            (Fin.natAdd
              (s₁.length (r :=
                {x : X × X |
                  match (motive := X × X → Prop) x with
                  | (x, y) => @IsMaximal _ inst _ x y}))
              i))))

Tactic:
simpa [e, -Fin.castSucc_natAdd, smash_natAdd, smash_succ_natAdd] using h₂.choose_spec i

Premises used: Exists.choose_spec, RelSeries.smash_succ_natAdd, RelSeries.smash_natAdd, Fin.castSucc_natAdd