General Notes On Lean

We start off with some Lean-specific definitions.

A proposition (Prop) is a statement that is either true or false.

A predicate is a function that takes arguments and returns a Prop.

Example:

/-- The sequence `u` of real numbers converges to `l`. -/
def SequenceHasLimit (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |u n - l| < ε

For example, SequenceHasLimit is a predicate of type (ℕ → ℝ) → ℝ → Prop.

Partially applying it, SequenceHasLimit u is of type ℝ → Prop — it takes a real number l and returns the proposition that u converges to l.

Only when all arguments are supplied do we get a Prop. That is, SequenceHasLimit u x₀ is a Prop — it is the statement that the sequence^[1] u converges to x₀, defined as:

$$\forall \varepsilon > 0, \exists N \in \mathbb{N}, \forall n \geq N, |u_n - x_0| < \varepsilon$$

This statement may or may not have a proof, but it is a well-formed proposition.

A Note: Curried Functions#

In Lean (and in type theory generally), multi-argument functions are curried by default, not tupled. So:

#check (add_complex_i : ℂ → ℂ)

def less_than_pi (x : ℝ) : Prop := x < π

#check less_than_pi
-- ⊢ ℝ → Prop


def less_than (x y : ℝ) : Prop :=
  x < y

-- ℝ → (ℝ → Prop)
#check (less_than)

The difference between these two signatures is:

• ℝ → ℝ → Prop (curried) — takes one ℝ, returns a function ℝ → Prop. This is what Lean uses.

First Proof#

Now let us look at a slightly non-trivial first proof in Lean. We start off by defining what it means for a sequence to have a limit, and for a function to be continuous.

/-- The sequence `u` of real numbers converges to `l`. -/
def SequenceHasLimit (u : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |u n - l| < ε

/-- The function `f : ℝ → ℝ` is continuous at `x₀`. -/
def ContinuousAtPoint (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ →
  |f (x) - f (x₀)| < ε

Then we state our first lemma:

We first prove this theorem on “paper” like we are used to, but in a way that is directly (or almost directly) translatable to Lean. This will give us a mental model of how to think of proofs in Lean. The unfold commands just expand out the goals for better viewing.

 1lemma first_proof (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
 2    (u_lim : SequenceHasLimit u x₀)
 3    (f_cont : ContinuousAtPoint f x₀) :
 4    SequenceHasLimit (f ∘ u) (f x₀) := by {
 5  unfold SequenceHasLimit
 6  -- Let ε > 0 be arbitrary
 7  intro (ε : ℝ) (hε : ε > 0)
 8  -- Since `f` is continuous, we can pick a `δ > 0` such that
 9  -- for all `x`, `|x - x₀| < δ → |f(x) - f(x₀)| < ε`.
10  unfold ContinuousAtPoint at f_cont
11  -- We want to invoke f_cont with eps and by assumption
12  obtain ⟨δ, hδ, f_prop⟩ := f_cont ε (by exact hε )
13  -- obtain ⟨δ, hδ, f_prop⟩ := f_cont ε (by assumption) -- also works if we don't want to remember hε 
14  -- Since `u` converges to `x₀`, we can pick a `N` such that
15  -- for all `n ≥ N`, `|u_n - x₀| < δ`.
16  unfold SequenceHasLimit at u_lim 
17  obtain ⟨N, u_prop⟩ := u_lim δ hδ
18  -- We pick this `N` to show that `f ∘ u` has limit `f(x₀)`.
19  use N
20  -- If `n ≥ N` we have `|u_n - x₀| < δ`,
21  intro m hn
22  specialize u_prop m hn
23  -- hence `|f(u_m) - f(x₀)| < ε`.
24  specialize f_prop (u m) u_prop
25  -- This finishes the proof.
26  exact f_prop  
27  }

Some comments:

obtain ⟨δ, hδ, f_prop⟩ := f_cont ε hε

or if you wanted to be maximally explicit with by:

have hε' : ε > 0 := by exact hε
obtain ⟨δ, hδ, f_prop⟩ := f_cont ε hε'

The (by assumption) on Line 13 is just finding hε : ε > 0 from the context automatically. Since you already have hε in scope, you can pass it directly as a term — no tactic needed at all. The by assumption version is a convenience for when you don’t want to remember/type the exact hypothesis name.

The Re Write Tactic#

example (a b c d : ℝ) (h : a + b = c - d) : 2 * (a + b) = 2 * c - 2 * d := by {
  rw [h, mul_sub]
  }

The rw tactic takes a list of rewrite rules and applies them left to right, in sequence. So rw [h, mul_sub] does two rewrites:

h — rewrites a + b to c - d, transforming the goal from 2 * (a + b) = 2 * c - 2 * d to 2 * (c - d) = 2 * c - 2 * d mul_sub — this is a Mathlib lemma stating a * (b - c) = a * b - a * c. It rewrites 2 * (c - d) to 2 * c - 2 * d, making the goal 2 * c - 2 * d = 2 * c - 2 * d, which closes automatically by reflexivity. Alternatively,

example (a b c d : ℝ) (h : a + b = c - d) : 2 * (a + b) = 2 * c - 2 * d := by {
  rw [h]
  rw [mul_sub]
}

also works.

The Ring Tactic#

Basic properties of addition, subtraction and multiplication that are supported by rings are handled by the ring tactic.

example (a b c d : ℝ) (h : a + b = c - d) : 2 * (a + b) = 2 * c - 2 * d := by {
  rw [h]
  ring 
}

This also works instead of re-writing mul_sub.

Simp#

Next tactic we have in computation is the simplifier simp. It will repeatedly apply a number of lemmas that are marked as simplification lemmas. For instance the proof below simplifies x - x to 0 and then |0| to 0.

Intro + Apply#

The apply tactic can be used to specialize universally quantified statements.

example (f : ℝ → ℝ) (hf : even_fun f) : f (-3) = f 3 := by
  apply hf 3

/-
Fortunately, Lean is willing to work for us, so we can leave out the `3` and
let the `apply` tactic compare the goal with the assumption
and decide to specialize it to `x = 3`.
-/

example (f : ℝ → ℝ) (hf : even_fun f) : f (-3) = f 3 := by
  apply hf

/-
In the following exercise, you get to choose whether you want help from Lean
or do all the work.
-/
example (f : ℝ → ℝ) (hf : even_fun f) : f (-5) = f 5 := by
  apply hf (5)

When i want to prove something like for all $x \in X$, $f(x)$ is true, i use the intro tactic. The intro tactic is akin to when we write in a real proof, let $x$ be an arbitrary element of set $X$, and then we prove that $f(x)$ is true.

example (f g : ℝ → ℝ) (hf : even_fun f) : even_fun (g ∘ f) := by
  unfold even_fun
  intro x
  specialize hf x
  calc
    (g ∘ f) (-x) = g (f (-x)) := by simp
    _            = g (f x) := by rw [hf]
    _            = (g ∘ f) (x) := by simp

In the above example we introduce $x$ and then specialise the hf function at x.

Alternate proof using apply

example (f g : ℝ → ℝ) (hf : even_fun f) : even_fun (g ∘ f) := by
  intro x
  calc
    (g ∘ f) (-x) = g (f (-x))   := by simp
    _            = g (f x)      := by congr 1; apply hf

A note about how apply works

apply H : H must be a hypothesis or theorem with type P1 -> P2 -> ... -> PN -> Q, where the goal has type Q. This tactic will replace the goal with N separate goals, P1, through PN, as it corresponds to deciding to prove the premises of H and then using it to prove the goal. In the simply case where you just have P -> Q this will replace Q with P.

In the above example, after congr 1, we had to prove f (-x) = f x, so why did apply hf work when hf: even_fun f? The reason for this is for any predicate P

∀ x, P x is definitionally (x : ℝ) → P x in Lean’s type theory. So apply on a universally quantified hypothesis works exactly like the P → Q pattern — the “premise” is just the implicit argument that Lean resolves automatically.

even_fun f unfolds to ∀ x, f (-x) = f x, which in Lean’s type theory is:

hf : (x : ℝ) → f (-x) = f x

So when I did apply hf, Lean then asked for an intro x which we had.

• P (premise): (x : ℝ) — you need to provide a real number
• Q (conclusion): f (-x) = f x — you get a proof of equality for that number. And as I did intro x I had a proof for that number.

This is how we say the apply tactic allows us to specialise. Alternatively, I could have specialised h earlier, and not needed to use hf.

def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂
example (f : ℝ → ℝ) (hf : non_decreasing f) (x₁ x₂ : ℝ) (hx : x₁ ≤ x₂) : f x₁ ≤ f x₂ := by
  apply hf x₁ x₂ hx

Here as hf is telling us that f is non_decreasing, so when we apply hf with the argumeents x1, x2 and the hypothesis that x1 <= x2, we reduce to getting what we need.

R cases#

In order to use h : ∃ x, P x, we use the rcases tactic to fix one x₀ that works.

example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := by
  rcases h₁ with ⟨k, hk⟩ -- we fix some `k` such that `b = a * k` i.e. hk: b = a * k
  rcases h₂ with ⟨l, hl⟩ -- we fix some `l` such that `c = b * l` i.e. hl: c = b * l
  -- Since `a ∣ c` means `∃ k, c = a*k`, we need the `use` tactic.
  use k*l
  calc
    c = b*l     := by congr
    _ = (a*k)*l := by congr
    _ = a*(k*l) := by ring

Complex Applies with specialise#

-- You don't need to specialise but this is more exolicit
example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) :
    non_increasing (g ∘ f) := by
  unfold non_increasing at *
  unfold non_decreasing at *
  intro x1 x2 hx
  specialize hf x1 x2
  specialize hg (f (x1)) (f (x2))
  apply hg
  apply hf
  exact hx

Scratch Notes From Bhavik Mehta’s course#

Sheet 1#

1. Tactics learned : intro, exact, apply

When the goal is P->Q we want to use the intro tactic, which in plain English is just saying, assume $P$ holds. Then the goal becomes to show $Q$ holds. Alternatively, when the goal is Q and we have an hypothesis that h: P->Q then apply h will make the new goal P. We can name our intro variables intro (fish: P) will create a proof fish: P of prop P. The default names are likely h.

These are the absolute basics of lean works.

2. trivial, exfalso

The trivial tactic in Lean 4 (and Mathlib) is a simple “try the obvious things” tactic. It runs a fixed sequence of cheap closing tactics and succeeds if any of them closes the goal. What it tries, roughly in order, includes rfl, assumption, contradiction, True.intro (for trivial-style True goals).

• change: I use this heavily in Bytecode expansions too.
• by_contra
• by_cases
• gcongr
• obtain or rcases

linarith handles linear arithmetic.

Obtain#

Pulling Out the Existential#

Say you have a proof of the following proposition.

hb : ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < eps0 / 2

Then

obtain <b0, hb0> := hb

sets b0 as the existential B, and hb0 is the proof that ∀ (n : ℕ), B ≤ n → |b n - u| < eps0 / 2

  rcases hb with ⟨B_1, hb1 ⟩

also does the same thing

A note on exact vs rw

• exact h uses h as a proof — h’s type must be the whole goal.
  • rw [h] uses h as a substitution rule — it finds one side of h inside the goal and swaps it for the other side. The goal can be anything (an =, a <, P x, …).

Another use case of rcases#

theorem lt_trichotomy.{u_1} {α : Type u_1} [LinearOrder α] (a b : α) : a < b ∨ a = b ∨ b < a

Says: for any two elements a,b of a linearly ordered type, exactly one of three things holds.

1. Either a < b
2. a = b
3. a > b.

To use we do

rcases lt_trichotomy c 0 with hc | hc | hc
-- this gives 3 cases
· 
·  
· 

Simp#

The three components

simp only [mul_comm c] at h2 └─ tactic └─ lemma set └─ target

• simp — the simplifier: it rewrites a goal/hypothesis by repeatedly applying equational lemmas left-to-right until nothing more fires.
• only — restricts simp to exactly the lemmas you list. Plain simp also throws in the entire default simp set (thousands of @[simp]-tagged lemmas); simp only uses nothing but [mul_comm c]. More predictable, faster, and won’t accidentally rewrite other things.
• [mul_comm c] — the single rewrite rule to use (more on this below).
• at h2 — apply the rewriting to hypothesis h2 instead of the goal. Without at h2, simp acts on the goal; with it, simp transforms h2 in place.

Difference between change and show?#

what is the diff between change and show ? minimal example please

⏺ In tactic mode, for the current goal they’re interchangeable: both restate the goal to a definitionally equal expression. The differences are at the edges.

The overlap (identical behavior)

example : 2 + 2 = 4 := by show 4 = 4 – ✓ 2+2 reduces to 4 definitionally rfl

example : 2 + 2 = 4 := by change 4 = 4 – ✓ exactly the same effect rfl

Difference 1 — change can target hypotheses, show can’t

example (h : 2 + 2 = 4) : True := by change 4 = 4 at h – ✓ rewrites h to h : 4 = 4 trivial

show 4 = 4 at h is a syntax error — show has no at clause. This is the main practical difference: change works on the goal and on hypotheses.

Difference 2 — change has a … with … replacement form

change a with b replaces a defeq subterm a by b everywhere it appears:

example : [1] ++ [2] = [1, 2] := by change [1] ++ [2] with [1, 2] – ✓ swap a subterm for a defeq one rfl

show has no such form — it only ever takes the whole new goal.

Difference 3 — show can select among multiple goals; works in term mode

When several goals are open, show brings the first defeq-matching one to the front:

example : Nat ∧ Bool := by constructor show Bool – reorders: now proving Bool first · exact true · exact 0

And show is also a term-mode keyword (show T from e, or (show T by tac)), whereas change is tactic-only.

Summary

┌────────────────────────────────────┬──────┬────────┐ │ │ show │ change │ ├────────────────────────────────────┼──────┼────────┤ │ Restate current goal (up to defeq) │ ✓ │ ✓ │ ├────────────────────────────────────┼──────┼────────┤ │ Act on a hypothesis (at h) │ ✗ │ ✓ │ ├────────────────────────────────────┼──────┼────────┤ │ Replace a subterm (a with b) │ ✗ │ ✓ │ ├────────────────────────────────────┼──────┼────────┤ │ Select/reorder among goals │ ✓ │ ✗ │ ├────────────────────────────────────┼──────┼────────┤ │ Usable in term mode │ ✓ │ ✗ │ └────────────────────────────────────┴──────┴────────┘

Rule of thumb: reach for show when you just want to re-display the goal more readably (especially to pick a goal); reach for change when you need to rewrite a hypothesis or a subterm by definitional equality.

True Vs Fale#

trivial is a “try the cheap stuff” tactic. It’s essentially a first | … | … that runs a fixed list of lightweight closing tactics in order and succeeds as soon as one of them closes the goal; if none do, trivial fails. The list includes (roughly):

• rfl — goal is a = a / a ≤ a / Iff.rfl etc. by reflexivity
• exact trivial — closes a True goal (see below)
• assumption — some hypothesis is the goal
• contradiction — there’s a False/absurd hypothesis in context

example : True := by trivial – via True.intro example (h : p) : p := by trivial – via assumption example : 2 + 2 = 4 := by trivial – via rfl example (h : False) : p := by trivial – via contradiction

It deliberately does no real reasoning — it won’t do arithmetic beyond rfl, won’t case-split, etc. It’s a convenience for goals that should close instantly. If trivial fails, that’s a hint you need an actual tactic.

True and False are propositions, not values

This is the key clarification: True and False live in Prop, and “provable” is the right lens, not “true/false.”

True : Prop — has exactly one constructor, True.intro (also named trivial as a term). So there’s always a proof; a True goal is always closable:

example : True := True.intro – or: trivial

False : Prop — has no constructors. So in a consistent system there’s no proof of False — a bare False goal is never provable:

example : False := ? – impossible; nothing to put here

Its power runs the other way: from a proof of False you can derive anything (False.elim : False → C):

example (h : False) : p := False.elim h

So to your question — “is False/True always true?”:

• True is always provable. ✓ always
• False is never provable (on its own). ✗ never
• But statements about False can be provable — e.g. False → p (vacuously true), or ¬False (which is False → False):

example : False → p := fun h => h.elim – ✓ provable, vacuously example : ¬ False := fun h => h – ✓ provable

Bonus: don’t confuse True/False (Prop) with true/false (Bool)

True False : Prop – propositions; you prove them true false : Bool – data values; you compute with them

Prop is about provability (a True goal needs a proof term True.intro). Bool is about computation (true/false are concrete values you can branch on with if, test for equality, etc.). They’re bridged by decide/Decidable when a proposition is decidable, but they’re fundamentally different layers. Mixing them up is a very common early stumbling block.

Explicit vs Implicit#

Short version: use explicit () for a reusable lemma like this — it matches Mathlib convention and stays flexible. But let me show you exactly how the choice interacts with your call site, because that’s the real consideration.

How each choice behaves at the call site

Your calc step’s goal is fully determined: |a n - b n - t| + |b n - u| on the right, so Lean can infer a and b by unification.

Implicit {a b : ℝ}: exact basic_triangle – ✓ a, b inferred from the goal exact basic_triangle (a n - b n - t) (b n - u) – ✗ can’t pass implicits positionally

Explicit (a b : ℝ): exact basic_triangle _ _ – ✓ underscores → unification fills them exact basic_triangle (a n - b n - t) (b n - u) – ✓ explicit, self-documenting exact basic_triangle – ✗ it’s a function, not a proof of the goal

So your two commented alternatives each only work with one of the two binder styles — that’s the crux of your question.

The rule of thumb

Make an argument implicit when it’s inferable and you’ll essentially never want to write it. Make it explicit when the caller may want to choose/supply it. For a and b here: they appear only in the conclusion, so they’re inferable in backward use (exact against a goal) — but in forward use (have h := basic_triangle …) Lean would have nothing to infer from and you’d get stuck metavariables. Explicit avoids that trap.

This is exactly why Mathlib’s real version uses explicit args:

theorem abs_add (a b : α) : |a + b| ≤ |a| + |b|

Tricks#

Right — Real.mul_self_sqrt wants 0 ≤ ε but you have hε : 0 < ε. Just weaken it with .le:

_ = ε := Real.mul_self_sqrt hε.le

hε.le is dot-notation for le_of_lt hε — every h : a < b has a .le field (LT.lt.le) giving a ≤ b. It’s the idiomatic one-character way to go from strict to non-strict.

(No need for refine here since there are no remaining holes — exact/bare term works. refine Real.mul_self_sqrt hε.le would also be fine, just unnecessary.)

Handy cousins for the reverse-ish situations, while you’re collecting these:

• hε.ne’ : ε ≠ 0 (from 0 < ε)
• hε.ne : 0 ≠ ε
• le_of_lt hε : the longhand for hε.le

1. In Lean sequeqnces are modelled as functions from the naturals to the reals (or whatever domain we are sequencing over). ↩