The stupid way to prove the divisibility of sums

Stream: new members

[agro1986]

Hi all. So, I proved that if d|a, d|b, then for any integers m, n, I have d | (ma + nb)

import tactic.ring
variables {a b c d: ℤ}
def divides (a b: ℤ): Prop := ∃(d: ℤ), b = a * d

theorem divides_linear_sum (hda: divides d a) (hdb: divides d b):
  ∀ (m n: ℤ), divides d (m * a + n * b) :=
begin
  assume m, assume n,
  cases hda with q hq,
  cases hdb with r hr,
  use m * q + n * r,
  rw [hq, hr],
  ring,
end

Now "obviously" this holds for the special case m = n = 1. However I couldn't write the proof in a concise way.

theorem divides_sum (hda: divides d a) (hdb: divides d b):
  divides d (a + b) :=
have h : divides d (1 * a + 1 * b), from divides_linear_sum hda hdb 1 1,
have simplify: 1 * a + 1 * b = a + b, from
  begin
    ring,
  end,
simplify ▸ h

I thought I could proof it in 1 step using divides_linear_sum hda hdb 1 1. The problem was, when I gave divides_linear_sum hda hdb 1 1 I got divides d (1 * a + 1 * b) which isn't the same as divides d (a + b) syntactically. Any pointers (like how to write it concisely in tactics mode)? Thanks!

[Kenny Lau]

theorem divides_sum (hda: divides d a) (hdb: divides d b):
  divides d (a + b) :=
by convert divides_linear_sum hda hdb 1 1; rw one_mul

[Kenny Lau]

theorem divides_sum (hda: divides d a) (hdb: divides d b):
  divides d (a + b) :=
by simpa only [one_mul] using divides_linear_sum hda hdb 1 1

[agro1986]

wow thanks! everyone's a wizard here :)

[Kevin Buzzard]

It's just practice. After a while your head ends up full of tricks

[Johan Commelin]

@agro1986 Btw, did you know that you can replicate the notation $a | b$ in Lean?