a simp question

Stream: new members

[mathnoter]

I am trying to prove the following statement in Lean:

example (a b : ℝ) (ha : a ≠ 0) (h : a * b - a = 0) : b = 1 := by
  sorry

I would like to know how to complete this proof using tactics like field_simp and ring (or any other suitable tactics) for a direct and concise solution, rather than a step-by-step manual manipulation. Could someone provide guidance on how to achieve this?

Thank you!

[Ruben Van de Velde]

import Mathlib
example (a b : ℝ) (ha : a ≠ 0) (h : a * b - a = 0) : b = 1 := by
  rw [sub_eq_zero] at h
  field_simp at h
  assumption

[Mauricio Collares]

Not as good, but:

import Mathlib
example (a b : ℝ) (ha : a ≠ 0) (h : a * b - a = 0) : b = 1 :=
  mul_right_injective₀ ha (by linarith : a * b = a * 1)

[mathnoter]

Mauricio Collares said:

Not as good, but:

import Mathlib
example (a b : ℝ) (ha : a ≠ 0) (h : a * b - a = 0) : b = 1 :=
  mul_right_injective₀ ha (by linarith : a * b = a * 1)

Thank you for your response! I appreciate the solution. To further enhance my understanding, could you please provide another example using similar techniques? Specifically, I am trying to prove the following statement:

example (a b c d : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (h : a * a * b * c - a * b * d = 0) : a * c = d := by
  sorry

Thank you!

[Mauricio Collares]

import Mathlib
example (a b c d : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (h : a * a * b * c - a * b * d = 0) : a * c = d := by
  rw [sub_eq_zero] at h
  apply_fun (· / (a * b)) at h
  convert h using 1 <;> field_simp
  ring

or maybe

import Mathlib
example (a b c d : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (h : a * a * b * c - a * b * d = 0) : a * c = d := by
  rw [sub_eq_zero] at h
  rw [← mul_right_inj' (by field_simp : a * b ≠ 0)]
  convert h using 1
  ring

[Ruben Van de Velde]

Or:

import Mathlib
example (a b c d : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (h : a * a * b * c - a * b * d = 0) : a * c = d := by
  apply mul_left_cancel₀ (by positivity : a * b ≠ 0)
  linarith