# Zulip Chat Archive

## Stream: new members

### Topic: Proof style

#### Anatole Dedecker (Jul 28 2020 at 21:56):

Focusing on style, which of the following proof would be preferred, e.g for a contribution to mathlib ?

```
lemma exists_has_deriv_at_eq_zero' (f f' : ℝ → ℝ) {a b l : ℝ} (hab : a < b)
(hfa : tendsto f (nhds_within a $ Ioi a) (nhds l)) (hfb : tendsto f (nhds_within b $ Iio b) (nhds l))
(hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) :
∃ c ∈ Ioo a b, f' c = 0 :=
have ∃ c ∈ Ioo a b, is_local_extr (λ x, if x ≤ a then l else if b ≤ x then l else f x) c, from
exists_local_extr_Ioo
(λ x, if x ≤ a then l else if b ≤ x then l else f x)
hab
( continuous_on_Icc_of_extend_continuous_Ioo hab
( λ x hx, (hff' x hx).continuous_at.continuous_within_at )
hfa hfb )
( by simp only [le_refl, if_true, if_t_t] ),
let ⟨c, hc, hcextr⟩ := this in
have heq : (λ (x : ℝ), ite (x ≤ a) l (ite (b ≤ x) l (f x))) =ᶠ[𝓝 c] f :=
eventually_eq_iff_exists_mem.mpr
⟨ Ioo a b,
Ioo_mem_nhds hc.1 hc.2,
λ x hx, by simp only [not_le_of_lt hx.1, not_le_of_lt hx.2, if_false] ⟩,
⟨c, hc, ( hcextr.congr heq ).has_deriv_at_eq_zero $ hff' c hc ⟩
lemma exists_has_deriv_at_eq_zero'' (f f' : ℝ → ℝ) {a b l : ℝ} (hab : a < b)
(hfa : tendsto f (nhds_within a $ Ioi a) (nhds l)) (hfb : tendsto f (nhds_within b $ Iio b) (nhds l))
(hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) :
∃ c ∈ Ioo a b, f' c = 0 :=
begin
have := exists_local_extr_Ioo
(λ x, if x ≤ a then l else if b ≤ x then l else f x)
hab
( continuous_on_Icc_of_extend_continuous_Ioo hab
( λ x hx, (hff' x hx).continuous_at.continuous_within_at )
hfa hfb )
(by simp only [le_refl, if_true, if_t_t]),
rcases this with ⟨c, hc, hcextr⟩,
use c, use hc,
apply ( hcextr.congr _ ).has_deriv_at_eq_zero (hff' c hc),
apply eventually_eq_iff_exists_mem.mpr,
use Ioo a b,
use Ioo_mem_nhds hc.1 hc.2,
exact λ x hx, by simp only [not_le_of_lt hx.1, not_le_of_lt hx.2, if_false],
end
```

#### Pedro Minicz (Jul 28 2020 at 22:02):

I know its a bit off topic, but I prefer the tactic mode proof, as I find it more legible. Looking at mathlib, it seems to have a fair share of both styles, although I have never seen a long tactic mode proof there (there are long term mode proofs, which is a bit unfortunate, again, because of my readability preferences).

#### Anatole Dedecker (Jul 28 2020 at 22:05):

I agree that tactic proofs are much easier to read *if you have lean turned-on to see the tactic state*. But if you have to read them as pure text, I honestly don't know which one is more readable

#### Patrick Massot (Jul 28 2020 at 22:18):

Anatole, you can write tactic proofs that are as readable as pure text as what you can get in term mode. You only need to put more type annotation to `have`

or use `obtain`

instead of `rcases`

.

#### Patrick Massot (Jul 28 2020 at 22:21):

For instance you can hopefully start the above proof with:

```
obtain ⟨c, hc, hcextr⟩ :
∃ c ∈ Ioo a b, is_local_extr (λ x, if x ≤ a then l else if b ≤ x then l else f x) c,
```

#### Anatole Dedecker (Jul 28 2020 at 22:23):

That's way better indeed

#### Scott Morrison (Jul 28 2020 at 22:50):

I prefer the tactic style for readability/maintainability. Even better is a tactic style proof interspersed with comments!

#### Yury G. Kudryashov (Jul 30 2020 at 05:45):

BTW, we have src#has_deriv_at_of_has_deriv_at_of_ne

Possibly it should be modified to require `∀ᶠ y in nhds_within x {y | y ≠ x}, has_deriv_at f (g y) y`

instead of `∀...`

.

Last updated: May 14 2021 at 21:11 UTC