[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
a : α × α
h : a ∈ offDiag s
⊢ ¬Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) a)
[PROOFSTEP]
rw [Sym2.isDiag_iff_proj_eq]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
a : α × α
h : a ∈ offDiag s
⊢ ¬a.fst = a.snd
[PROOFSTEP]
exact (mem_offDiag.1 h).2.2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ m ∈ Finset.sym2 s ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
refine mem_image.trans ⟨?_, fun h ↦ ⟨m.out, mem_product.2 ⟨h _ m.out_fst_mem, h _ m.out_snd_mem⟩, m.out_eq⟩⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ (∃ a, a ∈ s ×ˢ s ∧ Quotient.mk' a = m) → ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
rintro ⟨⟨a, b⟩, h, rfl⟩
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ ∀ (a_1 : α), a_1 ∈ Quotient.mk' (a, b) → a_1 ∈ s
[PROOFSTEP]
rw [Quotient.mk', @Sym2.ball _ (fun x ↦ x ∈ s)]
[GOAL]
case intro.mk.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ a b : α
h : (a, b) ∈ s ×ˢ s
⊢ a ∈ s ∧ b ∈ s
[PROOFSTEP]
rwa [mem_product] at h 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Quotient.mk (Sym2.Rel.setoid α) (a, b) ∈ Finset.sym2 s ↔ a ∈ s ∧ b ∈ s
[PROOFSTEP]
rw [mem_sym2_iff, Sym2.ball]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Finset.sym2 s = ∅ ↔ s = ∅
[PROOFSTEP]
rw [Finset.sym2, image_eq_empty, product_eq_empty, or_self_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Finset.Nonempty (Finset.sym2 s) ↔ Finset.Nonempty s
[PROOFSTEP]
rw [Finset.sym2, Nonempty.image_iff, nonempty_product, and_self_iff]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
inst✝ : Fintype α
⊢ Finset.sym2 univ = univ
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
inst✝ : Fintype α
a✝ : Sym2 α
⊢ a✝ ∈ Finset.sym2 univ ↔ a✝ ∈ univ
[PROOFSTEP]
simp only [mem_sym2_iff, mem_univ, implies_true]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
m : Sym2 α
a : α
⊢ Finset.sym2 {a} = {Sym2.diag a}
[PROOFSTEP]
rw [Finset.sym2, singleton_product_singleton, image_singleton, Sym2.diag, Quotient.mk']
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ (∀ (b : α), b ∈ Sym2.diag a → b ∈ s) ↔ a ∈ s
[PROOFSTEP]
rw [← mem_sym2_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s
[PROOFSTEP]
exact mk'_mem_sym2_iff.trans <| and_self_iff _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s
[PROOFSTEP]
simp [diag_mem_sym2_mem_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ image Quotient.mk' (diag s) ∪ image Quotient.mk' (offDiag s) = Finset.sym2 s
[PROOFSTEP]
rw [← image_union, diag_union_offDiag]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ image Quotient.mk' (s ×ˢ s) = Finset.sym2 s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m ∈ Finset.sym s Nat.zero ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
refine' mem_singleton.trans ⟨_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
m : Sym α Nat.zero
⊢ m = ∅ → ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
rintro rfl
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ∀ (a : α), a ∈ ∅ → a ∈ s
[PROOFSTEP]
exact fun a ha ↦ (Finset.not_mem_empty _ ha).elim
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ m ∈ Finset.sym s (Nat.succ n) ↔ ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
refine' mem_sup.trans ⟨_, fun h ↦ _⟩
[GOAL]
case succ.refine'_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
⊢ (∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)) → ∀ (a : α), a ∈ m → a ∈ s
[PROOFSTEP]
rintro ⟨a, ha, he⟩ b hb
[GOAL]
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : m ∈ image (Sym.cons a) (Finset.sym s n)
b : α
hb : b ∈ m
⊢ b ∈ s
[PROOFSTEP]
rw [mem_image] at he 
[GOAL]
case succ.refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
a : α
ha : a ∈ s
he : ∃ a_1, a_1 ∈ Finset.sym s n ∧ a ::ₛ a_1 = m
b : α
hb : b ∈ m
⊢ b ∈ s
[PROOFSTEP]
obtain ⟨m, he, rfl⟩ := he
[GOAL]
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ a ::ₛ m
⊢ b ∈ s
[PROOFSTEP]
rw [Sym.mem_cons] at hb 
[GOAL]
case succ.refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b = a ∨ b ∈ m
⊢ b ∈ s
[PROOFSTEP]
obtain rfl | hb := hb
[GOAL]
case succ.refine'_1.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
ha : b ∈ s
⊢ b ∈ s
[PROOFSTEP]
exact ha
[GOAL]
case succ.refine'_1.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b✝ : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ Finset.sym s n
hb : b ∈ m
⊢ b ∈ s
[PROOFSTEP]
exact ih.1 he _ hb
[GOAL]
case succ.refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
m : Sym α (Nat.succ n)
h : ∀ (a : α), a ∈ m → a ∈ s
⊢ ∃ v, v ∈ s ∧ m ∈ image (Sym.cons v) (Finset.sym s n)
[PROOFSTEP]
obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ
[GOAL]
case succ.refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a✝ b : α
n✝ : ℕ
m✝ : Sym α n✝
n : ℕ
ih : ∀ {m : Sym α n}, m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s
a : α
m : Sym α n
h : ∀ (a_1 : α), a_1 ∈ a ::ₛ m → a_1 ∈ s
⊢ ∃ v, v ∈ s ∧ a ::ₛ m ∈ image (Sym.cons v) (Finset.sym s n)
[PROOFSTEP]
exact ⟨a, h _ <| Sym.mem_cons_self _ _, mem_image_of_mem _ <| ih.2 fun b hb ↦ h _ <| Sym.mem_cons_of_mem hb⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b✝ : α
n✝ : ℕ
m : Sym α n✝
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
⊢ b ∈ s
[PROOFSTEP]
rwa [(Sym.mem_replicate.1 hb).2]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
h : Finset.sym s n = ∅
⊢ s = ∅
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty] at h ⊢
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
h : ¬Finset.Nonempty (Finset.sym s n)
⊢ ¬Finset.Nonempty s
[PROOFSTEP]
exact fun hs ↦ h (hs.sym _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym α Nat.zero
⊢ Finset.sym s Nat.zero = ∅ ↔ Nat.zero ≠ 0 ∧ s = ∅
[PROOFSTEP]
exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Finset.sym s (Nat.succ n✝) = ∅ ↔ Nat.succ n✝ ≠ 0 ∧ s = ∅
[PROOFSTEP]
refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
⊢ Nat.succ n✝ ≠ 0 ∧ s = ∅ → Finset.sym s (Nat.succ n✝) = ∅
[PROOFSTEP]
rintro ⟨_, rfl⟩
[GOAL]
case succ.intro
α : Type u_1
inst✝ : DecidableEq α
t : Finset α
a b : α
n✝ : ℕ
m : Sym α (Nat.succ n✝)
left✝ : Nat.succ n✝ ≠ 0
⊢ Finset.sym ∅ (Nat.succ n✝) = ∅
[PROOFSTEP]
exact sym_empty _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ Finset.Nonempty (Finset.sym s n) ↔ n = 0 ∨ Finset.Nonempty s
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty, Ne.def]
  -- Porting note: using simp_rw does not work here, it does nothing...
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m : Sym α n
⊢ ¬Finset.sym s n = ∅ ↔ n = 0 ∨ ¬s = ∅
[PROOFSTEP]
rwa [sym_eq_empty, not_and_or, not_ne_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a b : α
n✝ : ℕ
m : Sym α n✝
s t : Finset α
n : ℕ
⊢ Finset.sym (s ∩ t) n = Finset.sym s n ∩ Finset.sym t n
[PROOFSTEP]
ext m
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a b : α
n✝ : ℕ
m✝ : Sym α n✝
s t : Finset α
n : ℕ
m : Sym α n
⊢ m ∈ Finset.sym (s ∩ t) n ↔ m ∈ Finset.sym s n ∩ Finset.sym t n
[PROOFSTEP]
simp only [mem_inter, mem_sym_iff, imp_and, forall_and]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)
[PROOFSTEP]
convert sym_filterNe_mem a m.2
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
m : { x // x ∈ Finset.sym (insert a s) n }
⊢ s = erase (insert a s) a
[PROOFSTEP]
rw [erase_insert h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (fun m =>
        { fst := (Sym.filterNe a ↑m).fst,
          snd :=
            { val := (Sym.filterNe a ↑m).snd,
              property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
      ((fun m =>
          { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
        { fst := i, snd := { val := m, property := hm } }) =
    { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
refine' Function.Injective.sigma_map (Function.injective_id) (fun i ↦ _) _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Fin (n + 1) → Type ?u.22728
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (a : Fin (n + 1)) → { x // x ∈ Finset.sym s (n - ↑a) } → ?refine'_1 (id a)
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ Finset.sym s (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine'_2 i)
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id ?refine'_2
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id ?refine'_2 { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
exact fun i ↦ Sym α (n - i)
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (a : Fin (n + 1)) → { x // x ∈ Finset.sym s (n - ↑a) } → Sym α (n - ↑(id a))
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ Finset.sym s (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine'_2 i)
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id ?refine'_2
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id ?refine'_2 { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
swap
[GOAL]
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i✝ : Fin (n + 1)
m : Sym α (n - ↑i✝)
hm : m ∈ Finset.sym s (n - ↑i✝)
i : Fin (n + 1)
⊢ Function.Injective (?refine'_2 i)
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ (a : Fin (n + 1)) → { x // x ∈ Finset.sym s (n - ↑a) } → Sym α (n - ↑(id a))
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id ?refine'_2
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id ?refine'_2 { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
exact Subtype.coe_injective
[GOAL]
case refine'_4
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id (fun i a => ↑a)
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }
[PROOFSTEP]
refine Eq.trans ?_ (Sym.filter_ne_fill a _ ?_)
[GOAL]
case refine'_4.refine_1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ Sigma.map id (fun i a => ↑a)
      ((fun m =>
          { fst := (Sym.filterNe a ↑m).fst,
            snd :=
              { val := (Sym.filterNe a ↑m).snd,
                property := (_ : (Sym.filterNe a ↑m).snd ∈ Finset.sym s (n - ↑(Sym.filterNe a ↑m).fst)) } })
        ((fun m =>
            { val := Sym.fill a m.fst ↑m.snd, property := (_ : Sym.fill a m.fst ↑m.snd ∈ Finset.sym (insert a s) n) })
          { fst := i, snd := { val := m, property := hm } })) =
    Sym.filterNe a
      (Sym.fill a (Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }).fst
        (Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }).snd)
case refine'_4.refine_2
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
n : ℕ
m✝ : Sym α n
h : ¬a ∈ s
x✝ : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ Finset.sym s (n - ↑i)
⊢ ¬a ∈ (Sigma.map id (fun i a => ↑a) { fst := i, snd := { val := m, property := hm } }).snd
[PROOFSTEP]
exacts [rfl, h ∘ mem_sym_iff.1 hm a]
