Trouble with type classes

Stream: general

[Nikolas Kuhn]

I was trying to revert objects which have dependent type classes in order to make a proof by induction on the number of generators of a finitely generated monoid. This seems to cause trouble with the type class system, as noted below. Does anyone have an idea how to fix or get around this?
One thing I tried was to derive the class semiring S explicitly from comm_ring S, but then the class algebra R S didn't match anymore.

import ring_theory.local_properties
import ring_theory.localization.inv_submonoid

variables {R : Type*} (S : Type*) [comm_ring R] (M : submonoid R)  [comm_ring S] [algebra R S]
  [is_localization M S]
lemma finite_presentation_of_monoid_fg [monoid.fg M] : algebra.finite_presentation R S :=
begin
  unfreezingI
  { rw monoid.fg_iff_submonoid_fg at _inst_5,
    rcases _inst_5 with ⟨s, hs⟩,
    revert M,
    revert S,},
  classical,
  apply finset.induction_on s,
  {intros,
  rw finset.coe_empty at hs,
  rw submonoid.closure_empty at hs,
  replace hs := eq.symm hs,
  rw submonoid.eq_bot_iff_forall at hs,
  suffices : function.bijective (algebra_map R S).to_function, by --Error: algebra_map R S can't find type class instance for `semiring S`
  { sorry, },
    sorry, },
  {sorry,},
end

[Andrew Yang]

Does an resetI after intros work? You need to reset the cache when adding new instances into the scope, or else the type class system cannot see it.

[Eric Wieser]

Or combine them to introsI

[Nikolas Kuhn]

Perfect, thanks!