no goals
α : Type u_1
β : Type ?u.50039
n n' m : ℕ
s✝ : Sym α n
a✝ b✝ a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s
rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]