Zulip Chat Archive

Stream: new members

Topic: intro inside iff


view this post on Zulip Danila Kurganov (Jul 13 2020 at 13:28):

Hi,

Is there any way to do a version of intro x, where the x is then introduced (removed) from both sides of the goal statement at once?
⊢ (∀ (x : X), x ∈ A → x ∈ B) ↔ ∀ (x : X), x ∈ B ↔ x ∈ A ∪ B

view this post on Zulip Mario Carneiro (Jul 13 2020 at 13:28):

apply forall_congr, intro x

view this post on Zulip Jalex Stark (Jul 13 2020 at 13:44):

for what it's worth, forall_congr comes up if you ask suggest for advice (although it's not quite at the top of the list)

import tactic
example (X: Type) (A B : set X) : ( (x : X), x  A  x  B)   (x : X), x  B  x  A  B :=
begin
  suggest,
end

view this post on Zulip Mario Carneiro (Jul 13 2020 at 13:45):

The congr tactic should really be able to do this

view this post on Zulip Jalex Stark (Jul 13 2020 at 13:51):

I agree. I spent a minute trying to massage it into a form where congr or congr' did something, but this didn't work.

view this post on Zulip Danila Kurganov (Jul 13 2020 at 14:09):

I think I got a little tunnel vision doing a problem and forgot I could even do suggest!

view this post on Zulip Kevin Buzzard (Jul 13 2020 at 16:05):

@Danila Kurganov in some sense the reason this isn't easier (e.g. "true by definition") is that it's only a one way implication. "forall x, (P x <-> Q x)" certainly implies "(forall x, P x) <-> (forall x, Q x)", but the other implication is false in general. That's why you have to apply something.

view this post on Zulip Danila Kurganov (Jul 13 2020 at 21:00):

That's a good point, so for backwards reasonings generally


Last updated: May 13 2021 at 18:26 UTC