how to use wlog correctly?

Stream: new members

[Conner Bondurant]

Hi! I've been interested in lean4 in a small hobby level for a while now, and I was inspired to try and get my hands dirty through attempting to add a new entry to the formalized IMO problems. Go straight to the deep end and find what I still need to learn by getting stuck.
Specifically I've been chipping away at attempting to formalize 1971 P3

However I've hit a big sticking point for me. My understanding is that would like to use the wlog tactic to express the idea that if two numbers are not equal one of them must be the smaller one. but I find its syntax rather confusing and there is a real lack of examples of wlog in use that I've been able to find as references to get a sense of how it is expected to be used.

I'm also currently a bit baffled by the actual informal proof statement I am utilizing as reference, but at the moment I consider that secondary to trying to understand how to express this wlog idea that is so easy to express with words.

import Mathlib

namespace Imo1971P3

abbrev AllCoprime (s : Set ℕ+) : Prop :=
  s.Pairwise fun m n ↦ Nat.Coprime (2 ^ n.val - 3) (2 ^ m.val - 3)

-- We show how to enlarge a set of r such integers to a set of r+1.
-- s_gt_1 is trivial since we can choose the members of s as we wish
lemma can_extend (s : Finset ℕ+) (h : AllCoprime s) :
  (∃ n : ℕ+, And (n ∉ s) (AllCoprime (insert n s)) ) := by
  by_cases hs : s = ∅
  · sorry
  · let P := ∏ m ∈ s, (2 ^ m.val - 3) -- original proof uses m too many times, used P to distingush
    let pset := Finset.range (P + 1)

    have pidgeonhole_exists : ∃ i ∈ pset , ∃ j ∈ pset , i ≠ j ∧ P.ModEq (2^i) (2^j) := by
      sorry -- I have this proof completed

    obtain ⟨i, i_set, j, j_set, i_ne_k, i_cong_k_mod_p⟩ := pidgeonhole_exists

    -- context from obtain
    -- i : ℕ
    -- i_set : i ∈ pset
    -- j : ℕ
    -- j_set : j ∈ pset
    -- i_ne_k : i ≠ k
    -- i_cong_k_mod_p : 2 ^ i ≡ 2 ^ j [MOD P]

    -- I now have i and k that should be usable for showing 2^(i-j) - 1 ≡ 0 [MOD P]
    -- It's unclear, however how to pull in the needed facts for this?
    -- main thing I want is to be able to add i < j to the current context
    -- my understanding is that is possible with wlog?
    sorry

end Imo1971P3

Any advice would be greatly appreciated.

[Kenny Lau]

@Conner Bondurant you might have read this already, but in case you didn't, when you type wlog and hover your mouse over it, the following information appears:

image.png

[Kenny Lau]

so for your case you would type wlog h : i < j

[Kenny Lau]

I assume you are familiar enough with the syntax "h : p"

[Kenny Lau]

if not, it means "h is a proof of p"

[Etienne Marion]

Here is how to use the tactic:

import Mathlib

namespace Imo1971P3

abbrev AllCoprime (s : Set ℕ+) : Prop :=
  s.Pairwise fun m n ↦ Nat.Coprime (2 ^ n.val - 3) (2 ^ m.val - 3)

-- We show how to enlarge a set of r such integers to a set of r+1.
-- s_gt_1 is trivial since we can choose the members of s as we wish
lemma can_extend (s : Finset ℕ+) (h : AllCoprime s) :
  (∃ n : ℕ+, And (n ∉ s) (AllCoprime (insert n s)) ) := by
  by_cases hs : s = ∅
  · sorry
  · let P := ∏ m ∈ s, (2 ^ m.val - 3) -- original proof uses m too many times, used P to distingush
    let pset := Finset.range (P + 1)

    have pidgeonhole_exists : ∃ i ∈ pset , ∃ j ∈ pset , i ≠ j ∧ P.ModEq (2^i) (2^j) := by
      sorry -- I have this proof completed

    obtain ⟨i, i_set, j, j_set, i_ne_k, i_cong_k_mod_p⟩ := pidgeonhole_exists

    -- context from obtain
    -- i : ℕ
    -- i_set : i ∈ pset
    -- j : ℕ
    -- j_set : j ∈ pset
    -- i_ne_k : i ≠ k
    -- i_cong_k_mod_p : 2 ^ i ≡ 2 ^ j [MOD P]

    -- I now have i and k that should be usable for showing 2^(i-j) - 1 ≡ 0 [MOD P]
    -- It's unclear, however how to pull in the needed facts for this?
    -- main thing I want is to be able to add i < j to the current context
    -- my understanding is that is possible with wlog?
    wlog hij : i < j generalizing i j
    · exact this j j_set i i_set i_ne_k.symm i_cong_k_mod_p.symm (by grind)
    · sorry -- your proof when i < j

end Imo1971P3

[Conner Bondurant]

ohhhh! Ok I think I get it now. I had been trying to figure out when and where the tactic symm needed to be used.

[Conner Bondurant]

thank you!

[Conner Bondurant]

also, I wasn't sure what to call the thread here so its kinda out of scope, but if I could also go ahead and ask the following regarding the actual proof statement:
It makes what looks to me like a logical leap where because i_cong_k_mod_p, (oops I meant to rename that...) and that P is odd, that 2^(j-i) -1 ≡ 0 [MOD P] holds. From trying to figure out how that was a solid claim to make, I had thought it was based on linear congruence? But I'm realizing now that actually I don't think that's correct.
Despite a lot of searching I've not found any modular arithmatic identity/property that would actually imply this.