question about an easy proof

Stream: general

[Yujie Wang]

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]

If you want to formalize the second line in the screenshot, you'll note that it is a statement about all $k$ 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]

Thanks! that helps!

[Yujie Wang]

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

[Ruben Van de Velde]

@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]

And the tactic that used to be called split is nowconstructor