From 40274e487fa8a932a7c43bf0e5f2302f626ca9c6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 8 Aug 2021 13:26:46 +0200
Subject: [PATCH] chore: fix docs

---
 doc/tactics.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/tactics.md b/doc/tactics.md
index c24f142cf8..32d1076467 100644
--- a/doc/tactics.md
+++ b/doc/tactics.md
@@ -176,11 +176,11 @@ theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
     rw [Nat.mod_eq_sub_mod h₁.2]
     exact ih h
   | base x y h₁ =>
-     have : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.notAndIffOrNot ..) h₁
+     have : ¬ 0 < y ∨ ¬ y ≤ x := Iff.mp (Decidable.not_and_iff_or_not ..) h₁
      match this with
      | Or.inl h₁ => exact absurd h h₁
      | Or.inr h₁ =>
-       have hgt : y > x := Nat.gtOfNotLe h₁
+       have hgt : y > x := Nat.gt_of_not_le h₁
        rw [← Nat.mod_eq_of_lt hgt] at hgt
        assumption
 ```