-- 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
refine_4 :
  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)))))
refine_4₁ :
  a ∉
    (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))) :
      Sym α
        (n -
          (↑(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)))) :
            ℕ)))
⊢ 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 : ℕ)))) ⋯) :
            (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.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 Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)

Premises used: Sym.filter_ne_fill, Eq.trans