Rewrite through a chain
Use two equality hypotheses in a readable calc proof.
In this course 8 / 10
An equality hypothesis lets you replace one expression by another. With hab : a = b, the tactic rw [hab] changes occurrences of a into b in the goal.
Two equalities can be chained. A calc block records the intermediate expression, and every line supplies its own justification. The underscore begins where the previous line ended.
This is more informative than asking automation to normalize everything. A reader sees that the argument first moves from a to b, then from b to c.
The additions by one are deliberately carried through the chain. Rewriting works inside a larger expression, not only when the whole goal is exactly the equality from the context.
Worked example
example (x y : Nat) (h : x = y) : x + 2 = y + 2 := by
rw [h]One equality needs one rewrite. Your exercise composes two equalities and makes the middle expression visible.
Equality is a substitution rule. calc turns several substitutions into a proof whose intermediate steps remain visible.
Use hab and hbc in a two-step calc proof from a + 1 to c + 1.
Suggested steps
- Open a
calcchain ata + 1 - Rewrite the first step with
hab - Continue from
_and rewrite withhbc
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct