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

[Heather Macbeth]

Or:

import Mathlib
example (a b : ℝ) (ha : a ≠ 0) (h : a * b - a = 0) : b = 1 := by
  linear_combination (norm := field_simp) a⁻¹ * h

[Rado Kirov]

not the shortest or best solution (requires copying the expression and manupulating it), but putting out there for completeness. If there was some way to say use h.lhs term here it would have made it better.

example (a b : ℝ) (ha : a ≠ 0) (h : a * b - a = 0) : b = 1 := by
  rw [show a * b - a = a * (b - 1) by ring] at h
  simp [ha] at h
  linarith

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 [show a * a * b * c - a * b * d = a * b * (a * c - d) by ring] at h
  simp [ha, hb] at h
  linarith