golfing `a + b = 0 → a * c = 0 → b * c = 0`

Stream: new members

[Eric Wieser]

Can anyone come up with a way of doing this without needing conv?

example {α : Type*} [semiring α] (a b c : α)
  (h : a * b + b * a = 0) (h' : a * b * c = 0) : b * a * c = 0 :=
begin
  rw ← zero_add (_ * _),
  conv_lhs {rw ← h'},
  rw [← add_mul, h, zero_mul],
end

[Eric Wieser]

Or a simpler one:

lemma foo {α : Type*} [semiring α] (a b c : α)
  (h : a + b = 0) (h' : a * c = 0) : b * c = 0 :=
begin
  rw ← zero_add (_ * _),
  conv_lhs {rw ← h'},
  rw [← add_mul, h, zero_mul],
end

[Alex J. Best]

lemma foo {α : Type*} [semiring α] (a b c : α)
  (h : a + b = 0) (h' : a * c = 0) : b * c = 0 :=
begin
   apply_fun (* c) at h,
   simpa [add_mul, h'] using h,
end

[Mario Carneiro]

lemma foo {α : Type*} [semiring α] (a b c : α)
  (h : a + b = 0) (h' : a * c = 0) : b * c = 0 :=
by simpa [add_mul, h'] using congr_arg (* c) h

[Kenny Lau]

import tactic

lemma foo {α : Type*} [semiring α] (a b c : α)
  (h : a + b = 0) (h' : a * c = 0) : b * c = 0 :=
(zero_add _).symm.trans $ (congr_arg2 _ h'.symm rfl).trans $
(add_mul _ _ _).symm.trans $ (congr_arg2 _ h rfl).trans $ zero_mul _

[Johan Commelin]

It doesn't even use the dreaded black triangle!

[Eric Wieser]

I assume this lemma doesn't really deserve a place in mathlib?

[Mario Carneiro]

I miss lean 2, where you could do crazy things like

lemma foo {α : Type*} [semiring α] (a b c : α)
  (h : a + b = 0) (h' : a * c = 0) : b * c = 0 :=
!zero_add⁻¹ ▸ !add_mul⁻¹ ▸ h⁻¹ ▸ !zero_mul

that were real head scratchers on how that could possibly constitute a proof

[Johan Commelin]

What did the ! do?

[Mario Carneiro]

the opposite of @

[Mario Carneiro]

Eric Wieser said:

I assume this lemma doesn't really deserve a place in mathlib?

Maybe a + b = 0 -> (a = 0 <-> b = 0)?

[Mario Carneiro]

lemma bar {α : Type*} [add_monoid α] {a b : α} (h : a + b = 0) : a = 0 ↔ b = 0 :=
by split; rintro rfl; simpa using h

lemma foo {α : Type*} [semiring α] (a b c : α)
  (h : a + b = 0) (h' : a * c = 0) : b * c = 0 :=
(bar $ by simp [← add_mul, h]).1 h'

[Eric Wieser]

eq_zero_iff_eq_zero_of_add_eq_zero?

[Eric Wieser]

And the corresponding eq_one_iff_eq_one_of_mul_eq_one

[Eric Wieser]

#5169