congr

Stream: new members

[kana]

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

[Yakov Pechersky]

Do you know that f is injective?

[kana]

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

[Eric Wieser]

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

[Bjørn Kjos-Hanssen]

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]

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]

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]

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]

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]

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]

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]

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]

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