# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC