awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
i : α
e : β
he : e ∈ d
hi : ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) = i
h : ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) ∈ s
⊢ i ∈ s

Tactic:
rw [← hi]
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
i : α
e : β
he : e ∈ d
hi : ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) = i
⊢ ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) ∈ s

Tactic:
(hd e he).choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, setOf, And.left
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
i : α
e : β
he : e ∈ d
hi : ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) = i
⊢ ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = e) ∈ s

Tactic:
exact (hd e he).choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
h :
  Sym.map
      (fun (x : { x : β // x ∈ d }) ↦
        (g : (a : α) → β) (⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = (↑x : β))))
      d.attach =
    d
⊢ Sym.map.{u_1, u_2} (α := α) (⇑g : (a : α) → β) ((fun (p : Sym { x : β // x ∈ d } n) ↦ Sym.map g' p) d.attach) = d

Tactic:
simp only [Sym.map_map, Function.comp_apply, g']

Premises used: Function.comp_apply, Sym.map_map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
⊢ Sym.map (Subtype.val (p := fun (x : β) ↦ x ∈ d)) d.attach = d

Tactic:
Sym.attach_map_coe d

Premises used: Sym.attach_map_coe
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
h :
  ∀ (x : β) (hx : x ∈ d) (hx' : Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx ∈ d.attach),
    (g : (a : α) → β)
        (⋯.choose (p := fun (a : α) ↦
          a ∈ s ∧ (g : (a : α) → β) a = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β))) =
      (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β)
⊢ Sym.map
      (fun (x : { x : β // x ∈ d }) ↦
        (g : (a : α) → β) (⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = (↑x : β))))
      d.attach =
    d

Tactic:
convert! Sym.attach_map_coe d with ⟨x, hx⟩ hx'

Premises used: Sym.attach_map_coe
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
x : β
hx : x ∈ d
hx' : Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx ∈ d.attach
⊢ (g : (a : α) → β)
      (⋯.choose (p := fun (a : α) ↦
        a ∈ s ∧ (g : (a : α) → β) a = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β))) =
    (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β)

Tactic:
(hd x hx).choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, (g : (a : α) → β) a_2 = a
g' : { x : β // x ∈ d } → α :=
  fun (x : { x : β // x ∈ d }) ↦
    match (motive := { x : β // x ∈ d } → α) x with
    | ⟨x, hx⟩ => ⋯.choose (p := fun (a : α) ↦ a ∈ s ∧ (g : (a : α) → β) a = x)
x : β
hx : x ∈ d
hx' : Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx ∈ d.attach
⊢ (g : (a : α) → β)
      (⋯.choose (p := fun (a : α) ↦
        a ∈ s ∧ (g : (a : α) → β) a = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β))) =
    (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ d) x hx) : β)

Tactic:
exact (hd x hx).choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
d' : β
hd : d' ∈ d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
⊢ ∃ a ∈ b, (g : (a : α) → β) a = d'

Tactic:
rw [← hd', Sym.mem_map] at hd

Premises used: Sym.mem_map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
d' : β
hd : d' ∈ d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
hd₁ : ∃ a ∈ b, (g : (a : α) → β) a = d'
⊢ ∀ a ∈ b, a ∈ s

Tactic:
rw [← hd', Sym.mem_map] at hd

Premises used: Sym.mem_map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
d' : β
hd : d' ∈ d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
hd₁ : ∃ a ∈ b, (g : (a : α) → β) a = d'
hb₁ : ∀ a ∈ b, a ∈ s
⊢ Sym.map (⇑g : (a : α) → β) b = d

Tactic:
rw [← hd', Sym.mem_map] at hd

Premises used: Sym.mem_map
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h_1 : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
d' : β
b : Sym α n
hd : ∃ a ∈ b, (g : (a : α) → β) a = d'
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
h : ∀ (a : α) (ha : a ∈ b), ∃ a_1 ∈ s, Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) a_1 : β) ((g : (a : α) → β) a : β)
⊢ ∃ a ∈ s, (g : (a : α) → β) a = d'

Tactic:
obtain ⟨a, ha, rfl⟩ := hd

Premises used: rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
a : α
ha : a ∈ b
⊢ ∃ a_1 ∈ s, Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) a_1 : β) ((g : (a : α) → β) a : β)

Tactic:
⟨a, hb a ha, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
h : ∃ (a : Sym α n), (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g : (a : α) → β) a = d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g : (a : α) → β) b = d
a : α
ha : a ∈ b
⊢ ∃ a_1 ∈ s, Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) a_1 : β) ((g : (a : α) → β) a : β)

Tactic:
exact ⟨a, hb a ha, rfl⟩
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Finset (Sym α (n + 1))) (Finset.sym ∅ (n + 1)) ∅

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.sup, Finset.sym, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
a : α
inst : DecidableEq α
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
rwa rwa₁ rwa₂ rwa₃ : a ∈ s
⊢ b ∈ s

Tactic:
rwa [(Sym.mem_replicate.1 hb).2]

Premises used: Sym.mem_replicate, And.right, Iff.mp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
h : s.Nonempty
n : ℕ
⊢ (s.sym n).Nonempty

Tactic:
let ⟨_a, ha⟩ := h
  ⟨_, replicate_mem_sym ha n⟩

Premises used: Sym.replicate, Finset.replicate_mem_sym, _private.0.Finset.Nonempty.sym.match_1, Exists.intro, Finset.Nonempty, Finset.sym
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ Eq (α := Finset (Sym α n)) (Finset.sym {a} n) {Sym.replicate n a}

Tactic:
eq_singleton_iff_unique_mem.2
    ⟨replicate_mem_sym (mem_singleton.2 rfl) _, fun _s hs ↦
      Sym.eq_replicate_iff.2 fun _b hb ↦ eq_of_mem_singleton <| mem_sym_iff.1 hs _ hb⟩

Premises used: Iff.mpr, Finset.mem_singleton, Finset.mem_sym_iff, Sym.eq_replicate_iff, Finset.eq_of_mem_singleton, Finset.replicate_mem_sym, Finset.eq_singleton_iff_unique_mem, And.intro, Iff.mp, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
h : s.sym n = ∅
contrapose! : ∀ (h : s.Nonempty), (s.sym n).Nonempty
⊢ s = ∅

Tactic:
contrapose! h
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
h : s.Nonempty
⊢ (s.sym n).Nonempty

Tactic:
h.sym _

Premises used: Finset.Nonempty.sym
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
h : s.Nonempty
⊢ (s.sym n).Nonempty

Tactic:
exact h.sym _

Premises used: Finset.Nonempty.sym
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
zero : Eq (α := Finset (Sym α 0)) (s.sym 0) ∅ ↔ Ne (α := ℕ) 0 0 ∧ s = ∅
succ : ∀ (n : ℕ), Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) ∅ ↔ n + 1 ≠ 0 ∧ s = ∅
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
cases n
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ Eq (α := Finset (Sym α 0)) (s.sym 0) ∅ ↔ Ne (α := ℕ) 0 0 ∧ s = ∅

Tactic:
iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim

Premises used: False.elim, iff_of_false, And.left, Finset.singleton_ne_empty, rfl
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ Eq (α := Finset (Sym α 0)) (s.sym 0) ∅ ↔ Ne (α := ℕ) 0 0 ∧ s = ∅

Tactic:
exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim

Premises used: iff_of_false, Finset.singleton_ne_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) ∅ ↔ n + 1 ≠ 0 ∧ s = ∅

