-- Module: Mathlib.Analysis.Analytic.Inverse
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (p 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 E F) :
        (a : E →L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F)
      (↑i : E →L[𝕜] F))
n_1 n : ℕ
v : (i : Fin (n + 2)) → E
A :
  Eq (α := Finset (Composition (n + 2))) univ
    (Set.toFinset {c : Composition (n + 2) | c.length < n + 2} ∪ {Composition.ones (n + 2)})
B :
  Disjoint (α := Finset (Composition (n + 2))) (Set.toFinset {c : Composition (n + 2) | c.length < n + 2})
    {Composition.ones (n + 2)}
C :
  Eq.{u_2 + 1} (α := E)
    ((p.leftInv i x (Composition.length (n := n + 2) (Composition.ones (n + 2))) :
          (a : (i : Fin (Composition.ones (n + 2)).length) → F) → E)
        fun (j : Fin (Composition.length (n := n.succ.succ) (Composition.ones n.succ.succ))) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ j) :
      E)
    ((p.leftInv i x (n + 2) : (a : (i : Fin (n + 2)) → F) → E) fun (j : Fin (n + 2)) ↦
        (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j :
      E)
convert_2 :
  Eq.{u_2 + 1} (α := E)
    (∑ a ∈ Set.toFinset {x : Composition (n + 2) | x.length < n + 2},
      (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E)) a
            (p.leftInv i x a.length) :
          (a : (i : Fin (n + 2)) → F) → E)
        fun (j : Fin (n + 2)) ↦ (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j)
    (∑ c ∈ Set.toFinset {c : Composition (n + 2) | c.length < n + 2},
      (p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v))
⊢ Eq.{u_2 + 1} (α := E)
    (∑ a : { c : Composition (n + 2) // c.length < n + 2 },
      (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap (↑i.symm : F →L[𝕜] E))
            (↑a : Composition (n + 2)) (p.leftInv i x (↑a : Composition (n + 2)).length) :
          (a : (i : Fin (n + 2)) → F) → E)
        fun (j : Fin (n + 2)) ↦ (p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ v j)
    (∑ c ∈ Set.toFinset {c : Composition (n + 2) | c.length < n + 2},
      (p.leftInv i x c.length : (a : (i : Fin c.length) → F) → E) (p.applyComposition c v))

Tactic:
convert!
        (sum_toFinset_eq_subtype (fun c : Composition (n + 2) => c.length < n + 2)
              (fun c : Composition (n + 2) =>
                (ContinuousMultilinearMap.compAlongComposition
                    (p.compContinuousLinearMap (i.symm : F →L[𝕜] E)) c (p.leftInv i x c.length))
                  fun j : Fin (n + 2) => p 1 fun _ : Fin 1 => v j)).symm.trans
          _

Premises used: ContinuousLinearEquiv.symm, Composition.length, ContinuousMultilinearMap.compAlongComposition, FormalMultilinearSeries.compContinuousLinearMap, HAdd.hAdd, Finset.sum_toFinset_eq_subtype, LT.lt, OfNat.ofNat, Eq.symm, DFunLike.coe, FormalMultilinearSeries.leftInv, Eq.trans, ContinuousLinearEquiv.toContinuousLinearMap