intro inside iff

Stream: new members

[Danila Kurganov]

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

[Mario Carneiro]

apply forall_congr, intro x

[Jalex Stark]

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

[Mario Carneiro]

The congr tactic should really be able to do this

[Jalex Stark]

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

[Danila Kurganov]

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

[Kevin Buzzard]

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

[Danila Kurganov]

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