Zulip Chat Archive
Stream: lean4
Topic: WLOG syntax confusion
Haocheng Wang (Aug 08 2024 at 08:12):
I am new to this tactic Wlog. I am trying to prove the question that if a, b ,c are three side of a triangle and follow proposition stands. I am trying to state that by symmetric we can assume x ≤ y ≤ z to close it.
I have saw one of the topic provide an example but I'm still confuse when proving this. May some expert give me some hints?
import Mathlib
namespace question
variable {a b c x y z: ℝ}
variable (h₀ : a > 0 ∧ b > 0 ∧ c > 0) (h₁ : a + b > c ∧ a + c > b ∧ b + c > a)
variable (hx : x = √ b + √ c - √ a) (hy : y = √ c + √ a - √ b) (hz : z = √ a + √ b - √ c)
variable (x y z :ℝ)
noncomputable abbrev g : ℝ := (x - y) * (x - z) / (4 * x ^ 2)
--√ (b+c-a)/(√ b + √ c - √ a)
theorem question_lemma : (g x y z) + (g z x y) + (g y z x) ≥ 0 := by
wlog hxy : x ≤ y generalizing x y z with H1
. push_neg at hxy
obtain h := H1 y x z hxy.le
sorry
. wlog hyz : y ≤ z generalizing x y z with H2
. push_neg at hyz
rcases le_total x z with hxz | hxz
. obtain h1:= H2 x z y hxz hyz.le
sorry
. obtain h1:= H2 x y z hxy sorry
exact h1
. sorry
end question
Haocheng Wang (Aug 12 2024 at 02:32):
/
Johan Commelin (Aug 12 2024 at 06:21):
The expression (g x y z) + (g z x y) + (g y z x) ≥ 0
isn't invariant under all permutations of [x,y,z]
so you can't assume x \le y \le z
wlog, right? But you can assume that x
is smaller than y
and smaller than z
.
Johan Commelin (Aug 12 2024 at 06:30):
import Mathlib
namespace question
variable {a b c x y z: ℝ}
variable (h₀ : a > 0 ∧ b > 0 ∧ c > 0) (h₁ : a + b > c ∧ a + c > b ∧ b + c > a)
variable (hx : x = √ b + √ c - √ a) (hy : y = √ c + √ a - √ b) (hz : z = √ a + √ b - √ c)
variable (x y z :ℝ)
noncomputable abbrev g : ℝ := (x - y) * (x - z) / (4 * x ^ 2)
--√ (b+c-a)/(√ b + √ c - √ a)
theorem question_lemma : (g x y z) + (g z x y) + (g y z x) ≥ 0 := by
wlog hxyz : x ≤ y ∧ x ≤ z generalizing x y z with H1
. push_neg at hxyz
by_cases hxy : x ≤ y
· have hzx := (hxyz hxy).le
have := H1 z x y ⟨hzx, hzx.trans hxy⟩
linarith
push_neg at hxy
by_cases hyz : y ≤ z
· have := H1 y z x ⟨hyz, hxy.le⟩
linarith
push_neg at hyz
have := H1 z x y ⟨hyz.le.trans hxy.le, hyz.le⟩
. sorry
end question
Johan Commelin (Aug 12 2024 at 06:30):
It would be nice if we had better tooling for the cyclic permutation argument
Last updated: May 02 2025 at 03:31 UTC