Stream: new members
Topic: intro inside iff
Danila Kurganov (Jul 13 2020 at 13:28):
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 (Jul 13 2020 at 13:28):
apply forall_congr, intro x
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
Mario Carneiro (Jul 13 2020 at 13:45):
congr tactic should really be able to do this
Jalex Stark (Jul 13 2020 at 13:51):
I agree. I spent a minute trying to massage it into a form where
congr' did something, but this didn't work.
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!
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
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