lean baffled by my definition

Stream: new members

[Alexandra Foster]

Hi there! I'm a math undergrad at McMaster University in Hamilton, Ontario with a bit of a geometry addiction who decided to try and acquire some skill at Lean over the course of the summer by proving some elementary propositions in algebraic geometry about monomial ideals and their corresponding varieties. However, I've hit an enigmatic error and I'm not sure what to do about it to please Lean. Here is the code I'm attempting to run:

import data.set.basic
import data.fintype.basic
import algebra.field

noncomputable theory

variables {k : Type} [field k]
variables {σ : Type} [fintype σ]

-- a subset V of k^n is called a "coordinate subspace"
--   if there exists a subset τ of the set of variable
--   indices σ such that
--        V = {(x₁,x₂,...,xₙ) | ∀ t ∈ τ, xₜ = 0}
def coordinate_subspace (τ : set σ) : (set (σ → k)) :=
  {x : σ → k |
    ∀ t ∈ τ, x t = 0}

-- proposition: V is a union of coordinate subspaces
def union_of_coords (V : set (σ → k)) : Prop :=
  ∃ α : set (set σ),
    ∀ p : σ → k, p ∈ V → ∃ τ : set σ,
                     τ ∈ α ∧ p ∈ coordinate_subspace τ

The error I get:

-- don't know how to synthesize placeholder
-- context:
-- k : Type,
-- _inst_1 : field k,
-- σ : Type,
-- _inst_2 : fintype σ,
-- V : set (σ → k),
-- α : set (set σ),
-- p : σ → k,
-- ᾰ : p ∈ V,
-- τ : set σ
-- ⊢ Type

How can I uhhh... make it so that it is possible to umm... synthesize a "placeholder context"?
(BTW, for motivation & context: my eventual goal is to prove that any variety corresponding to a monomial ideal is a union of coordinate subspaces, Proposition 1 of Chapter 9 of Ideals, Varieties & Algorithms by Cox, Little & O'Shea)

[Heather Macbeth]

variables (k : Type) [field k]

...

-- proposition: V is a union of coordinate subspaces
def union_of_coords (V : set (σ → k)) : Prop :=
  ∃ α : set (set σ),
    ∀ p : σ → k, p ∈ V → ∃ τ : set σ,
                     τ ∈ α ∧ p ∈ coordinate_subspace k τ

[Heather Macbeth]

Lean was having trouble figuring out what the field k was ... if you make that argument explicit, it can figure out what it is.

[Heather Macbeth]

(Welcome! Lots of good geometry at McMaster, although I know the differential geometry side better.)

[Alexandra Foster]

(I honestly have ambitions toward differential geometry but I sorta flunked an elementary differential geometry course last fall term so maybe my dreams are just dreams)

[Alexandra Foster]

Heather Macbeth said:

Lean was having trouble figuring out what the field k was ... if you make that argument explicit, it can figure out what it is.

all good now!! thank you!!!