-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
f : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l } → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((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
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ‖f
        (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
          (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
            (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))‖₊ ≤
    nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun
                (i :
                  Fin
                    (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                          (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                            (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs))) +
                      Sigma.fst (β := fun (l_1 : ℕ) ↦
                        { s_1 :
                          Finset
                            (Fin
                              (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                                  (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                                    (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                                      (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs))) +
                                l_1)) //
                          s_1.card = l_1 })
                        (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                          (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                            (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                              (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))))) ↦
              E)
            F)
          (p
            (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                  (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                    (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs))) +
              Sigma.fst (β := fun (l_1 : ℕ) ↦
                { s_1 :
                  Finset
                    (Fin
                      (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                          (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                            (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                              (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs))) +
                        l_1)) //
                  s_1.card = l_1 })
                (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                  (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                    (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                      (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))))) *
        HPow.hPow (β := ℕ) ‖x‖₊
          (Sigma.fst (β := fun (l_1 : ℕ) ↦
            { s_1 :
              Finset
                (Fin
                  (Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                      (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                        (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                          (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs))) +
                    l_1)) //
              s_1.card = l_1 })
            (Sigma.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
              (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
                (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                  (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs))))) *
      ‖y‖₊ ^
        Sigma.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
          (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
            (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
              (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))
have dsimp : ‖f
      (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
        (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
          (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))‖₊ ≤
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) * ‖x‖₊ ^ l *
    ‖y‖₊ ^ k
Tactic: dsimp only [Subtype.coe_mk]