algebra.adjoin is subring.closure

Stream: Is there code for X?

[Eric Wieser]

I seem to be having difficulty stating this lemma:

lemma mem_adjoin_eq {R A : Type*} {x : A} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :
  x ∈ algebra.adjoin R s ↔ x ∈ subsemiring.closure (set.range (algebra_map R A) ∪ s)
begin
   sorry
end

which gives

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

Does this exist already? Am I missing something obvious to make this statement work?

[Adam Topaz]

What are your imports?

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/0bb5e5d94d688bdbde8615d924742315cbe19def/src/ring_theory/algebra.lean#L1093

[Kenny Lau]

This is exactly how adjoin is defined

[Eric Wieser]

I know it is @Kenny Lau, but I can't work out how to unfold that in a proof

[Eric Wieser]

The error was becaused I missed the trailing := ...