∀ {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} [inst : AddCommMonoid M] [inst_1 : Semiring R]
  [inst_2 : Module R M] [inst_3 : Semiring R₁] [inst_4 : Module R₁ M] [inst_5 : Semiring R₂] [inst_6 : Module R₂ M]
  {l₁ l₂ : Mathlib.Tactic.Module.NF R M} {l₁' : Mathlib.Tactic.Module.NF R₁ M} {l₂' : Mathlib.Tactic.Module.NF R₂ M}
  {x₁ x₂ : M}, x₁ = l₁'.eval → x₂ = l₂'.eval → l₁.eval = l₁'.eval → l₂.eval = l₂'.eval → l₁.eval = l₂.eval → x₁ = x₂