Can't inline lemma to rw

Stream: lean4

[Bolton Bailey]

MWE:

import Mathlib.RingTheory.IntegralDomain
import Mathlib.FieldTheory.Finite.Basic

open scoped Classical

theorem Polynomial.sum_eval_eq_iff' {F : Type} [Field F] [Fintype F]  {G : Subgroup (Units (F))} (σ : F) :
    σ = (Fintype.card G) * (σ / (Fintype.card G)) := by

  -- rw [mul_div_cancel' (FiniteField.card_cast_subgroup_card_ne_zero G)]
  -- -- did not find instance of the pattern in the target expression

  rw [mul_div_cancel']
  exact FiniteField.card_cast_subgroup_card_ne_zero G
  -- works fine

Why can I not do the first one?

[Matthew Ballard]

rw [mul_div_cancel' _ (FiniteField.card_cast_subgroup_card_ne_zero G)]

[Bolton Bailey]

Thank you, I'm dumb.

[Matthew Ballard]

Just ambitious :)

[Bolton Bailey]

Wait I'm still confused

[Bolton Bailey]

Why is the first one not a type error then?

[Matthew Ballard]

It looks like Lean tries to make sense of that as (a : ?G0)

[Bolton Bailey]

If I do have := mul_div_cancel' (FiniteField.card_cast_subgroup_card_ne_zero G) it gives

typeclass instance problem is stuck, it is often due to metavariables
  CommGroupWithZero ?m.1195

Why isn't that the error I see in my example?

[Matthew Ballard]

It appears if you trace the output with trace.Meta.isDefEq

[Bolton Bailey]

It seems to me I shouldn't have to do a fancy trace to see that if this is the problem

[Eric Wieser]

I think in the context of rw, stuck TC problems are allowed and resolved later

[Eric Wieser]

But it's still weird that that example gets that far, because it looks like there's a universe issue long before a typeclass issue