Typeclass instance problem is stuck here

Stream: new members

[Jeremy Tan]

How do I fix the error in the last line below?

import Mathlib.RingTheory.Localization.FractionRing
import Mathlib.RingTheory.Localization.Integer
import Mathlib.RingTheory.UniqueFactorizationDomain

variable {R : Type _} [CommRing R] (M : Submonoid R) {S : Type _} [CommRing S]

variable [Algebra R S] {P : Type _} [CommRing P]

open IsLocalization

variable (A : Type _) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A]

variable {K : Type _} [Field K] [Algebra A K] [IsFractionRing A K]

theorem exists_reduced_fraction (x : K) :
    ∃ (a : A)(b : nonZeroDivisors A), (∀ {d}, d ∣ a → d ∣ b → IsUnit d) ∧ mk' K a b = x :=
    sorry

noncomputable def num (x : K) : A :=
  Classical.choose (exists_reduced_fraction A x)

noncomputable def denom (x : K) : nonZeroDivisors A :=
  Classical.choose (Classical.choose_spec (exists_reduced_fraction A x))

@[simp]
theorem mk'_num_denom (x : K) : mk' K (num A x) (denom A x) = x :=
  (Classical.choose_spec (Classical.choose_spec (exists_reduced_fraction A x))).2

variable {A}

theorem num_mul_denom_eq_num_mul_denom_iff_eq {x y : K} :
    num A y * denom A x = num A x * denom A y ↔ x = y := -- the error is in mk'_eq_of_eq' h below
  ⟨fun h => by simpa only [mk'_num_denom] using mk'_eq_of_eq' h, fun h => by rw [h]⟩

[Jeremy Tan]

The error being

typeclass instance problem is stuck, it is often due to metavariables
  IsLocalization (nonZeroDivisors A) ?m.10189

[Jeremy Tan]

So in this tactic state

R: Type ?u.102398
inst✝⁹: CommRing R
M: Submonoid R
S: Type ?u.102498
inst✝⁸: CommRing S
inst✝⁷: Algebra R S
P: Type ?u.102758
inst✝⁶: CommRing P
A: Type u_1
inst✝⁵: CommRing A
inst✝⁴: IsDomain A
inst✝³: UniqueFactorizationMonoid A
K: Type u_2
inst✝²: Field K
inst✝¹: Algebra A K
inst✝: IsFractionRing A K
xy: K
h: num A y * ↑(denom A x) = num A x * ↑(denom A y)
⊢ mk' ?m.104168 (num A x) (denom A x) = mk' ?m.104168 (num A y) (denom A y)

I want to put S into the place of ?m.104168 but I don't know how

[Adam Topaz]

theorem num_mul_denom_eq_num_mul_denom_iff_eq {x y : K} :
    num A y * denom A x = num A x * denom A y ↔ x = y :=
  ⟨fun h => by simpa only [mk'_num_denom] using mk'_eq_of_eq' (S := K) h, fun h => by rw [h]⟩

[Adam Topaz]

This is a new feature in lean4, where you can fill in implicit variables with (_ := _). In lean3 you would have had to write @mk'_eq_of_eq' with a bunch of underscores.