Is there an idiom for applying a subproof in two directions?

Stream: maths

[Dan Abramov]

Here's a little example:

import Mathlib

open Set
open Function

variable {α β : Type*} [Nonempty β]
variable (f : α → β) (g : β → α

example (x : Set α) (hx: x = univ ∨ x = ∅) : (Injective f) := by
  intro a1 a2 heq

  have direct_iif : a1 ∈ x ↔ a2 ∈ x := by
    constructor
    · intro aex
      rcases hx with (h1 | h2)
      · rw [h1]
        trivial
      · rw [h2] at aex
        trivial
    · intro aex
      rcases hx with (h1 | h2)
      · rw [h1]
        trivial
      · rw [h2] at aex
        trivial
  sorry

Note I'm interested in having a statement like direct_iif : a1 ∈ x ↔ a2 ∈ x so I can use it later. However, I'm not excited about proving it in both directions because a1 and a2 are equivalent and the exact same proof can be reused. In the above example, it's this part:

    · intro aex
      rcases hx with (h1 | h2)
      · rw [h1]
        trivial
      · rw [h2] at aex
        trivial

You can see it being repeated twice because we need to cover both directions.

Is there an idiomatic way to treat a1 and a2 as interchangeable in a certain context, saying "we proved this for a1 and a2 but we didn't rely on anything differentiating them during that proof, therefore the proof holds for a2 and a1 too".

I assume the wlog tactic might have something to do with it but I can't figure out how to use it. (It would help if the documentation for each tactic contained at least a single actual example of actually using them to prove something — even a toy one. :)

[Riccardo Brasca]

Yeah, wlog is a pain. The problem is that when we say informally "wlog a ≤ b" we often say "since clearly the same proof works, interchanging a and b, let's suppose a ≤ b. But Lean of course does not understand this "clearly" andwlog asks to show that the case a ≤ b implies the case b ≤ a, that if often not our way of thinking.

[Riccardo Brasca]

Having said that, usually you can extract a sublemma. Here it would be that s = univ implies x ∈ s, for all x.

[Riccardo Brasca]

No sorry, I misread your code.

[Ruben Van de Velde]

For your particular example, obtain rfl|rfl := hx <;> simp works, but that might be simplified too much :)

[Dan Abramov]

Haha yeah the code is a bit simplified, the main thing is really this pattern:

• I have some a1 and a2 of the same type
• I want to prove something about their interrelation
• This thing I want to prove is symmetric and I'd rather not prove it twice
• I'd also rather not extract a whole lemma out of it or further abstract it with more variables

[Riccardo Brasca]

Something like

import Mathlib

open Set
open Function

variable {α β : Type*} [Nonempty β]
variable (f : α → β) (g : β → α)

lemma foo {x : Set α} (hx : x = univ ∨ x = ∅) {a1 a2 : α} (ha1 : a1 ∈ x) : a2 ∈ x := by
  rcases hx with (h1 | h2)
  · rw [h1]
    trivial
  · rw [h2] at ha1
    trivial

example (x : Set α) (hx: x = univ ∨ x = ∅) : (Injective f) := by
  intro a1 a2 heq

  have direct_iif : a1 ∈ x ↔ a2 ∈ x := by
    constructor
    · exact foo hx
    · exact foo hx
  sorry

[Riccardo Brasca]

You can even do have direct_iif : a1 ∈ x ↔ a2 ∈ x := ⟨foo hx, foo hx⟩

[Dan Abramov]

Fair enough, guess that's where I'm going. No change wlog would simplify this?

[Riccardo Brasca]

But maybe you are looking for

  have direct_iif : a1 ∈ x ↔ a2 ∈ x := by
    constructor
    all_goals {
      intro aex
      rcases hx with (h1 | h2)
      · rw [h1]
        trivial
      · rw [h2] at aex
        trivial }

[Dan Abramov]

Heh, this is not bad.

[Riccardo Brasca]

There is also the similar any_goals (not relevant here, but if learn about one it is worth to know that the other exists)

[Riccardo Brasca]

Note also that using by assumption (or ‹_› to look fancy) you can sometimes improves the behavior of all_goals tac, since it works also if the only difference in the goals is a name of an hypothesis.

[Yakov Pechersky]

We also have swap_var to do a rough renaming of hypotheses/variables that is a poor man's wlog

[Dan Velleman]

By the way, I don't see how your original example can be right. Did you perhaps mean:

example (h : ∀ (x : Set α), x = univ ∨ x = ∅) : Injective f

[Dan Abramov]

Please ignore the statement itself, I just wrote something minimal that typechecks to create something that can be copy pasted into the editor.

The actual problem I'm working on was this one, see heq_imp_same_directness and how it's applied for what I was trying to achieve (I'd still like to see if it's possible to inline it without making the proof bloated).

[Chris Wong]

I think the reason why wlog doesn't work here is because it doesn't actually understand symmetry, it just tries to negate the assumption, which works for linear orders (docs#le_of_not_le) but doesn't work for implication.

[Chris Wong]

I wonder if there's demand for a wlog_swap that works for iffs.

[Mario Carneiro]

Note that wlog used to be a lot smarter and it got downscoped because it had too many bells and whistles and/or was too slow. Maybe @Johan Commelin remembers the story better

[Johan Commelin]

It was so slow in Lean 3 that it wasn't really practical.
I agree that the current version is so downscoped that it isn't really practical either.
It would be great to have the Goldilocks version of wlog. :bear: :bowl: :woman_blond_hair: