feedback on two very similar (beginner) proofs

Stream: new members

[rzeta0]

The following are two very simple proofs of the same theorem. The only difference is

• apply ne_of_lt
• apply ne_of_lt at h

Question: Are there any merits to one over the other? Are there risks / bad habits that one leads to over the other?

import Mathlib.Tactic

example {n : ℕ} (h : n < 5) : n ≠ 5 := by
  apply ne_of_lt
  exact h

and

import Mathlib.Tactic

example {n : ℕ} (h : n < 5) : n ≠ 5 := by
  apply ne_of_lt at h
  exact h

[Julian Berman]

Neither are the proof someone would likely write "in real life", so it's hard to answer. Assuming the statement is something useful (which is already kind of a bit difficult to answer questions about because it would only be something someone writes in the context of either more generality or some larger proof), then I think most people would write that as example {n : ℕ} (h : n < 5) : n ≠ 5 := h.ne, or they'd use a tactic which solves the whole thing if they didn't know .ne existed, like by linarith, or they'd use whatever by exact? spits out and move on.

[Daniel Weber]

The tactic themselves aren't actually similar, and it's only because the proof is so simple that they both work. apply uses backwards reasoning — it says "I want to use this to prove the goal, I'll now prove the required assumptions for it". On the other hand, apply at uses forward reasoning — "this hypothesis is an assumption of this, so we can get the conclusion".

[Michael Rothgang]

Generally, using Lean I mostly work backwards. There are exceptions (e.g. rw, when you apply a sequence of rewrites in that order, or calc blocks), but these are not the rule. It takes some getting used to, but after a certain point is perfect natural.
If you write longer proofs*, one common theme is to state intermediate steps with have (so, using forward reasoning on the high level), but proving these intermediate steps using backward reasoning.

[Michael Rothgang]

(Side note: standard advice, particularly for mathlib-level material, is to split out all reusable results you can --- so proofs become much shorter than one may think.)

[Alex Mobius]

I sadly do write proofs like these... Next thing you tell me, there's a better version of lt_of_lt_of_le too.

[Yaël Dillies]

Yes of course there is. At least two even :grinning: : docs#LT.lt.trans_le (for dot notation) and calc blocks (for readability)

[Alex Mobius]

I still have no idea on how to use calc for inequalities, TPIL just kinda glossed over that.

[Yaël Dillies]

Have you read Heather's Mechanic of Proofs?

[Alex Mobius]

I have referenced it (: Didn't have the time to do all of the exercises yet. But evidently I should!