Skip to content

Commit

Permalink
replace rw by simp
Browse files Browse the repository at this point in the history
  • Loading branch information
@yannickseurin @avigad
yannickseurin authored and avigad committed Aug 19, 2024
1 parent 8719991 commit 2956151
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down

0 comments on commit 2956151

Please sign in to comment.