## Stream: general

### Topic: and_iff_and_of_iff_and_iff

#### Johan Commelin (Oct 03 2018 at 08:04):

Would this be a useful lemma for mathlib? If so, where should it go? I currently solve this by split; intros; split, but that is a bit of a hack, and creates 4 goals where usually 2 should suffice.

theorem and_iff_and_of_iff_and_iff {P1 P2 Q1 Q2 : Prop} (H : (P1 \iff Q1) \and (P2 \iff Q2)) :
(P1 \and P2) \iff (Q1 \and Q2) := sorry


#### Mario Carneiro (Oct 03 2018 at 08:06):

This looks like and_congr

#### Johan Commelin (Oct 03 2018 at 08:08):

Cool, I'll use that! Is there a way that I could have discovered that name myself?

#### Sean Leather (Oct 03 2018 at 08:09):

I also had trouble finding that. Like me, Johan may have been look for something iff-named instead of and- and congr-named.

#### Sean Leather (Oct 03 2018 at 08:11):

I probably tried git grep 'and.*iff' and git grep 'iff.*and'.

#### Mario Carneiro (Oct 03 2018 at 08:11):

That's true. This is a special pattern, like ext. congr lemmas mean if the inputs are equal then a function applied to those inputs is equal

#### Mario Carneiro (Oct 03 2018 at 08:13):

There are similar theorems for all the propositional functions, and for regular functions congr the tactic will often generate these on the fly

#### Mario Carneiro (Oct 03 2018 at 08:16):

You will also find custom congr lemmas for things like list.map_congr, where we want to insert an additional assumption into the hypothesis (if \all x \in l, f x = g x then map f l = map g l)

#### Mario Carneiro (Oct 03 2018 at 08:17):

so many higher order functions have some kind of altered congr lemma

Last updated: May 10 2021 at 23:11 UTC