Filling in some implicit variables in complicated functions

Stream: lean4

[aprilgrimoire]

Hi! I want to use

Subfield.closure_induction.{u} {K : Type u} [DivisionRing K] {s : Set K} {p : (x : K) → x ∈ Subfield.closure s → Prop}
  (mem : ∀ (x : K) (hx : x ∈ s), p x ⋯) (one : p 1 ⋯)
  (add : ∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x + y) ⋯)
  (neg : ∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p (-x) ⋯)
  (inv : ∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p x⁻¹ ⋯)
  (mul : ∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x * y) ⋯) {x : K}
  (h : x ∈ Subfield.closure s) : p x h

Which takes many arguments. For clarity, I want to fill in p first to make sure the type inference system provides easy-to-read complaints. However, I don't want to fill in things such as K and s explicitly. How can I achieve this?

Thanks!

EDIT: After using @, I'm asked to fill in inst variables, which I don't know how to do.

[Joachim Breitner]

Are you using this in apply or induction … using or outside of tactics?

[Joachim Breitner]

You can write `Subfield.closure_induction (p := …) to fill in only one parameter.

[aprilgrimoire]

T

Joachim Breitner said:

You can write `Subfield.closure_induction (p := …) to fill in only one parameter.

outside of tactics.

Thanks! That's a very convenient syntax I haven't seen in any references.