From f08b5420682793da7054f78436d28341cc09f9ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Aug 2021 06:44:12 -0700
Subject: [PATCH] chore: add `Nat.add_mul` and `Nat.mul_add` for tutorial

---
 src/Init/Data/Nat/Basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index eeda5f150d..6a8949da42 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -126,6 +126,12 @@ protected theorem right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k :=
   have h₄ : n * k + k * m = n * k + m * k := Nat.mul_comm m k ▸ rfl
   ((h₁.trans h₂).trans h₃).trans h₄
 
+protected theorem mul_add (n m k : Nat) : n * (m + k) = n * m + n * k :=
+  Nat.left_distrib n m k
+
+protected theorem add_mul (n m k : Nat) : (n + m) * k = n * k + m * k :=
+  Nat.right_distrib n m k
+
 protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
   | n, m, 0      => rfl
   | n, m, succ k =>