Intro to Math Reasoning Lean Commands

calc

Used to write calculational proofs, such as showing a

sequence of steps, like a = b = c ≤ d, and so on.

simp

The simp tactic automatically simplifies the goal by re-

peatedly applying a large database of established rewrite

rules and definitions.

ring

Used to automatically prove algebraic identities in any

commutative ring. This includes properties like associa-

tivity, commutativity, and distributivity of addition and

multiplication.

congr

Used to simplify goals that are equalities from applica-

tions of functions. If you want to prove f x = f y, congr

reduces the goal to proving x = y.

gcongr

Another version of congr that works for inequalities.

While congr needs arguments to be equal, gcongr uses

monotonicity rules. For example, if f is an increasing

function and x ≤ y, then f x ≤ f y.

unfold

expose a chosen definition.

constructor

This tactic breaks a goal into the parts needed to prove

it. For example, to prove P ∧ Q, you must prove both

P and Q. Applying constructor creates two separate

goals: prove P and prove Q

refine

This supplies a partially completed proof, leaving place-

holders such as ?_ as new goals. For example, if the goal

is

∃m : N, m = n + 2,

then

refine 〈n + 2, ?_〉

chooses the witness n + 2 and leaves the goal

n + 2 = n + 2

rw

This rewrites a goal or hypothesis using an equality or

equivalence. If h : a = b, then

rw [h]

replaces matching occurrences of a by b in the goal.

To rewrite within a hypothesis named h2, use:

rw [h] at h2

linarith

This proves goals using linear arithmetic equations and

inequalities

cases

If the hypothesis h states P ∨ Q, then the tactic cases

splits the proof into two branches: one assuming P , and

the other assuming Q

rcases

This splits a hypothesis into cases and lets us name the

resulting hypotheses. For example, if h states P ∨ Q,

then

rcases h with hp | hq

creates two branches: one with the hypothesis hp stat-

ing P , and the other with the hypothesis hq stating Q.

The vertical bar separates the two alternatives. Unlike

cases, rcases can unpack several nested logical struc-

tures in a single command