_Logic and Proof_, Exercise 15.5, first cut

Exercise 15.5.lean

-- Exercise 15.5.5

import data.set
open set

variable {U : Type}
variables A B : set U

variable f : U → U      

-- The definition of f[A] for the f given above
-- I can't get it to work for now, so it's included here for reference.
variable image_of_f : set U → set U
def h_img (A : set U) : Prop :=
∀ y, (y ∈ image_of_f A ↔ ∃ x, (x ∈ A ∧ y = f x))


example : image_of_f A \ image_of_f B ⊆ image_of_f (A \ B) :=
show ∀ y, (y ∈ image_of_f A \ image_of_f B → y ∈ image_of_f (A \ B)),
from
  assume y,
  show y ∈ image_of_f A \ image_of_f B → y ∈ image_of_f (A \ B),
  from (
    assume h1 : y ∈ image_of_f A \ image_of_f B,
    have h2 : y ∈ image_of_f A ∧ y ∉ image_of_f B, from h1,

    have h3 : y ∈ image_of_f A, from and.left h2,
    have lemma_A : ∃ x, (x ∈ A ∧ y = f x), from sorry,  -- by definition from h3

    have h4 : ¬ (y ∈ image_of_f B), from and.right h2,
    have h5 : ¬ ∃ x, (x ∈ B ∧ y = f x), from sorry,  -- from h4
    have lemma_B : ∀ x, ¬ (x ∈ B ∧ y = f x), from sorry,  -- from h5

    have h6 : ∃ x, (x ∈ A \ B ∧ y = f x),
    from exists.elim lemma_A (
      assume x0 (hx1 : x0 ∈ A ∧ y = f x0),
      have       y = f x0, from and.right hx1,
      have       x0 ∈ A, from and.left hx1,
      have hx2 : ¬ (x0 ∈ B ∧ y = f x0), from lemma_B x0,
      have       x0 ∉ B,
      from (
        assume : x0 ∈ B,
        have hy1 : x0 ∈ B ∧ y = f x0,
          from and.intro ‹x0 ∈ B› ‹y = f x0›,
        hx2 hy1
      ),
      have hx3 : x0 ∈ A ∧ x0 ∉ B,
        from and.intro ‹x0 ∈ A› ‹x0 ∉ B›,
      have       x0 ∈ A \ B, from hx3,
      have hx4 : x0 ∈ A \ B ∧ y = f x0,
        from and.intro ‹x0 ∈ A \ B› ‹y = f x0›,
      show ∃ x, (x ∈ A \ B ∧ y = f x),
        from exists.intro x0 hx4
    ),
    show y ∈ image_of_f (A \ B), from sorry  -- by definition from h6
  )