Getting prod_mk_mem_set_prod_eq to work

Stream: new members

[Andrew Lubrino]

I know I've been asking a lot about Cartesian products, but I've been having some trouble and want to ask one more. I have the below code:

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

  example : A ×ˢ (B ∩ C) = (A ×ˢ B) ∩ (A ×ˢ C) :=
  assume x : U,
  assume y : U,
  assume h₁ : (x, y) ∈ A ×ˢ (B ∩ C),
  have h₂ : (x, y) ∈ A ×ˢ B ∩ C = (x ∈ A ∧ y ∈ B ∩ C), from prod_mk_mem_set_prod_eq

In my line starting with have h2, I'm getting an error: failed to synthesize type class instance. Does anyone have an idea about how I can fix this?

[Eric Rodriguez]

what are your imports?

[Andrew Lubrino]

only open set

[Eric Rodriguez]

you may need the brackets around the B ∩ C on the have in the last line

[Andrew Lubrino]

wow, clutch. Thanks!

[Andrew Lubrino]

Okay, I wrote up a proof in Lean about the equality of Cartesian products, but I'm having getting it to compile. I proved both sides of the equality, but I'm now getting errors when I try to finish off the proof with eq_of_subset_of_subset. What command should I use to prove the equality of Cartesian products?

  example : A ×ˢ (B ∩ C) = (A ×ˢ B) ∩ (A ×ˢ C) :=
    eq_of_subset_of_subset
    (assume x : U,
    assume y : U,
    assume h₁ : (x, y) ∈ A ×ˢ (B ∩ C),
    have h₂ : (x, y) ∈ A ×ˢ (B ∩ C) = (x ∈ A ∧ y ∈ B ∩ C), from prod_mk_mem_set_prod_eq,
    have h₃ : x ∈ A ∧ y ∈ B ∩ C, from eq.subst h₂ h₁,
    have h₄ : (x, y) ∈ A ×ˢ B, from
      (have h₅ : y ∈ B, from (h₃.right).left,
      show (x, y) ∈ A ×ˢ B, from mk_mem_prod (h₃.left) h₅),
    have h₅ : (x, y) ∈ A ×ˢ C, from
      (have h₆ : y ∈ C, from (h₃.right).right,
      show (x, y) ∈ A ×ˢ C, from mk_mem_prod (h₃.left) h₆),
    show (x, y) ∈ (A ×ˢ B) ∩ (A ×ˢ C), from and.intro h₄ h₅)
    (assume x : U,
    assume y : U,
    assume h₁ : (x, y) ∈ (A ×ˢ B) ∩ (A ×ˢ C),
    have h₂ : x ∈ A ∧ y ∈ (B ∩ C), from
      (have h₃ : (x, y) ∈ (A ×ˢ B), from h₁.left,
      have h₄ : (x , y) ∈ A ×ˢ B = (x ∈ A ∧ y ∈ B), from prod_mk_mem_set_prod_eq,
      have h₅ : x ∈ A ∧ y ∈ B, from eq.subst h₄ h₃,
      have h₆ : (x, y) ∈ (A ×ˢ C), from h₁.right,
      have h₇ : (x , y) ∈ A ×ˢ C = (x ∈ A ∧ y ∈ C), from prod_mk_mem_set_prod_eq,
      have h₈ : x ∈ A ∧ y ∈ C, from eq.subst h₇ h₆,
      show x ∈ A ∧ y ∈ (B ∩ C), from and.intro h₅.left (and.intro (h₅.right) (h₈.right))),
    have h₃ : (x, y) ∈ A ×ˢ (B ∩ C) = (x ∈ A ∧ y ∈ B ∩ C), from prod_mk_mem_set_prod_eq,
    show (x, y) ∈ A ×ˢ (B ∩ C), from eq.subst h₃ h₂)

[Andrew Lubrino]

I've also tried ext with iff.intro, but I'm not able to get it to work

[Eric Wieser]

Is there a reason you're not using tactic mode?

[Eric Wieser]

ext, simp can probably close this, if we don't already have docs#set.prod_inter

[Kevin Buzzard]

@Andrew Lubrino #mwe . Can you please include your imports and opens in your initial post so that other people can run your code more easily?