Zulip Chat Archive

Stream: general

Topic: question about an easy proof


Yujie Wang (Jan 17 2025 at 23:55):

image.png
image.png

Hi guys, I'm trying to do this proof, but for the k here, how could I prove it with this variable k? As I couldn't find many examples online :smiling_face_with_tear:

theorem M_test (n : ) (hn : 3  n) (x y :   )
  (hx :  i, x i  0)
  (h :  k : , 1  k  k < n 
    |∑ i in Finset.Icc 1 k, x i| + |∑ i in Finset.Icc (k+1) n, x i| =
    |∑ i in Finset.Icc 1 k, y i| + |∑ i in Finset.Icc (k+1) n, y i|) :
  IsGreatest {M :  | M = ( i in Finset.Icc 1 n, |y i|) / ( i in Finset.Icc 1 n, |x i|)} M 
  (Odd n  M = n) 
  (Even n  M = n - 1) := by{
    let X :=  i in Finset.Icc 1 n, |x i|


    let S1 :=  i in Finset.Icc 1 k, x i
    let S2 :=  i in Finset.Icc (k+1) n, x i

  }

Ruben Van de Velde (Jan 18 2025 at 00:01):

If you want to formalize the second line in the screenshot, you'll note that it is a statement about all kk in a certain range. So you start with:

have h1 : \forall k \in Finset.Ico 1 n, ... something about k ... := by
  intro k hk
  sorry

Yujie Wang (Jan 18 2025 at 00:05):

Thanks! that helps!

Yujie Wang (Jan 18 2025 at 00:40):

image.png
Hi sorry for borther again, for the cases here, why it shows that it's unknown tactic?

Ruben Van de Velde (Jan 18 2025 at 08:56):

@Yujie Wang where did you get this code? It looks like lean 3 rather than lean 4.

If you write cases hk without anything else, you should get a :light_bulb: icon in the left hand margin that allows you to compete the syntax

Ruben Van de Velde (Jan 18 2025 at 08:57):

And the tactic that used to be called split is nowconstructor


Last updated: May 02 2025 at 03:31 UTC