Zulip Chat Archive

Stream: new members

Topic: congr


kana (Feb 18 2021 at 19:30):

How to move from a = b goal to f a = f b?

Yakov Pechersky (Feb 18 2021 at 19:37):

Do you know that f is injective?

kana (Feb 18 2021 at 19:42):

Oh, my bad, I understood why it is not correct in the general case. Thanks

Eric Wieser (Feb 18 2021 at 20:08):

apply (_ : function.injective f) would probably do it.

Bjørn Kjos-Hanssen (Aug 04 2022 at 22:54):

Is there a more idiomatic way to do these? Maybe involving some flavor of congr_...?

theorem in_eq {β:Type} (x:β) (A B: set β): A=B x A x B :=
λ he, λ hx, by {rw he at hx,exact hx,}

theorem eq_in {β:Type} (x y:β) (A: β Prop): x=y  A x  A y :=
λ he, λ hx,  by {rw he at hx,exact hx,}

Adam Topaz (Aug 04 2022 at 22:58):

theorem in_eq {β : Type} (x : β) (A B : set β): A = B  x  A  x  B :=
λ h hx, by rwa  h

theorem eq_in {β:Type} (x y : β) (A: β  Prop): x = y  A x  A y :=
λ h hA, by rwa  h

Kevin Buzzard (Aug 04 2022 at 22:59):

I guess in mathlib the idiomatic thing to do is to move as much as you can left of the colon so you don't have to do the lambdas (i.e.

theorem in_eq {β : Type} (x : β) (A B : set β) (he : A = B) (hx : x  A) : x  B :=
by { rw he at hx, exact hx, }

). Here's another proof:

theorem in_eq' {β : Type} (x : β) (A B : set β) (he : A = B) (hx : x  A) : x  B :=
by { subst he, assumption, }

Adam Topaz (Aug 04 2022 at 23:00):

or if you want to go full term-mode

theorem in_eq {β : Type} (x : β) (A B : set β): A = B  x  A  x  B :=
λ h hx, h  hx

theorem eq_in {β:Type} (x y : β) (A: β  Prop): x = y  A x  A y :=
λ h hA, h  hA

Adam Topaz (Aug 04 2022 at 23:01):

But yeah, as Kevin said, it's usually best practice to put as many hypotheses as you can to the left of the :

Adam Topaz (Aug 04 2022 at 23:01):

This also works

theorem in_eq {β : Type} (x : β) (A B : set β): A = B  x  A  x  B :=
eq.subst

theorem eq_in {β:Type} (x y : β) (A: β  Prop): x = y  A x  A y :=
eq.subst

Bjørn Kjos-Hanssen (Aug 04 2022 at 23:08):

Kevin Buzzard said:

I guess in mathlib the idiomatic thing to do is to move as much as you can left of the colon so you don't have to do the lambdas (i.e.

theorem in_eq {β : Type} (x : β) (A B : set β) (he : A = B) (hx : x  A) : x  B :=
by { rw he at hx, exact hx, }

).

Interesting; I've noticed that not everything can be moved to left of colon, e.g. when you need a strong induction hypothesis for rec_on

Adam Topaz (Aug 04 2022 at 23:11):

Yeah sometimes induction makes things complicated. It's usually possible to write induction ... generalizing ... for appropriate values of ... that should accomplish the same thing.

Adam Topaz (Aug 04 2022 at 23:12):

of if you want to use term-mode, you can match on a hypothesis instead of using the equation compiler


Last updated: Dec 20 2023 at 11:08 UTC