From 9bb5d4dc93b7cb3479bc78c70cd79c6c3999c312 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Sep 2021 07:51:41 -0700
Subject: [PATCH] chore: `Nat.ltWf` => `Nat.lt_wf`

---
 src/Init/Data/Nat/Div.lean | 10 +++++-----
 src/Init/Data/Nat/Gcd.lean |  2 +-
 src/Init/WF.lean           |  4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index 338eaf0671..ef69149895 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -16,12 +16,12 @@ private def div.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) :
 
 @[extern "lean_nat_div"]
 protected def div (a b : @& Nat) : Nat :=
-  WellFounded.fix ltWf div.F a b
+  WellFounded.fix lt_wf div.F a b
 
 instance : Div Nat := ⟨Nat.div⟩
 
 private theorem div_eq_aux (x y : Nat) : x / y = if h : 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
-  congrFun (WellFounded.fix_eq ltWf div.F x) y
+  congrFun (WellFounded.fix_eq lt_wf div.F x) y
 
 theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
   dif_eq_if (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0 ▸ div_eq_aux x y
@@ -39,19 +39,19 @@ theorem div.inductionOn.{u}
       (ind  : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
       (base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y)
       : motive x y :=
-  WellFounded.fix Nat.ltWf (div.induction.F motive ind base) x y
+  WellFounded.fix Nat.lt_wf (div.induction.F motive ind base) x y
 
 private def mod.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) : Nat :=
   if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y else x
 
 @[extern "lean_nat_mod"]
 protected def mod (a b : @& Nat) : Nat :=
-  WellFounded.fix ltWf mod.F a b
+  WellFounded.fix lt_wf mod.F a b
 
 instance : Mod Nat := ⟨Nat.mod⟩
 
 private theorem mod_eq_aux (x y : Nat) : x % y = if h : 0 < y ∧ y ≤ x then (x - y) % y else x :=
-  congrFun (WellFounded.fix_eq ltWf mod.F x) y
+  congrFun (WellFounded.fix_eq lt_wf mod.F x) y
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
   dif_eq_if (0 < y ∧ y ≤ x) ((x - y) % y) x ▸ mod_eq_aux x y
diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean
index f2c51e4d8c..86aff647d9 100644
--- a/src/Init/Data/Nat/Gcd.lean
+++ b/src/Init/Data/Nat/Gcd.lean
@@ -15,7 +15,7 @@ private def gcdF (x : Nat) : (∀ x₁, x₁ < x → Nat → Nat) → Nat → Na
 
 @[extern "lean_nat_gcd"]
 def gcd (a b : @& Nat) : Nat :=
-  WellFounded.fix ltWf gcdF a b
+  WellFounded.fix lt_wf gcdF a b
 
 @[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
   rfl
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index de9c3ff473..b23bb4da73 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -144,7 +144,7 @@ def wf (h : WellFounded r) : WellFounded (TC r) :=
 end TC
 
 -- less-than is well-founded
-def Nat.ltWf : WellFounded Nat.lt := by
+def Nat.lt_wf : WellFounded Nat.lt := by
   apply WellFounded.intro
   intro n
   induction n with
@@ -164,7 +164,7 @@ def measure {α : Sort u} : (α → Nat) → α → α → Prop :=
   InvImage (fun a b => a < b)
 
 def measureWf {α : Sort u} (f : α → Nat) : WellFounded (measure f) :=
-  InvImage.wf f Nat.ltWf
+  InvImage.wf f Nat.lt_wf
 
 def sizeofMeasure (α : Sort u) [SizeOf α] : α → α → Prop :=
   measure sizeOf