set theory grunt work

Stream: general

[Patrick Massot]

I need to prove the following (hoping I didn't mess up my lemma extraction):

example {α : Type*}
  (U₁ V₁ U₂ V₂ : set α)
  (VU₁ : V₁ ⊆ U₁)
  (VU₂ : V₂ ⊆ U₂)
  (H : U₁ ∩ U₂ = ∅)
  (u v w : α)
  (u_in : u ∈ V₁)
  (v_in : v ∈ V₂)
  (huw : (u, w) ∈ (U₁.prod U₁) ∪ (U₂.prod U₂) ∪ ((-(V₁ ∩ V₂)).prod $ -(V₁ ∩ V₂)))
  (hwv : (w, v) ∈ (U₁.prod U₁) ∪ (U₂.prod U₂) ∪ ((-(V₁ ∩ V₂)).prod $ -(V₁ ∩ V₂))) :
  (u, w) ∈ U₁.prod U₁ :=
sorry

Is there anything smart I could do here (besides taking an intern to prove it)?

[Patrick Massot]

The real world proof is to draw four circles on a piece of paper.

[Patrick Massot]

Or, if you have strong opinion about pictures like Bourbaki, not doing anything.

[Rob Lewis]

I didn't even try to process what this is saying, but are you sure it's stated right? simp [set.prod] at *, tauto! reduces it to something unprovable.

[Rob Lewis]

tauto being the usual go-to for set theory grunt work.

[Patrick Massot]

Yes, it's correct, although I forgot to remove that last assumption which is useless (it's used for the variant you have to prove next).

[Patrick Massot]

Because V1 is disjoint from U2 and U3.

[Rob Lewis]

