-- Module: Mathlib.Order.JordanHolder
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
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})
        (Fin.castSucc
          (((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))))
                  h).symm :
              (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
          (((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))))
                  h).symm :
              (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})
        i.castSucc,
      s₂.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i.succ)

Tactic:
simpa using h.choose_spec (h.choose.symm i)

Premises used: Exists.choose_spec, Exists.choose, Equiv.symm, DFunLike.coe