using mul_right_cancel

Stream: new members

[JK]

Can someone help with the syntax for using mul_right_cancel? Here is what I would like to prove:

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 := by

It seems obvious to try to use

mul_right_cancel₀

here, but I can't seem to get the syntax right

[Kenny Lau]

import Mathlib

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 := by
  rw [mul_left_inj'] at h2
  · exact h2
  · exact h1

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 := by
  exact mul_right_cancel₀ h1 h2

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 :=
  mul_right_cancel₀ h1 h2

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 := by
  apply mul_right_cancel₀ at h2
  · exact h2
  · exact h1

[Aaron Liu]

apply?

[Kenny Lau]

import Mathlib

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 := by
  apply mul_right_cancel₀
  · exact h1
  · exact h2

[Kim Morrison]

import Mathlib

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 := by
  try?

[suhr]

import Mathlib

example (s t : ℚ) (h1 : s ≠ 0) (h2 : t*s = 3*s) : t = 3 :=
  mul_right_cancel₀ h1 h2