-- Lean 4 proof step from Mathlib.Data.Finset.Sym (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
x : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))
i : Fin (n + 1)
m : Sym α (n - (↑i : ℕ))
hm : Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) m
refine_1 : Fin (n + 1) → Type u_1
refine_2 : (a : Fin (n + 1)) → ↥(s.sym (n - (↑a : ℕ))) → Sym α (n - (↑(id a) : ℕ))
refine_3 :
  ∀ (i : Fin (n + 1)),
    Function.Injective (β := Sym α (n - (↑(id i) : ℕ))) fun (a : ↥(s.sym (n - (↑i : ℕ)))) ↦
      (↑a : Sym α (n - (↑(id i) : ℕ)))
⊢ Eq.{u_1 + 1} (α := (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ))))
    ((fun (m : ↥((insert a s).sym n)) ↦
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
            ((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
            (Subtype.mk (p :=
              fun
                (x :
                  Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))) ↦
              Membership.mem (γ :=
                Finset
                  (Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))))
                (s.sym
                  (n -
                    (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
                x)
              ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) ⋯) :
          (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))))
      ((fun (m : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))) ↦
          Subtype.mk (p := fun (x : Sym α n) ↦ x ∈ (insert a s).sym n)
            (Sym.fill a (m.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))))
              (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : Sym α (n - (↑m.fst : ℕ))))
            ⋯)
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
          (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
            Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))))
    (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
      (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
        Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm))
have refine_4 : Eq.{max (u_1 + 1) 1} (α := (i : Fin (n + 1)) × Sym α (n - (↑i : ℕ)))
  (Sigma.map (β₁ := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) (β₂ := fun (i : Fin (n + 1)) ↦
    Sym α (n - (↑i : ℕ))) id (fun (i : Fin (n + 1)) (a : ↥(s.sym (n - (↑i : ℕ)))) ↦ (↑a : Sym α (n - (↑(id i) : ℕ))))
    ((fun (m : ↥((insert a s).sym n)) ↦
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))
            ((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
            (Subtype.mk (p :=
              fun
                (x :
                  Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))) ↦
              Membership.mem (γ :=
                Finset
                  (Sym α
                    (n -
                      (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
                        ℕ))))
                (s.sym
                  (n -
                    (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
                x)
              ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) sorry) :
          (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))))
      ((fun (m : (i : Fin (n + 1)) × ↥(s.sym (n - (↑i : ℕ)))) ↦
          Subtype.mk (p := fun (x : Sym α n) ↦ x ∈ (insert a s).sym n)
            (Sym.fill a (m.fst (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))))
              (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ))))) : Sym α (n - (↑m.fst : ℕ))))
            sorry)
        (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
          (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
            Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm)))))
  (Sigma.map (β₁ := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) (β₂ := fun (i : Fin (n + 1)) ↦
    Sym α (n - (↑i : ℕ))) id (fun (i : Fin (n + 1)) (a : ↥(s.sym (n - (↑i : ℕ)))) ↦ (↑a : Sym α (n - (↑(id i) : ℕ))))
    (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(s.sym (n - (↑i : ℕ)))) i
      (Subtype.mk (p := fun (x : Sym α (n - (↑i : ℕ))) ↦
        Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) x) m hm)))
Tactic: refine Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_)
        (Function.injective_id) (fun i ↦ ?_) ?_