Need help understanding why it doesn't unify

Stream: new members

[Kevin Cheung]

The following should be easy but I have no idea why Lean is stuck:

import Mathlib.Data.Real.Basic

example (a b c : ℝ) (h : b ≠ 0) : a / b = c → a = b * c := by
  intro g
  apply eq_mul_of_div_eq

The error is:

tactic 'apply' failed, failed to unify
  ?a = ?b * ?c
with
  a = b * c
a b c: ℝ
h: b ≠ 0
g: a / b = c
⊢ a = b * c

Lean is saying that the following about expected type:

a b c: ℝ
h: b ≠ 0
g: a / b = c
⊢ ∀ {G : Type ?u.168} [inst : Group G] {a b c : G}, a / c = b → a = b * c

Why couldn't Lean unify? Is it because ℝ is not an instance of Group? Any help on how to proceed greatly appreciated.

[Damiano Testa]

eq_mul_of_div_eq requires working with a (multiplicative) Group, but Real under multiplication is not, because of 0.

[Kevin Cheung]

Right. So how does one prove that example?

[Damiano Testa]

example (a b c : ℝ) (h : b ≠ 0) : a / b = c → a = b * c := by
  intro g
  rwa [div_eq_iff h, mul_comm] at g

[Kevin Cheung]

All right. I have a proof. But is there a shorter way?

example (a b c : ℝ) (h : b ≠ 0) : a / b = c → a = c * b := by
  intro g
  rw [div_eq_mul_inv] at g
  rw [← g]
  rw [mul_assoc]
  rw [mul_comm b⁻¹]
  rw [mul_inv_cancel]
  rw [mul_one]
  exact h

[Kevin Cheung]

Thank you.

[Kevin Cheung]

I guess I just didn't know how to search for such a result.

[Damiano Testa]

Remembering that the LHS is supposed to be "harder" than the RHS, a reasonable guess is that the lemma in mathlib will convert a division into a multiplication. So, I started looking for div_eq|Ctrl Space...

[Kevin Cheung]

Thanks for the tip.