wloggery

Stream: general

[Kevin Buzzard]

Can I use wlog to get around that suffices trick below?

import data.set.basic

open function

variables {X Y : Type} (f : X → Y)

lemma image_injective : injective f → injective (λ S, f '' S) :=
begin
  intro hf,
  intros S T h,
  dsimp at h,
  ext x,
  /-
  X Y : Type
  f : X → Y
  hf : injective f
  S T : set X
  h : f '' S = f '' T
  x : X
  ⊢ x ∈ S ↔ x ∈ T
  -/
  -- how do I say "wlog I only have to do one implication?"
  suffices : ∀ S T : set X, f '' S = f '' T → x ∈ S → x ∈ T,
  { split,
      apply this _ _ h,
      apply this _ _ h.symm,
  },
  clear h S T,
  intros S T h,
  sorry
end

[Mario Carneiro]

It's a little silly because wlog isn't designed to handle wlogging in the goal, only the hypotheses

lemma image_injective : injective f → injective (λ S, f '' S) :=
begin
  intro hf,
  intros S T h,
  dsimp at h,
  ext x,
  by_contra,
  wlog : ¬(x ∈ S → x ∈ T) using [S T, T S],
  { simpa only [← not_and_distrib, iff_def] using h },
  apply case, clear case h_1,
  intros h,
  sorry
end