-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x y : E
n : ℕ
t : Finset (Fin n)
this :
  ∀ (m : ℕ) (hm : n = m),
    Eq.{u_3 + 1} (α := F)
      ((p n : (a : (i : Fin n) → E) → F)
          (t.piecewise (π := fun (i : Fin n) ↦ E) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
        F)
      ((p m : (a : (i : Fin m) → E) → F)
          ((Finset.map (finCongr hm).toEmbedding t).piecewise (π := fun (i : Fin m) ↦ E) (fun (x_1 : Fin m) ↦ x)
            fun (x : Fin m) ↦ y) :
        F)
simp_rw :
  Eq.{u_3 + 1} (α := F)
    ((p n : (a : (i : Fin n) → E) → F)
        (t.piecewise (π := fun (i : Fin n) ↦ E) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      F)
    ((p
            (HAdd.hAdd (α := ℕ)
              (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                ((changeOriginIndexEquiv.symm :
                    (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                  (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))
              (Sigma.fst (β := fun (l : ℕ) ↦
                { s :
                  Finset
                    (Fin
                      (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                          ((changeOriginIndexEquiv.symm :
                              (a : (n : ℕ) × Finset (Fin n)) →
                                (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                            (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)) +
                        l)) //
                  s.card = l })
                (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                  ((changeOriginIndexEquiv.symm :
                      (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                    (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t))))) :
          (a :
              (i :
                  Fin
                    (((changeOriginIndexEquiv.symm :
                            (a : (n : ℕ) × Finset (Fin n)) →
                              (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                          ⟨n, t⟩).fst +
                      ((changeOriginIndexEquiv.symm :
                              (a : (n : ℕ) × Finset (Fin n)) →
                                (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                            ⟨n, t⟩).snd.fst)) →
                E) →
            F)
        (Finset.piecewise (π :=
          fun
            (i :
              Fin
                (HAdd.hAdd (α := ℕ)
                  (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                    ((changeOriginIndexEquiv.symm :
                        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))
                  (Sigma.fst (β := fun (l : ℕ) ↦
                    { s :
                      Finset
                        (Fin
                          (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                              ((changeOriginIndexEquiv.symm :
                                  (a : (n : ℕ) × Finset (Fin n)) →
                                    (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)) +
                            l)) //
                      s.card = l })
                    (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      ((changeOriginIndexEquiv.symm :
                          (a : (n : ℕ) × Finset (Fin n)) →
                            (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))))) ↦
          E)
          (↑(Sigma.snd (β := fun (l : ℕ) ↦
                  { s :
                    Finset
                      (Fin
                        (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                            ((changeOriginIndexEquiv.symm :
                                (a : (n : ℕ) × Finset (Fin n)) →
                                  (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                              (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)) +
                          l)) //
                    s.card = l })
                  (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                    ((changeOriginIndexEquiv.symm :
                        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t))) :
                { s :
                  Finset
                    (Fin
                      (HAdd.hAdd (α := ℕ)
                        (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                          ((changeOriginIndexEquiv.symm :
                              (a : (n : ℕ) × Finset (Fin n)) →
                                (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                            (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))
                        (Sigma.fst (β := fun (l : ℕ) ↦
                          { s :
                            Finset
                              (Fin
                                (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                    ((changeOriginIndexEquiv.symm :
                                        (a : (n : ℕ) × Finset (Fin n)) →
                                          (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                      (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)) +
                                  l)) //
                            s.card = l })
                          (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                            ((changeOriginIndexEquiv.symm :
                                (a : (n : ℕ) × Finset (Fin n)) →
                                  (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                              (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))))) //
                  s.card =
                    Sigma.fst (β := fun (l : ℕ) ↦
                      { s :
                        Finset
                          (Fin
                            (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                ((changeOriginIndexEquiv.symm :
                                    (a : (n : ℕ) × Finset (Fin n)) →
                                      (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                  (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)) +
                              l)) //
                        s.card = l })
                      (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        ((changeOriginIndexEquiv.symm :
                            (a : (n : ℕ) × Finset (Fin n)) →
                              (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                          (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t))) }) :
            Finset
              (Fin
                (((changeOriginIndexEquiv.symm :
                        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      ⟨n, t⟩).fst +
                  ((changeOriginIndexEquiv.symm :
                          (a : (n : ℕ) × Finset (Fin n)) →
                            (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        ⟨n, t⟩).snd.fst)))
          (fun
              (x_1 :
                Fin
                  (HAdd.hAdd (α := ℕ)
                    (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      ((changeOriginIndexEquiv.symm :
                          (a : (n : ℕ) × Finset (Fin n)) →
                            (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))
                    (Sigma.fst (β := fun (l : ℕ) ↦
                      { s :
                        Finset
                          (Fin
                            (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                ((changeOriginIndexEquiv.symm :
                                    (a : (n : ℕ) × Finset (Fin n)) →
                                      (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                  (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)) +
                              l)) //
                        s.card = l })
                      (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        ((changeOriginIndexEquiv.symm :
                            (a : (n : ℕ) × Finset (Fin n)) →
                              (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                          (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))))) ↦
            x)
          fun
            (x :
              Fin
                (HAdd.hAdd (α := ℕ)
                  (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                    ((changeOriginIndexEquiv.symm :
                        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))
                  (Sigma.fst (β := fun (l : ℕ) ↦
                    { s :
                      Finset
                        (Fin
                          (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                              ((changeOriginIndexEquiv.symm :
                                  (a : (n : ℕ) × Finset (Fin n)) →
                                    (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)) +
                            l)) //
                      s.card = l })
                    (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      ((changeOriginIndexEquiv.symm :
                          (a : (n : ℕ) × Finset (Fin n)) →
                            (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t)))))) ↦
          y) :
      F)
⊢ let s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l } :=
    (changeOriginIndexEquiv.symm :
        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
      (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t);
  Eq.{u_3 + 1} (α := F)
    (((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))
                (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β :=
                      fun (l : ℕ) ↦
                      { s_1 :
                        Finset
                          (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                        s_1.card = l })) :
                  Finset (Fin (s.fst + s.snd.fst)))
                ⋯ :
              (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
            fun
              (x_1 :
                Fin
                  (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β :=
                    fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l }))) ↦
            x :
          (a : (i : Fin s.fst) → E) → F)
        fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y :
      F)
    ((p n : (a : (i : Fin n) → E) → F)
        (t.piecewise (π := fun (i : Fin n) ↦ E) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      F)

Tactic:
simp_rw [changeOriginSeriesTerm_apply, eq_comm]

Premises used: FormalMultilinearSeries.changeOriginSeriesTerm_apply, eq_comm