Tactic:
⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩

Premises used: Nat.succ_ne_zero, Finset.eq_empty_of_sym_eq_empty, And.intro, Iff.intro
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
succ : n + 1 ≠ 0 ∧ s = ∅ → Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) ∅
⊢ Eq (α := Finset (Sym α (n + 1))) (s.sym (n + 1)) ∅ ↔ n + 1 ≠ 0 ∧ s = ∅

Tactic:
refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
left : n + 1 ≠ 0
⊢ Eq.{u_1 + 1} (α := Finset (Sym α (n + 1))) (Finset.sym ∅ (n + 1)) ∅

Tactic:
sym_empty _

Premises used: Finset.sym_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
left : n + 1 ≠ 0
⊢ Eq.{u_1 + 1} (α := Finset (Sym α (n + 1))) (Finset.sym ∅ (n + 1)) ∅

Tactic:
exact sym_empty _

Premises used: Finset.sym_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
contrapose! : s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅
⊢ (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

Tactic:
contrapose!
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
sym_eq_empty

Premises used: Finset.sym_eq_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
exact sym_eq_empty

Premises used: Finset.sym_eq_empty
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Finset (Sym α n)) (Finset.sym univ n) univ

Tactic:
eq_univ_iff_forall.2 fun _s ↦ mem_sym_iff.2 fun _a _ ↦ mem_univ _

Premises used: Iff.mpr, Finset.mem_univ, Finset.eq_univ_iff_forall, Finset.mem_sym_iff
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
n : ℕ
⊢ s.sym n ⊆ t.sym n

Tactic:
fun _m hm ↦
  mem_sym_iff.2 fun _a ha ↦ h <| mem_sym_iff.1 hm _ ha

