Multiplying both sides of an expression by a constant

Stream: new members

[ROCKY KAMEN-RUBIO]

MWE
Is there an automated way to do stuff like this? The best I can think of is to prove 2!= 0, multiply both sides by 2, rw mul_add, mul_sub, add_mul, add_sub a bunch of times, then prove 2*(1/2) = 1 and apply that with some other algebra. I feel like there should be a faster way I'm missing.

example (a b c d e f g : ℝ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
sorry,
end

More Context
I'm having trouble massaging this identity to prove Binet's formula for the Fibonacci numbers.

import data.real.basic
import data.nat.basic
import data.nat.fib
import tactic
noncomputable theory
def phi : ℝ := ((1 + real.sqrt 5) / 2)
def psi : ℝ := ((1 - real.sqrt 5) / 2)

lemma psi_phi_identity (k : ℕ) : phi ^ k - psi ^ k + (phi ^ (k + 1) - psi ^ (k + 1)) = phi ^ (k + 2) - psi ^ (k + 2) :=
begin
induction k with n hn,
{simp only [pow_one, zero_add, pow_zero, sub_self],
rw phi,
rw psi,
rw pow_succ,
simp only [div_pow, pow_one, mul_add, add_mul],
sorry,},
sorry,
end

[Matt Earnshaw]

how about:

example (a b c d e f g : ℝ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
  field_simp,
  rw ← add_assoc,
  rw h,
  ring,
end

[Matt Earnshaw]

sadly not of great generality

[Kevin Buzzard]

Here are some thoughts on Binet's formula which might end up in Mathematics in Lean at some point.

[Mario Carneiro]

example (a b c d e f g : ℝ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
  apply_fun (λ x, x/2) at h,
  convert h; ring,
end

[Kevin Buzzard]

hey, where is the ring++ usage??

[Mario Carneiro]

that works too:

example (a b c d e f g : ℝ) (h : a + b + c = d - e + f - g) : a/2 + b/2 + c/2 = d/2 - e/2 + f/2 - g/2 :=
begin
  ring_rw [h / 2],
end

[Mario Carneiro]

modulo the existence of the tactic

[Reid Barton]

Mario Carneiro said:

modulo the existence of the tactic

Now you are proving like a mathematician!

[Johan Commelin]

The tactic is left as an exercise for the reader

[Kevin Buzzard]

Of course Mochizuki also left a tactic as an exercise for the reader, and it's stumped Scholze.

[Patrick Massot]

What happened to rumors of Mochizuki's work being published?

[Johan Commelin]

Last thing I heard, it happened.

[Johan Commelin]

Peter Woit had a long discussion on his blog, and he summarised it in some 40 page pdf

[Kevin Buzzard]

PRIMS announced they were going to do it