show trivial distributive law

Stream: new members

[Asei Inoue]

import Mathlib.Tactic

@[ext]
structure Point : Type where
  x : Int
  y : Int
  z : Int

namespace Point

def add (a b : Point) : Point :=
  ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

instance : Add Point where
  add := add

def smul (r : Int) (a : Point) : Point where
  x := r * a.x
  y := r * a.y
  z := r * a.z

instance : HSMul Int Point Point where
  hSMul r a := smul r a

theorem smul_distrib (r : Int) (a b : Point) :
    (r • a) + (r • b) = r • (a + b) := by
  ext <;> sorry -- How to show this?

[Yaël Dillies]

Add lemmas of the form @[simp] lemma x_add (a b : Point) : (a + b).x = a.x + b.x := rfl (and same for •), then your proof will just be simp [mul_add]

[Asei Inoue]

There is clearly symmetry in the definition of Point.add, but can it be exploited and automated?

[Eric Wieser]

@[simps] on the instance and on add would generate the lemmas for you, but with terrible names