# Zulip Chat Archive

## Stream: general

### Topic: suffices to prove

#### Kevin Buzzard (Dec 28 2019 at 17:28):

Idly proving that equivalence relations are the same as partitions (thinking about a future Lean maths challenge). Here's a goal:

1 goal X : Type, R : {R // equivalence R}, c d : set X, hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class ↑R x}, hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class ↑R x}, x : X, hx : x ∈ c ∩ d ⊢ c = d

I want to prove this by saying "it suffices to prove c \sub d and d \sub c, but by symmetry we only need to prove c \sub d". I know I can factor out a lemma saying "if all the things in the local context are true then c \sub d" and then I can just apply this lemma twice -- but I don't see any obstruction in theory to having a tactic where I say "by `set.subset.antisymm`

and the underlying symmetry, change the goal to `c \sub d`

please" and maybe Lean replies "just convince me that `x ∈ d ∩ c`

and you're good to go".

Can this already be done with some `wlog`

trickery? I couldn't see how.

#### Kevin Buzzard (Dec 28 2019 at 17:29):

PS `def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y}`

, not that it matters here (all that matters is that the local context is symmetric in c and d)

#### Patrick Massot (Dec 28 2019 at 17:49):

I came across the same question last week, and I don't think `wlog`

helps here.

#### Patrick Massot (Dec 28 2019 at 17:52):

If you post a realistic MWE I can try to cook up something.

#### Kevin Buzzard (Dec 28 2019 at 17:55):

Is this realistic:

def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y} example (X : Type) (R : X → X → Prop) (HR : equivalence R) : ∀ (c d : set X), c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c = d := begin intros c d hc hd hcd, sorry end

?

#### Yury G. Kudryashov (Dec 28 2019 at 18:25):

`wlog not (c ⊂ d)`

?

#### Kevin Buzzard (Dec 28 2019 at 18:40):

I don't think that's syntactically correct (but I don't know much about `wlog`

). `wlog not (c ⊂ d)`

gives me complaints about unknown identifiers `c`

and `d`

. `wlog h: not (c ⊂ d)`

gives me

To generate cases at least two permutations are required, i.e. `using [x y, y x]` or exactly 0 or 2 variables state: X : Type, R : X → X → Prop, HR : equivalence R, c d : set X, hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hcd : c ∩ d ≠ ∅ ⊢ c = d

#### Patrick Massot (Dec 28 2019 at 18:41):

Can you write a tactic script that you would like to see reduced to one tactic?

#### Yury G. Kudryashov (Dec 28 2019 at 18:52):

Sorry, does `wlog h : (not (c ⊂ d))`

work?

#### Kevin Buzzard (Dec 28 2019 at 18:56):

I get the same error "To generate cases at least two permutations..." as above.

#### Kevin Buzzard (Dec 28 2019 at 19:10):

import tactic def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y} example (X : Type) (R : X → X → Prop) (HR : equivalence R) : ∀ (c d : set X), c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c = d := begin intros c d hc hd hcd, /- 1 goal X : Type, R : X → X → Prop, HR : equivalence R, c d : set X, hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hcd : c ∩ d ≠ ∅ ⊢ c = d -/ suffices htemp : ∀ (X : Type) (R : X → X → Prop) (HR : equivalence R) (c d : set X) (hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}) (hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}) (hcd : c ∩ d ≠ ∅), c ⊆ d, -- I want this to be my final goal apply set.subset.antisymm, exact htemp X R HR c d (by assumption) (by assumption) (by assumption), suffices htemp2 : d ∩ c ≠ ∅, -- I want this to be the last but one goal exact htemp X R HR d c (by assumption) (by assumption) (htemp2), -- `by assumption` fails for htemp2 /- currently two goals. first is ⊢ d ∩ c ≠ ∅ and we have a hypothesis hcd : c ∩ d ≠ ∅, -/ sorry, /- other goal is overkill currently: X : Type, R : X → X → Prop, HR : equivalence R, c d : set X, hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hcd : c ∩ d ≠ ∅ ⊢ ∀ (X : Type) (R : X → X → Prop), equivalence R → ∀ (c d : set X), c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c ⊆ d -/ clear hcd hd hc c d HR R X, intros X R HR c d hc hd hcd, /- X : Type, R : X → X → Prop, HR : equivalence R, c d : set X, hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x}, hcd : c ∩ d ≠ ∅ ⊢ c ⊆ d -/ sorry end

#### Kevin Buzzard (Dec 28 2019 at 19:24):

It's the "suffices : htemp" line which I can't be bothered to write. On the blackboard I'd just say "we want c=d, but it suffices to prove c sub d as the other inclusion then follows by symmetry"

#### Kevin Buzzard (Dec 28 2019 at 19:24):

I don't have to quantify over X and R, I could have left them as constants

#### Kenny Lau (Dec 29 2019 at 00:11):

import tactic.wlog def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y} example (X : Type) (R : X → X → Prop) (HR : equivalence R) : ∀ (c d : set X), c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c = d := begin classical, intros c d hc hd hcd, rw set.subset.antisymm_iff, by_contra h, rw not_and_distrib at h, wlog h1 : ¬c ⊆ d := h using [c d, d c], end

#### Kevin Buzzard (Dec 29 2019 at 01:34):

Oh nice :-) I think this is what Yury was thinking of?

Last updated: Dec 20 2023 at 11:08 UTC