Having trouble with types

Stream: new members

[Colin Jones ⚛️]

Hi I'm having trouble proving this because of type issues:

import Mathlib

open BigOperators Finset

example : ∑ i in range (n+1), i = n*(n + 1)/2 := by
  induction n
  -- n = 0 case
  · norm_num
  · rename_i n hn
    rw [succ_eq_add_one]
    rw [show n + 1 + 1 = n + 2 by rw [Nat.add_right_cancel_iff]]
    have h : ∑ x in Finset.range (n + 2), x = (n + 1) + ∑ x in range (n + 1), x := by
      exact sum_range_succ_comm (fun x => x) (n + 1)
    rw [h, hn]; rify -- transforms prop to Real numbers because untrue in Nat
    rw [show (n:ℝ) = 2*n / 2 by field_simp; rw [mul_comm]]
    rw [show (1:ℝ) = 2/2 by field_simp]
    field_simp
    rw [show (((n:ℝ) * ((n:ℝ) + 1) / 2):ℝ) * (2:ℝ) = ((n:ℝ) * (n + 1)) by rify; field_simp]
sorry

[Richard Copley]

I'm not too sure the thing you have in the goal, ↑(↑n * (↑n + 1) / 2) * 2, and the thing you have on the left-hand side of the rw equation, ↑n * (↑n + 1) / 2 * 2, differ only by a matter of type. It can be proved that they're equivalent for all natural n, but that only gets you back to square one. Personally I would stay in the naturals and supply the necessary side-conditions for subtraction and division lemmas as they come up (sorry @Kevin Buzzard :smile:). For example,

import Mathlib.Tactic

set_option autoImplicit false

open BigOperators in
example (n : ℕ) : ∑ i in Finset.range (n + 1), i = n * (n + 1) / 2 := by
  induction n with
  | zero => norm_num
  | succ n ih =>
    symm
    apply Nat.div_eq_of_eq_mul_right two_pos
    rw [Finset.sum_range_succ, ih, Nat.succ_eq_add_one, mul_add 2]
    rw [show n + 1 + 1 = n + 2 by rw [Nat.add_right_cancel_iff]]
    have hle : 2 * (n + 1) ≤ (n + 1) * (n + 2) := by
      have : 0 < n + 1 := by
        rw [← Nat.succ_eq_add_one]
        exact Nat.zero_lt_succ n
      rw [mul_comm, mul_le_mul_left this]
      exact Nat.le_add_left 2 n
    have heven : 2 ∣ n * (n + 1) := by
      cases Nat.even_or_odd n with
      | inl h => exact h.two_dvd.mul_right _
      | inr h => exact (h.add_odd odd_one).two_dvd.mul_left _
    rw [← Nat.sub_eq_iff_eq_add hle, ← Nat.mul_div_assoc _ heven, eq_comm]
    apply Nat.div_eq_of_eq_mul_right two_pos
    rw [eq_comm, mul_tsub, Nat.sub_eq_iff_eq_add (Nat.mul_le_mul_left _ hle)]
    ring

[Colin Jones ⚛️]

Thank you. I also forgot how to properly setup an induction proof so that helps a lot

[Kevin Buzzard]

You set it up with typing induction n and then clicking on the yellow light bulb and then clicking on the thing that basically says "set this induction proof up for me"

[Jireh Loreaux]

@Richard Copley why not have the best of both worlds? Get the result for ℕ, but use ℚ to do it. Like this, with much less effort and checking of side conditions.

import Mathlib.Tactic

set_option autoImplicit false

open BigOperators in
example (n : ℕ) : ∑ i in Finset.range (n + 1), i = n * (n + 1) / 2 := by
  apply Nat.cast_injective (R := ℚ)
  rw [Nat.cast_div (even_iff_two_dvd.mp n.even_mul_succ_self) (by norm_num)]
  push_cast
  rw [eq_div_iff_mul_eq (by norm_num)]
  induction n with
  | zero => norm_num
  | succ n ih =>
    rw [Finset.sum_range_succ, add_mul, ih]
    simp
    ring

[Jireh Loreaux]

Or just stay in ℕ and get rid of the / 2 up front:

example (n : ℕ) : ∑ i in Finset.range (n + 1), i = n * (n + 1) / 2 := by
  symm
  rw [Nat.div_eq_iff_eq_mul_left (by norm_num) (even_iff_two_dvd.mp n.even_mul_succ_self)]
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [Finset.sum_range_succ, add_mul, ←ih, n.succ_eq_add_one]
    ring