multiply LHS and RHS by two

Stream: new members

[Nicholas Wilson]

Silly question: how do I multiply the left and right hand sides of a proposition by 2?

I'm trying to get a proof for sin (ω * x) * sin (ω * y) = (cos ( ω *(x - y))-cos (ω * (x + y)))/2, I have so far

example (ω x y :ℝ ) : 2 * sin (ω * x) * sin (ω * y) = (cos ( ω *(x - y))-cos (ω * (x + y))) := by
  ring_nf
  simp only [cos_add,cos_sub]
  simp
  rw [mul_two]

[Nicholas Wilson]

also how do I solve

example (a b : ℝ ): (a*2) +(b*2)/4 = (a+b)/2 := by sorry

simp failed. ring does work, but as a tactic converts (1/2) to (↑(Int.ofNat 1) / ↑2) (or (↑(Int.negOfNat 1) / ↑2 depending on the sign. Is there a different tactic that will work here other than ring (which for the above reasons I'd prefer to avoid)?

[Shreyas Srinivas]

example (a b : ℝ ): (a*2) +(b*2)/4 = (a+b)/2 := by
  field_simp
  ring
  done -- error here. From the tactic state, you can see the claim is wrong.

[Nicholas Wilson]

argh, I forgot to recopy the corrected parens, sorry. example (a b : ℝ ): ((a*2) +(b*2))/4 = (a+b)/2 := by ring was what I meant.

[Shreyas Srinivas]

Then the example is complete:

import Mathlib.Tactic

example (a b : ℝ ): ((a*2) +(b*2))/4 = (a+b)/2 := by
  field_simp
  ring
  done

[Shreyas Srinivas]

If you want to avoid typing in field_simp followed by ring many times, you can use a simple macro:

import Mathlib.Tactic

macro "field" : tactic => do
  `(tactic|(
      field_simp
      ring_nf
  ))
example (a b : ℝ ): ((a*2) +(b*2))/4 = (a+b)/2 := by
  field
  done

[Nicholas Wilson]

Thanks. For some reason field_simp works fine on live.lean-lang.org, but locally I get unexpected identifier; expected command. The imports are the same.

[Ruben Van de Velde]

Are you on a particularly old version of mathlib?

[Nicholas Wilson]

I _ believe_ I am on 4.3-rc1.

[Nicholas Wilson]

Is there a way to check (I'm using VSCode, not the command line).

[Ruben Van de Velde]

That's a lean version, not a mathlib version. I'm on mobile right now, so can't check how to figure it out in detail

[Shreyas Srinivas]

check the imports.

[Kyle Miller]

Nicholas Wilson said:

Is there a way to check (I'm using VSCode, not the command line).

#eval Lean.versionString

[Kyle Miller]

Shreyas Srinivas said:

Then the example is complete:

import Mathlib.Tactic

example (a b : ℝ ): ((a*2) +(b*2))/4 = (a+b)/2 := by
  field_simp
  ring
  done

Linarith knows how to cancel denominators if they're constants.

example (a b : ℝ ): ((a*2) +(b*2))/4 = (a+b)/2 := by
  linarith

[Nicholas Wilson]

Thanks, I can confirm I am on Lean "4.3.0-rc1", but as noted that is not a Mathlib version

[Nicholas Wilson]

Silly question: can you not use linarith in a conv?

...
conv =>
  enter [1,2];ext;enter [2]; ext;
  enter [2]
  conv =>
    enter [1]
    ring_nf
  linarith

fails with unexpected identifier; expected command, replacing linarith with simp or ring_nf "works" (but doesn't do what I want)

example : ... := by linarith

works (assuming the example can be proved by linarith), in the same file.

[Shreyas Srinivas]

How did you set up the project?

[Shreyas Srinivas]

Is Mathlib available as a dependency?

(Also : linarith is not a conv tactic so that is expected)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Nicholas Wilson]

How did you set up the project?

I think it was "create a Mathlib dependent VSCode project", with a VSCode wizard for the configuration. I have Mathllib as a dependency of that project.

[Shreyas Srinivas]

Okay, in that case, if you still have this import issue, I suggest raising it in a fresh thread. I just checked the setup and it works for me. Do make sure that you are not trying to create the project in a folder that already contains a lean project.