Homework issue: Can the conditions in the MWE be extended?

Stream: general

[Jasin Jiang]

I am working on proving a theorem (goal), and the mathematical proof method I am using is shown in the diagram. I have written about 300 lines of Lean 4 code based on the proof method in the diagram. I realized that the range of hx​ in the previously written theorem (theorem Binomial_theorem') — 0<x<1 — conflicts with the range I am currently proving, which is 0≤k≤1. I want to rewrite the range of hx​ in the Binomial_theorem to extend it to 0≤x≤1, but I found that I am unable to prove that the equality holds when x=1.
Is there any way to solve this problem? Or is it the case that this mathematical proof cannot be reproduced in Lean 4? I have attached my code along with the minimal working example. I hope someone can help me.

This is the proof in nature language:
image.png

This is the #mwe that I expect to prove:

import Mathlib

open Nat
open Finset
open BigOperators

theorem Binomial_theorem' (n : ℕ) (x : ℝ) (hx : 0 <= x ∧ x <= 1) :
  ∑ k in Ico 1 (n + 1), (-1) ^ k * n.choose k * (1 - x) ^ (k - 1) = - ∑ k in Ico 1 (n + 1), x ^ (k - 1) := by

This is the whole Lean4 code that I have written (show that I am struggled with the range):
goal.lean

[Kevin Buzzard]

Given your recent posts, I am very unclear what is going on here. Are you asking the community to do your homework for you? PS can you change the title of this thread to something more helpful? Right now it conveys no useful information.

[Jasin Jiang]

Kevin Buzzard said:

Given your recent posts, I am very unclear what is going on here. Are you asking the community to do your homework for you? PS can you change the title of this thread to something more helpful? Right now it conveys no useful information.

Thank you for your suggestion. I have already updated the title. This is indeed an assignment for my Lean course. However, I believe that if I encounter something I can't figure out after thinking for a long time, it's important to ask for help. That's why I chose to post my question on the forum, hoping that kind people can offer me some advice on proving the theorem. I don't think this is a bad thing.

[Jasin Jiang]

If a problem has been bothering me for a time and I don't ask questions, how can I progress?

[Julian Berman]

It is a bad thing to ask for help with your homework without clearly indicating it is homework, such that people responding know not to give you answers to your problem but to instead point you to hints or tutorials such that you finish your own work yourself. Surely your university's ethics policy mentions this?

[Jasin Jiang]

Julian Berman said:

It is a bad thing to ask for help with your homework without clearly indicating it is homework, such that people responding know not to give you answers to your problem but to instead point you to hints or tutorials such that you finish your own work yourself. Surely your university's ethics policy mentions this?

I sincerely apologize, I didn't consider this issue. Next time when I ask a question, I will make sure to include 'homework' in the title.

[Julian Berman]

What materials have you been given to actually learn Lean sufficiently well to solve these problems? Surely you weren't simply given a bunch of problems and asked to solve them without being taught anything about Lean?

[Jasin Jiang]

Julian Berman said:

What materials have you been given to actually learn Lean sufficiently well to solve these problems? Surely you weren't simply given a bunch of problems and asked to solve them without being taught anything about Lean?

Not much learning material was provided. There were a few public lectures on Lean 4, mainly focusing on basic propositional reasoning, but after that, there were no further courses. I had to figure out how to prove things by watching how other students write code, looking at definitions in Lean 4 Mathlib, and asking questions in forums. I really feel like I’m self-learning

[Julian Berman]

And a few hours ago when you were linked https://leanprover-community.github.io/learn.html, which of those did you read?

[Jasin Jiang]

Julian Berman said:

And a few hours ago when you were linked https://leanprover-community.github.io/learn.html, which of those did you read?

try to play that game in this html.

[Patrick Massot]

@Jasin Jiang since your goal.lean shows clear work, here is a way to get started on your x = 1 question:

theorem Binomial_theorem'_aux (n : ℕ) :
  ∑ k in Ico 1 (n + 1), (-1 : ℝ) ^ k * n.choose k * (1 - 1) ^ (k - 1) = - ∑ k in Ico 1 (n + 1), 1 ^ (k - 1) := by
  cases n with
  | zero => simp
  | succ n =>
    suffices ∑ k ∈ Ico 1 (n + 2), (-1 : ℝ) ^ k * ((n + 1).choose k) * 0 ^ (k - 1) = -(n + 1) by simpa
    rw [← sum_Ioo_add_left]
    · sorry
    · sorry

[Patrick Massot]

Note the line with simpa was written by first writing simp and then copy-pasting the resulting goal into a suffices.

[Jasin Jiang]

@_**Patrick Massot

have : (-1 : ℝ) ^ 1 * ↑((n + 1).choose 1) * 0 ^ (1 - 1) = -(↑n + 1) := by
      simp

What is 0 ^ 0 defined as in Lean 4? I really didn't notice this, I thought it was undefined.
I am really surprised that a single simp can make this expression hold.

[Kevin Buzzard]

I am not at all surprised that simp can make progress here. simp just rewrites with many theorems of the form X=Y where Y is an obviously simpler form of X. So it will simplify x^1 to x, it will simplify x-x to 0, it will simplify 0^0 to 1, it will simplify x*1 to x and so on

[Kevin Buzzard]

Nothing is undefined in lean, even 1/0 is defined and it's 0

[Jasin Jiang]

thank you

[Patrick Massot]

Note that your question would not make any sense if this was not defined.

[Jasin Jiang]

ok, i get it