## Stream: general

### Topic: easy subset/subtype lemma

#### Kevin Buzzard (Jul 16 2018 at 14:15):

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 (Jul 16 2018 at 14:18):

can you try by ext; dsimp; tauto?

#### Simon Hudon (Jul 16 2018 at 14:19):

Sorry, no that won't work

#### Mario Carneiro (Jul 16 2018 at 14:20):

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

#### Mario Carneiro (Jul 16 2018 at 14:20):

wait, that's not type correct

#### Patrick Massot (Jul 16 2018 at 14:20):

hence Kevin's .val

#### Simon Hudon (Jul 16 2018 at 14:22):

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

#### Mario Carneiro (Jul 16 2018 at 14:23):

I think and.congr_right needs a biconditional version

#### Mario Carneiro (Jul 16 2018 at 14:38):

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]


Thanks Mario.

#### Kevin Buzzard (Jul 16 2018 at 14:50):

@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.

Last updated: May 08 2021 at 10:12 UTC