proving equality of cartesian product

Stream: Is there code for X?

[Andrew Lubrino]

I'm trying to prove the equality of sets of Cartesian products. I've tried using eq_of_subset_of_subset and ext with iff.intro but Lean keeps throwing an error. Can anyone point me in the right direction here? Code is below:

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₂)

[Adam Topaz]

Can you provide a #mwe ?

[Adam Topaz]

Nevermind... I ggot it:

import data.set

variables {α β : Type*} (A : set α) (B C : set β)

example : A ×ˢ (B ∩ C) = (A ×ˢ B) ∩ (A ×ˢ C) := by tidy

[Adam Topaz]

If you want a less automatic proof:

example : A ×ˢ (B ∩ C) = (A ×ˢ B) ∩ (A ×ˢ C) :=
begin
  ext,
  split,
  { rintros ⟨h1,h2,h3⟩,
    exact ⟨⟨h1,h2⟩,⟨h1,h3⟩⟩ },
  { rintros ⟨⟨h1,h1'⟩,⟨h2,h2'⟩⟩,
    exact ⟨h1,h1',h2'⟩ }
end

[Adam Topaz]

Or in term-mode:

example : A ×ˢ (B ∩ C) = (A ×ˢ B) ∩ (A ×ˢ C) :=
set.ext $ λ x, ⟨λ ⟨h1,h2,h3⟩, ⟨⟨h1,h2⟩,h1,h3⟩, λ ⟨⟨h1,h1'⟩,h2,h3⟩, ⟨h2,h1',h3⟩⟩