Using rintro to simplify derivations of A ≠ B in Lean

One of the most common goals in Lean is to prove that two objects are not equal, that is, A ≠ B. This is often done by showing that assuming A = B leads to a contradiction. To understand how to prove this, remember that the goal A ≠ B is equivalent to ¬ (A = B); that is, we need to show that we can derive False from the assumption A = B.

To solve this goal, we typically begin by loading the assumption A = B into the context with the intro tactic and then substitute A for B—i.e., we replace every occurrence of B with A in the context—as a step toward deriving a contradiction:

have : A ≠ B := by
  intro h_eq
  subst h_eq
  ...

However, we can simplify this process with the rintro tactic, which introduces the assumption and performs the substitution in a single step. This works because rintro permits the rfl modifier, which automatically replaces a term with its definition when it is equal to another term.

Here’s how we can use rintro to prove A ≠ B:

have : A ≠ B := by
  rintro rfl
  ...

This single line eliminates the need for both intro and subst, making the proof more concise and readable.