Implicit/explicit arguments

Stream: new members

[Jon Eugster]

I don't quite understand something that I think has to do with explicit/implicit arguments to my lemma MyLemma below. I get the error:

type mismatch at application
 MyLemma (integral_closure.is_integral x)
term
  integral_closure.is_integral x
has type
  is_integral A x
but is expected to have type
  is_integral ?m_1 ?m_6

And the code producing it is:

import ring_theory.integral_closure
import ring_theory.localization
import linear_algebra.finite_dimensional
import ring_theory.trace

variables {A L: Type*} [comm_ring A] [is_domain A] [field L] [algebra A L] [algebra (fraction_ring A) L]
variable (x:(integral_closure A L))

lemma MyLemma
  {x:L} (h:is_integral A x) : is_integral A ((algebra.trace (fraction_ring A) L) x) :=
begin
  sorry
end

#check (integral_closure.is_integral x)     -- is_integral A x
#check (MyLemma (integral_closure.is_integral x)) --Error here at MyLemma

Why does it ask for m_1 and m_6 instead of figuring out to plug in x and A? Thanks for the help.

[Eric Rodriguez]

this usually means the lemma has stronger typeclass arguments that you don't have in your case

[Jon Eugster]

I see, thinking about what you said I found the mistake, thx.
The lemma was about [algebra (fraction_ring A) L] but the statement used it with [algebra (fraction_ring A) (integral_closure A L)] so the two L should not have been the same things and Lean tried to find an instance [field (integral_closure A L)] which didn't exist