## Stream: new members

### Topic: multiply LHS and RHS by two

#### Nicholas Wilson (Nov 25 2023 at 10:20):

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
rw [mul_two]


#### Nicholas Wilson (Nov 25 2023 at 12:04):

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 (Nov 25 2023 at 12:05):

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 (Nov 25 2023 at 12:07):

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 (Nov 25 2023 at 12:10):

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 (Nov 25 2023 at 12:12):

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 (Nov 25 2023 at 12:15):

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 (Nov 25 2023 at 12:17):

Are you on a particularly old version of mathlib?

#### Nicholas Wilson (Nov 25 2023 at 12:21):

I _ believe_ I am on 4.3-rc1.

#### Nicholas Wilson (Nov 25 2023 at 12:22):

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

#### Ruben Van de Velde (Nov 25 2023 at 12:23):

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 (Nov 25 2023 at 12:29):

check the imports.

#### Kyle Miller (Nov 25 2023 at 17:10):

Nicholas Wilson said:

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

#eval Lean.versionString

#### Kyle Miller (Nov 25 2023 at 17:13):

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 (Nov 25 2023 at 23:39):

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

#### Nicholas Wilson (Nov 25 2023 at 23:44):

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 (Nov 26 2023 at 12:37):

How did you set up the project?

#### Shreyas Srinivas (Nov 26 2023 at 12:37):

Is Mathlib available as a dependency?

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

(deleted)

(deleted)

#### Nicholas Wilson (Nov 26 2023 at 22:59):

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 (Nov 27 2023 at 06:44):

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.

Last updated: Dec 20 2023 at 11:08 UTC