deprecation warning を消す

lean-ja · Nov 28, 2024 · 2592311 · 2592311
1 parent e88896c
commit 2592311
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LeanByExample/Reference/Tactic/Linarith.lean b/LeanByExample/Reference/Tactic/Linarith.lean
@@ -32,7 +32,7 @@ example (h : x ≤ y) (pos : 0 ≤ x) : x + x ^ 2 ≤ y + y ^ 2 := by
 
   -- `linarith` 単独で扱えない部分、つまり `x ^ 2 ≤ y ≤ 2` を示すための
   -- 補題を引数で渡してやると通る
-  linarith [pow_le_pow_left pos h 2]
+  linarith [pow_le_pow_left₀ pos h 2]
 
 /- ## 舞台裏
 `linarith` は一般に、型クラス `LinearOrderedCommRing` のインスタンスに対して動作します。ここで linear order とは全順序のことです。-/