# Zulip Chat Archive

## Stream: maths

### Topic: rfl lemma

#### Thomas Browning (Dec 23 2020 at 21:47):

The lemma `adjoin_empty`

in field_theory/adjoin is actually a rfl-lemma. Is it worth making a PR?

```
@[simp] lemma adjoin_empty (F E : Type*) [field F] [field E] [algebra F E] :
adjoin F (∅ : set E) = ⊥ :=
eq_bot_iff.mpr (adjoin_le_iff.mpr (set.empty_subset _))
```

```
@[simp] lemma adjoin_empty (F E : Type*) [field F] [field E] [algebra F E] :
adjoin F (∅ : set E) = ⊥ := rfl
```

#### Patrick Massot (Dec 23 2020 at 21:52):

There is no problem at all with PRs that are easy to review.

#### Bryan Gin-ge Chen (Dec 23 2020 at 22:04):

@Mario Carneiro once gave some reasons why we shouldn't replace all possible proofs with `rfl`

when possible; not sure whether that advice applies in this case though.

#### Mario Carneiro (Dec 23 2020 at 22:05):

The question is whether the defeq can be proven using only "public" defeq facts

#### Mario Carneiro (Dec 23 2020 at 22:07):

I think it is fair to say that `bot = empty = {x | false]`

is public, but I don't know much about `adjoin`

#### Mario Carneiro (Dec 23 2020 at 22:09):

Looking around it seems like you have to dig through many layers to get this result, so I would say that it shouldn't be public

#### Mario Carneiro (Dec 23 2020 at 22:10):

it seems like `adjoin_le_iff`

is the API for adjoin

#### Eric Wieser (Dec 23 2020 at 22:53):

Using `rfl`

vs not affects whether `dsimp`

applies this lemma, right?

Last updated: May 12 2021 at 07:17 UTC