Zulip Chat Archive
Stream: general
Topic: question about an easy proof
Yujie Wang (Jan 17 2025 at 23:55):
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 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