IsLeftCancelMul ℝ

Stream: new members

[ZhiKai Pong]

import Mathlib

variable (f : ℝ → ℝ) (c : ℝ)

example (h : ∀ x, c * f x = 0) (hc : c ≠ 0): f x = 0 := by
  have h' : c * f x = c * 0 := by
    rw [h]
    simp
  apply mul_left_cancel at h'
  exact h'
  -- goal: IsLeftCancelMul ℝ

I have this example which ends up with this goal and I don't know how to proceed or what am I missing.
I guess I would also like to ask is there a simpler way to do this e.g. without needing to define h'

[Ruben Van de Velde]

mul_left_cancel doesn't work if you have a zero; you need mul_left_cancel\0