rfl lemma

Stream: maths

[Thomas Browning]

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]

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

[Bryan Gin-ge Chen]

@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]

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

[Mario Carneiro]

I think it is fair to say that bot = empty = {x | false] is public, but I don't know much about adjoin

[Mario Carneiro]

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]

it seems like adjoin_le_iff is the API for adjoin

[Eric Wieser]

Using rfl vs not affects whether dsimpapplies this lemma, right?