push_neg for iUnion

Stream: new members

[Tian Hsia]

Hello,

I am proving the Schröder-Bernstein Theorem in MIL and feeling excited about it. But I ran into a problem and didn't know why it didn't work or an alternative solution.

I am doing this

theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by
  have : x ∈ g '' univ := by
    push_neg at hx

And the monitor showing

    α : Type u_1
    β : Type u_2
    inst✝ : Nonempty β
    f : α → β
    g : β → α
    x : α
    hx : x ∉ sbSet f g
    ⊢ x ∈ g '' univ

Some definitions are

def sbAux : ℕ → Set α
  | 0 => univ \ g '' univ
  | n + 1 => g '' (f '' sbAux n)

def sbSet :=
  ⋃ n, sbAux f g n

def sbFun (x : α) : β :=
  if x ∈ sbSet f g then f x else invFun g x

I am wondering why push_neg doesn't work here and what's the optimal solution to push the negative signe in this case.

Thanks for your helping!

[Patrick Massot]

push_neg does not unfold definitions, so you need to unfold sbSet, and probably use docs#Set.mem_iUnion too.

[Patrick Massot]

I just had a look and notice that the book gives a beginning of this proof that avoids this issue. Why did you discard it?

[Tian Hsia]

Patrick Massot said:

I just had a look and notice that the book gives a beginning of this proof that avoids this issue. Why did you discard it?

I wrote my proof on paper first and wanted to copy it. I understand the proof given by the book and it's definitely more elegant in lean.

Thank you for your help, I thought that negative signs before set operations were common so there should be some quick way to push it.