-- 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
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ Eq (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
    ((fun (s : (n : ℕ) × Finset (Fin n)) ↦
        (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
            (s.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)
            (Sigma.mk (β := fun (l : ℕ) ↦
              { s_1 :
                Finset
                  (Fin
                    (s.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card + l)) //
                s_1.card = l })
              s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card
              (Subtype.mk (p :=
                fun
                  (s_1 :
                    Finset
                      (Fin
                        (s.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
                          s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card))) ↦
                s_1.card = s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)
                (Finset.map (Equiv.toEmbedding (finCongr ⋯)) (s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)))) ⋯)) :
          (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
      ((fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n))
              (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))) :
            (n : ℕ) × Finset (Fin n)))
        (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.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 : Eq (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
  (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) (k + l - s.card)
    (Sigma.mk (β := fun (l_1 : ℕ) ↦ { s_1 : Finset (Fin (k + l - s.card + l_1)) // s_1.card = l_1 }) s.card
      (Subtype.mk (p := fun (s_1 : Finset (Fin (k + l - s.card + s.card))) ↦ s_1.card = s.card)
        (Finset.map (Equiv.toEmbedding (finCongr sorry)) s) sorry)))
  (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)))
Tactic: dsimp only [Subtype.coe_mk]