Oh, sorry, the result of tauto is provable (there's a contradiction in the hypotheses).

[Patrick Massot]

Indeed.

[Alistair Tucker]

What's U\3? I don't see it

[Patrick Massot]

Sorry, U3 is -(V₁ ∩ V₂)

[Patrick Massot]

Wait, I messed up something.

[Patrick Massot]

I meant union of V1 and V2, not intersection.

[Chris Hughes]

example : ¬ ∀ {α : Type*}
  (U₁ V₁ U₂ V₂ : set α)
  (VU₁ : V₁ ⊆ U₁)
  (VU₂ : V₂ ⊆ U₂)
  (H : U₁ ∩ U₂ = ∅)
  (u v w : α)
  (u_in : u ∈ V₁)
  (v_in : v ∈ V₂)
  (huw : (u, w) ∈ (U₁.prod U₁) ∪ (U₂.prod U₂) ∪ ((-(V₁ ∩ V₂)).prod $ -(V₁ ∩ V₂)))
  (hwv : (w, v) ∈ (U₁.prod U₁) ∪ (U₂.prod U₂) ∪ ((-(V₁ ∩ V₂)).prod $ -(V₁ ∩ V₂))),
  (u, w) ∈ U₁.prod U₁ :=
begin
  assume h,
  simpa using @h bool {tt} {tt} {ff} {ff} (by simp) (by simp)
    (by simp [set.ext_iff]) tt ff ff (by simp) (by simp)
end

[Chris Hughes]

It's false

[Patrick Massot]

Yes, I messed up the statement, as I wrote above.

[Patrick Massot]

Sorry about that.

[Patrick Massot]

It's too hot here.

[Chris Hughes]

In that case finish [set.ext_iff, set.subset_def] works

[Patrick Massot]

Thanks!

[Patrick Massot]

My computer is stupid, but fortunately Chris isn't.

[Patrick Massot]

(But Kenny will hate you for that)

[Jalex Stark]

if you post the correct statement i'll look for something faster than finish

[Patrick Massot]

The correct statement is:

example {α : Type*}
  (U₁ V₁ U₂ V₂ : set α)
  (VU₁ : V₁ ⊆ U₁)
  (VU₂ : V₂ ⊆ U₂)
  (H : U₁ ∩ U₂ = ∅)
  (u v w : α)
  (u_in : u ∈ V₁)
  (v_in : v ∈ V₂)
  (huw : (u, w) ∈ (U₁.prod U₁) ∪ (U₂.prod U₂) ∪ ((-(V₁ ∪ V₂)).prod $ -(V₁ ∪ V₂))) :
  (u, w) ∈ U₁.prod U₁ :=
sorry

[Chris Hughes]

set.mem_prod.2 ((huw.resolve_right (λ h, (h.1 $ or.inl u_in))).resolve_right
    (λ h, have u ∈ U₁ ∩ U₂, from ⟨VU₁ u_in, h.1⟩, by rwa H at this))

[Patrick Massot]

I knew the smart thing do to was to take an intern.

[Patrick Massot]

It's still a bit sad. Let's say finish will be fast in Lean 4.

[Patrick Massot]

Thank you very much Chris!

[Jalex Stark]

fwiw here's what I ended up with; i am a worse intern than chris

example {α : Type*}
  (U₁ V₁ U₂ V₂ : set α)
  (VU₁ : V₁ ⊆ U₁)
  (VU₂ : V₂ ⊆ U₂)
  (H : U₁ ∩ U₂ = ∅)
  (u v w : α)
  (u_in : u ∈ V₁)
  (v_in : v ∈ V₂)
  (huw : (u, w) ∈ (U₁.prod U₁) ∪ (U₂.prod U₂) ∪ ((-(V₁ ∪ V₂)).prod $ -(V₁ ∪ V₂))) :
  (u, w) ∈ U₁.prod U₁ :=
begin
  simp only [set.ext_iff, set.subset_def, set.mem_empty_eq, set.compl_union, set.mem_inter_eq, not_and, set.prod_mk_mem_set_prod_eq,
 set.mem_union_eq, set.mem_compl_eq, iff_false] at *,
  split, { tauto },
  have := H u,
  tauto,
end

[Patrick Massot]

Thanks anyway. tauto is way faster than finish

[Patrick Massot]

And I wouldn't be worried to be a worse intern that Chris...

[Bryan Gin-ge Chen]

Working through this was kind of relaxing...

import tactic

example {α : Type*}
  (U₁ V₁ U₂ V₂ : set α)
  (VU₁ : V₁ ⊆ U₁)
  (VU₂ : V₂ ⊆ U₂)
  (H : U₁ ∩ U₂ = ∅)
  (u v w : α)
  (u_in : u ∈ V₁)
  (v_in : v ∈ V₂)
  (huw : (u, w) ∈ (U₁.prod U₁) ∪ (U₂.prod U₂) ∪ ((-(V₁ ∪ V₂)).prod $ -(V₁ ∪ V₂))) :
  (u, w) ∈ U₁.prod U₁ :=
begin
simp only [set.ext_iff, set.subset_def, set.mem_empty_eq, set.compl_union, set.mem_inter_eq, not_and, set.prod_mk_mem_set_prod_eq,
  set.mem_union_eq, set.mem_compl_eq, iff_false] at *,
  rcases huw with ⟨⟨_, _⟩ | ⟨_, _⟩⟩ | ⟨⟨_, _⟩, _, _⟩,
  { split, assumption', },
  { have h := H u (VU₁ u u_in), contradiction, },
  { contradiction, },
end

[Patrick Massot]

We should collaborate more, we have very complementary ways of relaxing.

[Patrick Massot]

I have another one: what is the automated procedure that should have avoided proving by hand:

lemma chore {α : Type*} {U V S A B : set α} : (U ∩ S ∩ A) ∪ (V ∩ S ∩ B) = ((U ∩ A) ∪ (V ∩ B)) ∩ S :=
by  rw [inter_right_comm, inter_right_comm V, union_inter_distrib_right]

[Rob Lewis]

by { ext, simp, tauto! }

[Patrick Massot]

Thanks! I didn't try the right combination. I still wish it could be only one tactic.

[Simon Hudon]

you could have meta def set_theory := `[ext; simp; tauto!]. It's a pretty flexible approach