## Stream: maths

### Topic: WLOGgery

#### Kevin Buzzard (Jun 12 2020 at 11:35):

I have got two terms P and Q of a certain type, and I want to make a third term R of this type with some properties -- it has to be less than P and less than Q. The construction of R is completely symmetric in P and Q, at some point I extract a real eP from P and a real eQ from Q, and then I define eR to be min eP eQ and build R from this. My goal is now R < P \and R < Q. The proofs of these things will be (a) mildly lengthy and (b) essentially identical, there just being one point where I'll use le_min_left in one thread and le_min_right in the other, and one point where I'll use hP in
one thread and hQ in the other.

Is there some WLOGgery trick I can use to halve the amount of work I'm about to do?

Out of interest, my tactic state is this (this is not really relevant to the question but it gives some kind of an idea as to the situation I'm in):

X : Type,
d : X → X → ℝ,
_inst_1 : is_pseudometric d,
P Q : cover X,
εP : ℝ,
hεP : 0 < εP,
hP : ∀ (x : X), ∃ (U : set X) (H : U ∈ P.C), closed_ball d x εP ⊆ U,
εQ : ℝ,
ε : ℝ := min εP εQ / 2,
hεQ : 0 < εQ,
hQ : ∀ (x : X), ∃ (U : set X) (H : U ∈ Q.C), closed_ball d x εQ ⊆ U,
hε : 0 < min εP εQ,
hε : ε = min εP εQ / 2
⊢ closed_ball_cover d ε _ <* P ∧ closed_ball_cover d ε _ <* Q


#### Kevin Buzzard (Jun 12 2020 at 11:36):

(this is teaching material, I'm using non-standard versions of metric spaces, closed balls etc, this is not the issue)

#### Kevin Buzzard (Jun 12 2020 at 11:39):

Over the board I'd just say "of course the proof of the second case is the same"

#### Kevin Buzzard (Jun 12 2020 at 11:57):

I finished my proof and just cut and pasted it; I had to change two lines for the second case.

  { rw star_ref_iff,
rintros _ ⟨x, rfl⟩,
rcases hP x with ⟨U, hUP, hUε⟩, -- <- changes to rcases hQ x
use [U, hUP],
rintros _ ⟨y, rfl⟩ hxy,
rw ne_empty_iff_nonempty at hxy,
rcases hxy with ⟨z, hzx, hzy⟩,
refine subset.trans _ hUε,
intros t hty,
rw mem_closed_ball at ⊢ hzx hzy hty,
suffices : d x t ≤ 3 * ε,
{ refine le_trans this _,
rw hε,
convert min_le_left εP εQ, -- <- changes to min_le_right
linarith,
},
calc d x t ≤ d x z + d z t : d_triangle d x z t
...        ≤ d x z + (d z y + d y t) : by linarith [d_triangle d z y t]
...        = d x z + (d y z + d y t) : by rw d_comm d z y
...        ≤ 3 * ε : by linarith
},


#### Jalex Stark (Jun 12 2020 at 12:01):

I think the thing I would do is generalize some tail of the proof script so that it closes both goals

#### Jalex Stark (Jun 12 2020 at 12:02):

So in this part,

      rw hε,
convert min_le_left εP εQ, -- <- changes to min_le_right
linarith,


I'd make it so that linarith just needs to be told min_le_left and min_le_right, and I'd have the line before it put both of those inequalities into the tactic state

#### Jalex Stark (Jun 12 2020 at 12:03):

and in this part,

 { rw star_ref_iff,
rintros _ ⟨x, rfl⟩,
rcases hP x with ⟨U, hUP, hUε⟩, -- <- changes to rcases hQ x


I'd do something like

all_goals  { rw star_ref_iff,   rintros _ ⟨x, rfl⟩},
rcases hP x with ⟨U, hUP, hUε⟩,
swap, rcases hQ x with ⟨U, hUP, hUε⟩,
all_goals {...


#### Jalex Stark (Jun 12 2020 at 12:04):

I guess this is bad pedagogy, though, you're really hoping for one thing you can say at the beginning that's like the mathematician's wlog

#### Kevin Buzzard (Jun 12 2020 at 17:32):

I am looking for a WLOG but I might be asking for too much. I feel like I want to be able to say "Anything you can ask me for P, I can tell you the analogous thing for Q" but I'm unclear about whether this is ludicrously optimistic.

#### Yury G. Kudryashov (Jun 12 2020 at 18:00):

Did you trywlog?

#### Jalex Stark (Jun 12 2020 at 19:14):

The last time I tried to use wlog from just reading tactic#wlog i didn't understand it. I found a couple of examples in the library, and it looks pretty to use and looks like it covers kevin's case:
https://github.com/leanprover-community/mathlib/blob/ff3130da134188aa6491efa6cebe94efa4247273/src/algebra/char_zero.lean
https://github.com/leanprover-community/mathlib/blob/64e464f1970e29ab77e8bdf0a9d3751cdd429f5a/src/data/set/disjointed.lean

#### Jalex Stark (Jun 12 2020 at 19:15):

kevin, do you have a mwe? or just a pointer to a file in a github project?

#### Kevin Buzzard (Jun 12 2020 at 19:32):

https://github.com/ImperialCollegeLondon/uniform-structures/blob/5e2e7ab47fcc425a801f8568d2638fccf2a4e511/exercises/covers_from_pseudometric.lean#L125

The goal at the split is R < P \and R < Q.
The last time I tried to use wlog I didn't understand it either. I'll try it again now.

#### Kevin Buzzard (Jun 12 2020 at 19:35):

@Yury G. Kudryashov my (limited) understanding of wlog is that it is able to add extra hypotheses of the form "a <= b" if everything is symmetric in a and b. I have a goal of the form P and Q and I want to say "it suffices to prove P, because a proof of P can be used to generate a proof of Q".

#### Yury G. Kudryashov (Jun 12 2020 at 21:17):

Can you say wlog p implies q?

Last updated: May 18 2021 at 06:15 UTC