Fin-indexed tuples of finsets

theorem Fin.mem_piFinset_succ {n : ℕ} {α : Fin (n + 1) → Type u_1} {x : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)} : x ∈ Fintype.piFinset s ↔ x 0 ∈ s 0 ∧ Fin.tail x ∈ Fintype.piFinset (Fin.tail s)

theorem Fin.mem_piFinset_succ' {n : ℕ} {α : Fin (n + 1) → Type u_1} {x : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)} : x ∈ Fintype.piFinset s ↔ Fin.init x ∈ Fintype.piFinset (Fin.init s) ∧ x (Fin.last n) ∈ s (Fin.last n)

theorem Fin.cons_mem_piFinset_cons {n : ℕ} {α : Fin (n + 1) → Type u_1} {x₀ : α 0} {x : (i : Fin n) → α i.succ} {s₀ : Finset (α 0)} {s : (i : Fin n) → Finset (α i.succ)} : Fin.cons x₀ x ∈ Fintype.piFinset (Fin.cons s₀ s) ↔ x₀ ∈ s₀ ∧ x ∈ Fintype.piFinset s

theorem Fin.snoc_mem_piFinset_snoc {n : ℕ} {α : Fin (n + 1) → Type u_1} {x : (i : Fin n) → α i.castSucc} {xₙ : α (Fin.last n)} {s : (i : Fin n) → Finset (α i.castSucc)} {sₙ : Finset (α (Fin.last n))} : Fin.snoc x xₙ ∈ Fintype.piFinset (Fin.snoc s sₙ) ↔ x ∈ Fintype.piFinset s ∧ xₙ ∈ sₙ