left_cancel_semigroup ℝ

Stream: Is there code for X?

[Kunhao Zheng]

Hello! I wanna prove a simple algebra exercise like

import tactic.gptf
import data.real.basic
import data.real.nnreal
import data.real.sqrt
import data.complex.basic
import algebra.algebra.basic

example (b : ℝ) (h₁ : b > 0) (h₂ : 6*b=54/b) : b*b=9 :=
begin
  have key: (6*b)*b=(54/b)*b,
  {
    rw ← mul_right_inj b at h₂,
  },
end

and my first attemp is to multiply b at both end, but obviously lean is not happy and it requires

 failed to synthesize type class instance for
b : ℝ,
h₁ : b > 0,
h₂ : 6 * b = 54 / b
⊢ left_cancel_semigroup ℝ
state:
b : ℝ,
h₁ : b > 0,
h₂ : 6 * b = 54 / b
⊢ 6 * b * b = 54 / b * b

do you have any hint of that? Thank you a lot!

[Kevin Buzzard]

Your problem is that mul_right_inj is a theorem about groups (or more precisely about a structure which is slightly weaker than a group) and it says that you can always cancel anything.

[Kevin Buzzard]

You will need a lemma about fields (or maybe integral domains or something) saying that you can cancel anything as long as it's nonzero.

[Bhavik Mehta]

I think it might be mul_right_inj' that you want

[Kevin Buzzard]

but actually it would be easier just to work backwards and rewrite h2 on the goal -- often in Lean it's easier to go backwards than forwards.

[Eric Wieser]

have key : whatyouhave := congr_fun (* b) h should also produce key

[Kevin Buzzard]

A style issue: in Lean we prefer < always instead of > -- otherwise we have to write every lemma about inequalities twice. Your hypothesis h₁ should be 0 < b, it will be easier to use than b > 0.

[Kunhao Zheng]

Thank you for your help and advice! I finally managed to get it work like this,

import data.real.basic
import data.real.nnreal
import data.real.sqrt
import data.complex.basic
import algebra.algebra.basic


example (b : ℝ) (h₁ : 0 < b) (h₂ : 6*b=54/b) : b*b=9 :=
begin
  have key₁ : b ≠ 0 := ne_of_gt h₁,
  have key₃ :  6*b*b=54 := (eq_div_iff key₁).mp h₂,
  linarith,
end

[Kevin Buzzard]

Here's my solution:

import data.real.basic

example (b : ℝ) (h₁ : 0 < b) (h₂ : 6*b=54/b) : b*b=9 :=
begin
  rw eq_div_iff (ne_of_gt h₁) at h₂,
  linarith,
end

[Kevin Buzzard]

(generated independently but I now realise it's exactly the same!). My instinct is not to make new key variables because they just clutter things up.

[Kunhao Zheng]

that looks good! learnt a lot