Help with a problem in Mathematics in Lean

Stream: new members

[debord]

Hello. I've been working through Mathematics in Lean, though using Lean 4 instead of Lean 3. So far so good until the proof of sum_sqr on page 74. The proof proceeds basically the exact same way as the proof before it does, however it seems that the symmetry tactic does not exist in mathlib4. Here is what I have:

theorem sum_sqr (n : ℕ) : ∑ i in Finset.range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_range_succ, ih, Nat.succ_eq_add_one]
    ring_nf

This brings me a pretty complicated expression as a goal: 1 + n * 2 + n ^ 2 + (n + n ^ 2 * 3 + n ^ 3 * 2) / 6 = (6 + n * 13 + n ^ 2 * 9 + n ^ 3 * 2) / 6. linarith or other tactics do not seem to be capable of tackling this. When I try to verify this on paper, I make use of the identity a / b + c / d = ad + bc / bd, writing n ^ 2 as n^ 2 / 1 etc., but apparently the version of this in mathlib4, div_add_div, cannot be used in my goal, because I get failed to synthesize instance Semifield ℕ, which I assume means that ℕ is not a semifield, and I can't find a version of adding fractions for ℕ to articulate what I'm trying to do. Am I approaching this completely wrong? Is there an equivalent for the symmetry tactic in mathlib4 so that the proof can work as expected? Thanks for your time.

[Ruben Van de Velde]

symmetry is now symm, I think

[debord]

Genius! Thank you Ruben.

[Kevin Buzzard]

I really discourage my students from writing lemmas like that. It doesn't represent what a mathematician means by $\sum_{i=0}^ni^2=n(n+1)(2n+1)/6$ because the division on naturals is pathological. I argue that if you want to use division you should coerce to rationals, where the division is non-pathological.

import Mathlib

open BigOperators

theorem sum_sqr (n : ℕ) : ∑ i in Finset.range (n + 1), (i : ℚ) ^ 2 = (n : ℚ) * (n + 1) * (2 * n + 1) / 6 := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_range_succ, ih, Nat.succ_eq_add_one]
    push_cast
    ring

works fine

[Eric Wieser]

The problem with the rat version is that you can't use it to rewrite statements about nat. So it's sometimes worth proving both.

[Kevin Buzzard]

Fortunately the nat statement involves natural division so you never want to rewrite it ;-)

[Eric Wieser]

The LHS doesn't...