Applying specifc implicit arguemnts

Stream: new members

[Michael Novak]

I think I read about it in the past, but I forgot how to do it and I can't find this information now: How can you apply to a theorem with many implicit arguments only some of the implicit arguments that are not possible for lean to infer? For example I want apply arguments f and n in theorem docs#iteratedDerivWithin_of_isOpen. Btw, why are these arguments in this theorem implicit to begin with? How could lean possibly infer them?

[Snir Broshi]

foo (x := 1) (y := 2)

[Michael Novak]

Thank you very much!

[Michael Rothgang]

docs#iteratedDerivWithin_of_isOpen

[Alex Meiburg]

Btw, why are these arguments in this theorem implicit to begin with? How could lean possibly infer them?

They could be inferred by the context of the surrounding goal. So it wouldn't work with a have h := ..., you're right. Imagine that I have a conclusion of the form

ContinuousOn (Set.piecewise (iteratedDerivWithin n f s) (iteratedDeriv n f)) (Set.ite t s s')

that I want to prove. Now I know that continuousOn_piecewise_ite will be useful, so I could do

refine continuousOn_piecewise_ite ?_ ?_ ?_(iteratedDerivWithin_of_isOpen ?_)

for example. In this case, the arguments to iteratedDerivWithin_of_isOpen are inferred. Or another way this could appear is something like

apply continuousOn_piecewise_ite
· fun_prop
· fun_prop
· <complicated stuff>
· exact iteratedDerivWithin_of_isOpen h

or something, so where I get a sidegoal for Set.EqOn and then it fills it in there.

[Michael Novak]

Alex Meiburg said:

Btw, why are these arguments in this theorem implicit to begin with? How could lean possibly infer them?

They could be inferred by the context of the surrounding goal. So it wouldn't work with a have h := ..., you're right. Imagine that I have a conclusion of the form

ContinuousOn (Set.piecewise (iteratedDerivWithin n f s) (iteratedDeriv n f)) (Set.ite t s s')

that I want to prove. Now I know that continuousOn_piecewise_ite will be useful, so I could do

refine continuousOn_piecewise_ite ?_ ?_ ?_(iteratedDerivWithin_of_isOpen ?_)

for example. In this case, the arguments to iteratedDerivWithin_of_isOpen are inferred. Or another way this could appear is something like

apply continuousOn_piecewise_ite
· fun_prop
· fun_prop
· <complicated stuff>
· exact iteratedDerivWithin_of_isOpen h

or something, so where I get a sidegoal for Set.EqOn and then it fills it in there.

That makes sense, thank you very much!

[Michael Rothgang]

Another reason for making arguments implicit (which does not apply here) is in rw lemmas: if you want to rw by a lemma, any argument that is present on both sides can usually be implicit. This is why, for instance, f is implicit in docs#continuousOn_univ.

[Michael Novak]

Michael Rothgang said:

Another reason for making arguments implicit (which does not apply here) is in rw lemmas: if you want to rw by a lemma, any argument that is present on both sides can usually be implicit. This is why, for instance, f is implicit in docs#continuousOn_univ.

Thank you very much!