lcm and divisors

Stream: Is there code for X?

[Xavier Xarles]

I wrote a proof for the following lemma, but I am sure it can be done in a shorter way. Any help will be appreciated

import number_theory.divisors

lemma lcm_divisors (n: nat)(H0: n ≠ 0):  ∀ (a b : nat),
a ∈ n.divisors → b ∈ n.divisors → (a.lcm b) ∈  n.divisors :=
begin
  intros a b ha hb,
  rw nat.mem_divisors,
  split,
  rw nat.lcm_dvd_iff,
  split,
  rw nat.mem_divisors at ha,
  cases ha with Ha, exact Ha,
  rw nat.mem_divisors at hb,
  cases hb with Hb, exact Hb,
  exact H0,
end

[Kyle Miller]

I didn't check if there were any other mathlib lemmas that could help, but here's a compressed version of your proof:

lemma lcm_divisors (n : nat) (H0 : n ≠ 0) (a b : nat) (ha : a ∈ n.divisors) (hb : b ∈ n.divisors) :
  (a.lcm b) ∈ n.divisors :=
begin
  simp only [nat.mem_divisors, nat.lcm_dvd_iff] at ha hb ⊢,
  exact ⟨⟨ha.1, hb.1⟩, ha.2⟩,
end

This would probably be the mathlib name and implicit argument style:

lemma lcm_mem_divisors {n : ℕ} (H0: n ≠ 0) {a b : ℕ}
  (ha : a ∈ n.divisors) (hb : b ∈ n.divisors) : (a.lcm b) ∈ n.divisors :=
begin
  simp only [nat.mem_divisors, nat.lcm_dvd_iff] at ha hb ⊢,
  exact ⟨⟨ha.1, hb.1⟩, ha.2⟩,
end

[Yaël Dillies]

Maybe a version of this where you take a ∣ c, b ∣ c instead would be useful too?

[Xavier Xarles]

Thanks, I am learning to write in a more compressed way.
I am not sure of the meaning of ⊢ at the proof at the end of the simp only.

[Yaël Dillies]

Many tactics can work on locations. You can either refer to an hypothesis by its name or to the goal using ⊢.

[Patrick Johnson]

Assumption (H0 : n ≠ 0) is redundant. The proof can be even shorter:

import number_theory.divisors

lemma lcm_mem_divisors {n : ℕ} {a b : ℕ}
  (ha : a ∈ n.divisors) (hb : b ∈ n.divisors) : a.lcm b ∈ n.divisors :=
by simp [nat.lcm_dvd_iff, *] at *

[Eric Wieser]

I think the real takeaway here is that a ∈ n.divisors is not the preferred spelling, which is why we have no lemmas about it

[Eric Wieser]

You're expected to use docs#nat.mem_divisors_iff first

[Kevin Buzzard]

@Xavier Xarles in formalising it really helps if there is one "canonical way" to express an idea, and n \| m is the canonical way to say n divides m, not n \in divisors m