From 295615104e9c4c5353c26604dae2929983a0da37 Mon Sep 17 00:00:00 2001
From: Yannick Seurin <yannick.seurin@gmail.com>
Date: Sat, 20 Jul 2024 16:42:38 +0200
Subject: [PATCH] replace `rw` by `simp`

---
 .../S02_Induction_and_Recursion.lean                          | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
index ca4aa36a..2431acb4 100644
--- a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
+++ b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
@@ -239,8 +239,8 @@ EXAMPLES: -/
 -- QUOTE:
 example (n : ℕ) : fac n = ∏ i in range n, (i + 1) := by
   induction' n with n ih
-  · rw [fac, prod_range_zero]
-  rw [fac, ih, prod_range_succ, mul_comm]
+  · simp [fac, prod_range_zero]
+  simp [fac, ih, prod_range_succ, mul_comm]
 -- QUOTE.
 
 /- TEXT: