-- Module: Mathlib.Data.Finset.Sym
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
⊢ 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 : ℕ)))) ⋯) :
            (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)))) =
    Sym.filterNe a
      (Sym.fill a
        (Sigma.fst (β := fun (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) : ℕ))))
            (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.snd (β := fun (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) : ℕ))))
            (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:
exacts [rfl, h ∘ mem_sym_iff.1 hm a]

Premises used: Finset.mem_sym_iff, Iff.mp, rfl