Premises used: Iff.mpr, Finset.mem_sym_iff, Iff.mp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
n : ℕ
h : ∀ (m : Sym α n), m ∈ (s ∩ t).sym n ↔ m ∈ s.sym n ∩ t.sym n
⊢ (s ∩ t).sym n = s.sym n ∩ t.sym n

Tactic:
ext m
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ (s ∩ t).sym n ↔ m ∈ s.sym n ∩ t.sym n

Tactic:
simp only [mem_inter, mem_sym_iff, imp_and, forall_and]

Premises used: Finset.mem_sym_iff, imp_and, Finset.mem_inter, forall_and
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
n : ℕ
⊢ s.sym n ∪ t.sym n ⊆ (s ∪ t).sym n

Tactic:
union_subset (sym_mono subset_union_left n) (sym_mono subset_union_right n)

Premises used: Finset.union_subset, Finset.subset_union_left, Finset.subset_union_right, Finset.sym_mono
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
a : α
i : Fin (n + 1)
m : Sym α (n - (↑i : ℕ))
h : Membership.mem (γ := Finset (Sym α (n - (↑i : ℕ)))) (s.sym (n - (↑i : ℕ))) m
⊢ Sym.fill a i m ∈ (insert a s).sym n

Tactic:
mem_sym_iff.2 fun b hb ↦
    mem_insert.2 <| (Sym.mem_fill_iff.1 hb).imp And.right <| mem_sym_iff.1 h b

Premises used: Iff.mpr, Finset.mem_sym_iff, Sym.mem_fill_iff, Finset.mem_insert, And.right, Iff.mp, Or.imp
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
n : ℕ
m : Sym α n
a : α
h : m ∈ s.sym n
⊢ Membership.mem (γ :=
    Finset (Sym α (n - (↑((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ))))
    ((s.erase a).sym (n - (↑((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
    ((Sym.filterNe a m).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))

Tactic:
mem_sym_iff.2 fun b H ↦
    mem_erase.2 <| (Multiset.mem_filter.1 H).symm.imp Ne.symm <| mem_sym_iff.1 h b

Premises used: Iff.mpr, And.imp, Finset.mem_sym_iff, Ne.symm, Finset.mem_erase, Iff.mp, Multiset.mem_filter, And.symm
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ Membership.mem (γ :=
    Finset
      (Sym α (n - (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ))))
    (((insert a s).erase a).sym
      (n - (↑((Sym.filterNe a (↑m : Sym α n)).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)))
    ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))

Tactic:
sym_filterNe_mem a m.2

Premises used: Finset.sym_filterNe_mem, Subtype.property
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
h₁ : s = (insert a s).erase a
⊢ 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 : ℕ)))) : ℕ)))
    ((Sym.filterNe a (↑m : Sym α n)).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))

Tactic:
convert! sym_filterNe_mem a m.2

Premises used: Finset.sym_filterNe_mem, Subtype.property
-- Module: Mathlib.Data.Finset.Sym
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
h₁ h₂ : s = s
⊢ s = (insert a s).erase a

Tactic:
rw [erase_insert h]

Premises used: Finset.erase_insert
-- 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
⊢ 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))

Tactic:
Function.Injective.sigma_map (β₂ := ?_) (f₂ := ?_)
        (Function.injective_id) (fun i ↦ ?_) ?_

Premises used: Function.Injective.sigma_map, Function.injective_id
-- 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
⊢ Fin (n + 1) → Type u_1

Tactic:
exact fun i ↦ Sym α (n - i)

Premises used: HSub.hSub, Sym
-- 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_1 : Fin (n + 1)
m : Sym α (n - (↑i_1 : ℕ))
hm : Membership.mem (γ := Finset (Sym α (n - (↑i_1 : ℕ)))) (s.sym (n - (↑i_1 : ℕ))) m
i : Fin (n + 1)
⊢ Function.Injective (β := Sym α (n - (↑(id i) : ℕ))) fun (a : ↥(s.sym (n - (↑i : ℕ)))) ↦
    (↑a : Sym α (n - (↑(id i) : ℕ)))

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- 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_1 : Fin (n + 1)
m : Sym α (n - (↑i_1 : ℕ))
hm : Membership.mem (γ := Finset (Sym α (n - (↑i_1 : ℕ)))) (s.sym (n - (↑i_1 : ℕ))) m
i : Fin (n + 1)
⊢ Function.Injective (β := Sym α (n - (↑(id i) : ℕ))) fun (a : ↥(s.sym (n - (↑i : ℕ)))) ↦
    (↑a : Sym α (n - (↑(id i) : ℕ)))

Tactic:
exact Subtype.coe_injective

Premises used: Subtype.coe_injective
-- 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
⊢ 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:
Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)

Premises used: Sym.filter_ne_fill, Eq.trans