α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ filter ((fun x x_1 => x ≠ x_1) a) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ↑(filterNe a (fill a m.fst m.snd)).snd = ↑m.snd
rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ∀ (a_1 : α), ¬a_1 ∈ filter ((fun x x_1 => x ≠ x_1) a) ↑(replicate (↑m.fst) a)

α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ∀ (a_1 : α), a_1 ∈ ↑m.snd → (fun x x_1 => x ≠ x_1) a a_1
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ filter ((fun x x_1 => x ≠ x_1) a) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd
rw [filter_add, filter_eq_self.2, add_right_eq_self, eq_zero_iff_forall_not_mem]
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
b : α
hb : b ∈ filter ((fun x x_1 => x ≠ x_1) a) ↑(replicate (↑m.fst) a)
⊢ False
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ∀ (a_1 : α), ¬a_1 ∈ filter ((fun x x_1 => x ≠ x_1) a) ↑(replicate (↑m.fst) a)
intro b hb
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
b : α
hb : (↑m.fst ≠ 0 ∧ b = a) ∧ (fun x x_1 => x ≠ x_1) a b
⊢ False
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
b : α
hb : b ∈ filter ((fun x x_1 => x ≠ x_1) a) ↑(replicate (↑m.fst) a)
⊢ False
rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
no goals
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b✝ : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
b : α
hb : (↑m.fst ≠ 0 ∧ b = a) ∧ (fun x x_1 => x ≠ x_1) a b
⊢ False
exact hb.2 hb.1.2.symm
no goals
α : Type u_1
β : Type ?u.55875
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ¬a ∈ m.snd
⊢ ∀ (a_1 : α), a_1 ∈ ↑m.snd → (fun x x_1 => x ≠ x_1) a a_1
exact fun a ha ha' => h <| ha'.symm ▸ ha