WLOG syntax confusion

Stream: lean4

[Haocheng Wang]

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]

/

[Johan Commelin]

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]

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]

It would be nice if we had better tooling for the cyclic permutation argument