simplifying proves

Stream: new members

[ShaoYu]

apply Finset.sum_eq_zero
 intro k hk
 simp only [Finset.mem_range] at hk
 rw [ih (by linarith)]

How can I simplify these code to make it conform to mathlib4?Thanks!

[Kenny Lau]

it's a bit hard to test if you don't give me #mwe

exact Finset.sum_eq_zero fun k hk ↦ have := Finset.mem_range.1 hk; (ih (by linarith)).trans _

[ShaoYu]

sorry,these are the complete proof processes. I would like to simplify them with the goal of eventually merging into mathlib.

theorem fwdDiff_iter_pow_lt {x j n : ℕ} (h : j < n):
  Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦  0) x := by
  revert j
  induction' n with n IH
  · simp only [not_lt_zero', Function.iterate_zero, id_eq,
      IsEmpty.forall_iff, implies_true]
  · intro j hj
    rw [Function.iterate_succ, Function.comp_apply, fwdDiff_iter_eq_sum_shift]
    simp only [Int.reduceNeg, smul_eq_mul, mul_one, zsmul_eq_mul, Int.cast_mul,
      Int.cast_pow, Int.cast_neg, Int.cast_one, Int.cast_natCast]
    simp [fwdDiff_iter_eq_sum_shift] at IH
    conv_lhs=> enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,
      ← Nat.cast_pow,← Nat.cast_sub (by apply Nat.pow_le_pow_left; linarith),
      add_pow, Finset.sum_range_succ]
    simp only [one_pow, mul_one, Nat.cast_id,
      tsub_self, pow_zero, Nat.choose_self, Nat.cast_one]
    conv_lhs=> enter[2]; ext k; rw [Nat.add_sub_cancel_right (m := (x + k) ^ j),
      mul_assoc, ← Nat.cast_mul, Finset.mul_sum]
    norm_num
    simp [Finset.mul_sum, Finset.sum_comm, ← mul_assoc, ← mul_assoc, ← Finset.sum_mul]
    apply Finset.sum_eq_zero
    intro x_1 a
    simp_all only [mem_range]
    rw [IH (by linarith)]
    simp

[Kenny Lau]

#mwe

[Kenny Lau]

in any case, you don't need to worry about making your proof "mathlib compliant" until you make a PR, tho it would certainly be good practice

[Kenny Lau]

right now, the biggest issue (again, it's an issue only if you want to PR) is the non-terminal simp

[Kenny Lau]

i.e. a simp that is not the last step of a goal/subgoal

[Kenny Lau]

to fix that, make simp into simp? and then click the blue text to make it simp only

[ShaoYu]

okok, I will change it.Then an error occurred when replacing this code at the fourth last line with yours

 apply Finset.sum_eq_zero
    intro x_1 a
    simp_all only [mem_range]
    rw [IH (by linarith)]

[Kenny Lau]

don't replace it then; as I told you, I can't test it because it's not an #mwe

[Kevin Buzzard]

(click on the link to discover what Kenny means)

[Kevin Buzzard]

(click on the link to discover what Kenny means)

[ShaoYu]

import Mathlib

open Finset Nat Std List

open fwdDiff
variable {R : Type*} [CommRing R]

open Finset Nat Function

theorem fwdDiff_iter_pow_lt {x j n : ℕ} (h : j < n):
  Δ_[1] ^[n] (fun x ↦ x ^ j : ℕ → R) x = (fun _ ↦  0) x := by
  revert j
  induction' n with n ih
  · simp only [not_lt_zero', Function.iterate_zero, id_eq,
      IsEmpty.forall_iff, implies_true]
  · intro j hj
    rw [Function.iterate_succ, Function.comp_apply, fwdDiff_iter_eq_sum_shift]
    simp only [Int.reduceNeg, smul_eq_mul, mul_one, zsmul_eq_mul, Int.cast_mul,
      Int.cast_pow, Int.cast_neg, Int.cast_one, Int.cast_natCast]
    simp [fwdDiff_iter_eq_sum_shift] at ih
    conv_lhs=> enter[2]; ext k; enter[2]; rw [fwdDiff, ← Nat.cast_pow,
      ← Nat.cast_pow,← Nat.cast_sub (by apply Nat.pow_le_pow_left; linarith),
      add_pow, Finset.sum_range_succ]
    simp only [one_pow, mul_one, Nat.cast_id,
      tsub_self, pow_zero, Nat.choose_self, Nat.cast_one]
    conv_lhs=> enter[2]; ext k; rw [Nat.add_sub_cancel_right (m := (x + k) ^ j),
      mul_assoc, ← Nat.cast_mul, Finset.mul_sum]
    norm_num
    simp [Finset.mul_sum, Finset.sum_comm, ← mul_assoc, ← mul_assoc, ← Finset.sum_mul]
    apply Finset.sum_eq_zero
    intro k hk
    simp at hk
    rw [ih (by linarith)]
    simp only [zero_mul]

I got it, is this means?

[Kenny Lau]

@ShaoYu that works, yes, now you can replace those lines with:

exact Finset.sum_eq_zero fun k hk ↦ have _ := Finset.mem_range.1 hk; by simp [ih (by linarith)]

[Kenny Lau]

but I'm not sure if you understood my other messages

[ShaoYu]

I’m starting to get it now.We have already submitted two PRs #26790 #26793and are actively working on revisions to meet the standards for merging into Mathlib. Thank you for your attention, and we warmly welcome any further suggestions!