## 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 dsimpapplies this lemma, right?

Last updated: May 12 2021 at 07:17 UTC