[Merged by Bors] - feat(algebra/big_operators/basic): add lemma finset.prod_dvd_prod

[stuart-presnell]

For any S : finset α, if ∀ a ∈ S, g1 a ∣ g2 a then S.prod g1 ∣ S.prod g2.

---

[eric-wieser]

Suggested change

	apply finset.induction_on' S, { simp },
	induction S using finset.induction_on' with a T haS _ haT IH,
	{ simp },

[eric-wieser]

Although I think you might not need the primed version here based on the _ in your intros below.

[stuart-presnell]

I can get this to work with the unprimed version, although the proof then becomes a bit longer:

lemma prod_dvd_prod {S : finset α} (g1 g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) :
  S.prod g1 ∣ S.prod g2 :=
begin
  classical,
  induction S using finset.induction_on with a T haT h1, { simp },
  repeat {rw finset.prod_insert haT},
  apply mul_dvd_mul,
  { apply h, simp },
  { refine h1 (λ x hx, _), simp [h, mem_insert_of_mem hx] },
end

However, if I try using the primed version as you first suggested I immediately and consistently get Server has stopped due to signal SIGSEGV as soon as the compiler hits that line. Any idea what's going wrong here, or should I just ask on Zulip?

[eric-wieser]

If you reliably get a sigsegv, then I'd push the broken version and ask on zulip what's going on.

[stuart-presnell]

Hmm, just as mysteriously I'm no longer getting the SIGSEGV at all and I can't reproduce it.

Now induction S using finset.induction_on' just gives induction tactic failed, failed to create new goal (which is also strange, given that apply finset.induction_on' S does work).

[eric-wieser]

Well, the style guide wants

Suggested change

	apply finset.induction_on' S, { simp },
	apply finset.induction_on' S,
	{ simp },

Which means my spelling is fewer lines that the version matching the style

[stuart-presnell]

Really? I understood the style guide to say that it's ok to immediately close a trivial goal on the same line, and it explicitly gives the example of induction n, { simp }. A quick search turns up lots of examples of induction ..., { simp... on a single line (and several with apply or refine).

[stuart-presnell]

And although your version is fewer lines, I can't find a way to get it to work in fewer characters since, as I noted above, induction S using finset.induction_on' doesn't seem to work for some reason, while induction S using finset.induction_on produces a longer proof.

[jcommelin]

I think we've always taken a pretty pragmatic approach to that aspect of the style guide.
Arguable the induction .. with .. shares more semantic information than the generic apply. But I wouldn't get hung up over this.

[stuart-presnell]

Ok, thanks. So is the proof ok as it stands (in this respect, at least)?

[robertylewis]

LGTM!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests