simp or term proof in library

Stream: new members

[Anatole Dedecker]

When writing lemmas for the library, should we prefer a one-line simp proof (squeezified if necessary) or a few lines of term proof ? I know the term way is probably the fastest, but maybe there are other citerions to choose ?

[Anatole Dedecker]

Example : which should I choose here ?

import order.filter.basic

open filter
open_locale filter

lemma tendsto_sup {α β : Type*} (F G : filter α) (l : filter β) (f : α → β) :
  (tendsto f (F ⊔ G) l ↔ tendsto f F l ∧ tendsto f G l) :=
⟨ λ h,
  ⟨ tendsto_def.2 (λ s, λ hs, (mem_sup_sets.1 $ tendsto_def.1 h s hs).1),
    tendsto_def.2 (λ s, λ hs, (mem_sup_sets.1 $ tendsto_def.1 h s hs).2) ⟩,
  λ ⟨ h1, h2 ⟩, tendsto_def.2 $ λ s, λ hs, mem_sup_sets.2 ⟨ h1 hs, h2 hs ⟩ ⟩

lemma tendsto_sup' {α β : Type*} (F G : filter α) (l : filter β) (f : α → β) :
  (tendsto f (F ⊔ G) l ↔ tendsto f F l ∧ tendsto f G l) :=
by simp only [tendsto, map_sup, sup_le_iff]

[Scott Morrison]

I read these two proofs as:

1. "err... I guess I'm going to have to remember exactly how we've defined tendsto in the library before I understand this"
2. "the statement looks sensible, and apparently it follows easily from stuff we've already done, so lets keep going"

[Reid Barton]

There are also better term-mode proofs--not necessarily better than the by simp proof though.

[Anatole Dedecker]

I'm not really good at term mode yet :sweat_smile:

[Reid Barton]

apparently map_sup turns out to be a definitional equality, so one possibility is

lemma tendsto_sup {α β : Type*} (F G : filter α) (l : filter β) (f : α → β) :
  (tendsto f (F ⊔ G) l ↔ tendsto f F l ∧ tendsto f G l) :=
@sup_le_iff _ _ (F.map f) (G.map f) _

[Reid Barton]

or you can also help out Lean with show