Type class inference in forall

Stream: general

[Arnoud van der Leer]

Hi there, it's me again. I am trying to prove an equivalence about fields. One of these says "if R is a field, all morphisms to nonzero rings S are injective".

import algebra.field

universes u v

lemma p2 {R: Type u} [comm_ring R] (exists_pair_ne : ∃ (x y : R), x ≠ y) (h: is_field R) : ∀ {S: Type v} [comm_ring S] (f: R →+* S), function.injective f := begin
  sorry,
end

However, Lean does not compile the (f: R →+* S) part with an error

failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
exists_pair_ne : ∃ (x y : R), x ≠ y,
h : is_field R,
S : Type v,
_inst_2 : comm_ring S
⊢ semiring SLean

How should I fix this?

Note that the forall is part of a tfae, so I won't be able to get S and [comm_ring S] out of the forall.

[Mario Carneiro]

You need by exactI to pick up typeclass instances in binders

[Mario Carneiro]

lemma p2 {R: Type u} [comm_ring R] (exists_pair_ne : ∃ (x y : R), x ≠ y) (h: is_field R) :
  ∀ {S: Type v} [comm_ring S], by exactI ∀ (f: R →+* S), function.injective f :=
begin
  ...

[Arnoud van der Leer]

That works. Thank you!

[Kevin Buzzard]

exists_pair_ne already exists in Lean, it's called something like nontrivial, but here you don't need it at all because it's implied by is_field.

[Arnoud van der Leer]

Ah, right. In this case it was a remnant of the bigger tfae that I forgot to remove when writing my minimal example.
I'll have a look at nontrivial. I just copied is_field.exists_pair_ne.

[Eric Rodriguez]

nontriviality may be helpful - great tactic :)

[Anne Baanen]

(Beware that most of the library is designed assuming your parameters look like {R : Type u} [field R] rather than {R : Type u} [comm_ring R] (h : is_field R), so you might save yourself some trouble by switching if that is possible.)