easy subset/subtype lemma

Stream: general

[Kevin Buzzard]

I've reduced my goal to

example (X : Type) (U A B : set X) : U ∩ A = U ∩ B ↔ {u : U | u.val ∈ A} = {u : U | u.val ∈ B} := sorry

Is there a one-liner for this? As it happens I only need the <- direction but it somehow all looks easy.

[Simon Hudon]

can you try by ext; dsimp; tauto?

[Simon Hudon]

Sorry, no that won't work

[Mario Carneiro]

there should be a lemma {x : A | x \in B} = A \cap B

[Mario Carneiro]

wait, that's not type correct

[Patrick Massot]

hence Kevin's .val

[Simon Hudon]

Second attempt: dsimp [set_eq_def]; apply forall_congr; tauto

[Mario Carneiro]

I think and.congr_right needs a biconditional version

[Mario Carneiro]

lemma and.congr_right_iff {a b c : Prop} : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
⟨λ h ha, by simp [ha] at h; exact h, and_congr_right⟩

example (X : Type) (U A B : set X) :
  U ∩ A = U ∩ B ↔ {u : U | u.val ∈ A} = {u : U | u.val ∈ B} :=
by simp [set.set_eq_def, and.congr_right_iff]

[Kevin Buzzard]

Thanks Mario.

[Kevin Buzzard]

@Luca Gerolla is doing homotopy theory in Lean and this was all that was left for proving that a function on [0,1] is continuous iff its restriction to [0,1/2] and [1/2,1] is.