Mastering the `injection` tactic in Lean 4

Before moving on to the definition of order relations, this time I'll work through proving the theorem m * n = 0 → m = 0 ∨ n = 0 as an example of applying the injection tactic. As always, my reference is "Getting Started with Lean from Scratch: Learning Formal Mathematics Library Development Hands-On."

Reviewing the injection tactic

The injection tactic makes use of the following properties of the Peano axioms.

• The successor of distinct natural numbers is distinct
• 0 and the successor of any number are always distinct

Proving a lemma for addition

As preparation for proving m * n = 0 → m = 0 ∨ n = 0, I'll first prove that m + n = 0 → m = 0 ∧ n = 0 holds for addition. Using induction, once the hypothesis and goal are transformed as follows, injection comes into play.

ih : m + n = 0 → m = 0 ∧ n = 0
h : m + n + 1 = 0 
⊢ False

Since m + n + 1 = 0 reduces to m + n + 1 = MyNat.succ (m + n), we can derive a contradiction using the property that the successor of distinct natural numbers is distinct.

theorem MyNat.eq_zero_of_add_eq_zero : m + n = 0 → m = 0 ∧ n = 0 := by
  intro h
  induction n with
  | zero => -- h : m + 0 = 0 ⊢ m = 0 ∧ 0 = 0
    simp_all
  | succ n ih =>
    -- ih : m + n = 0 → m = 0 ∧ n = 0
    -- h : m + (n + 1) = 0
    -- ⊢ m = 0 ∧ n + 1 = 0
    exfalso -- ih : m + n = 0 → m = 0 ∧ n = 0 h : m + (n + 1) = 0 ⊢ False
    rw [show m + (n + 1) = m + n + 1 from by ac_rfl] at h
    injection h

I'll also prove the reverse implication and register the combined equivalence with simp.

theorem MyNat.add_eq_zero_of_eq_zero : m = 0 ∧ n = 0 → m + n = 0 := by
  intro h
  simp_all
@[simp]
theorem MyNat.add_eq_zero_iff_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0 := by
  exact ⟨ MyNat.eq_zero_of_add_eq_zero, MyNat.add_eq_zero_of_eq_zero ⟩

Proving m * n = 0 → m = 0 ∨ n = 0

Now for the main event. I'll prove m * n = 0 → m = 0 ∨ n = 0. Using induction, the case where n is 0 is trivial, so simp_all handles it. For the n + 1 case, we need to prove h : m * (n + 1) = 0 ⊢ m = 0 ∨ n + 1 = 0.

First, using distrib for the distributive law, we rewrite this as m * (n + 1) = m * n + m. Looking at the goal, since n + 1 = 0 can't hold, we know it suffices to show m = 0. From there, simp_all can derive m = 0 from m * n + m = 0, completing the proof.

Since this is set up as a proof of equivalence, the trivial right-to-left implication is also handled by simp_all.

@[simp]
theorem MyNat.mul_eq_zero (m n : MyNat) : m * n = 0 ↔ m = 0 ∨ n = 0 := by
  constructor <;> intro h
  case mpr =>
    cases h <;> simp_all
  case mp =>
    induction n with
    | zero =>
      simp_all
    | succ n _ =>
    -- a✝ : m * n = 0 → m = 0 ∨ n = 0
    -- h : m * (n + 1) = 0
    -- ⊢ m = 0 ∨ n + 1 = 0
      have : m * n + m = 0 := calc
        _ = m * (n + 1) := by distrib
        _ = 0 := by rw [h]
      simp_all

The code for this post is available in the following repository.

https://github.com/ringring-creator/LearnLean