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