First round of updates

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -167,7 +167,7 @@ theorem countedSequence_finite : ∀ p q : ℕ, (countedSequence p q).Finite
     rw [counted_succ_succ, Set.finite_union, Set.finite_image_iff (List.cons_injective.injOn _),
       Set.finite_image_iff (List.cons_injective.injOn _)]
     exact ⟨countedSequence_finite _ _, countedSequence_finite _ _⟩
-termination_by _ p q => p + q -- Porting note: Added `termination_by`
+termination_by p q => p + q -- Porting note: Added `termination_by`
 #align ballot.counted_sequence_finite Ballot.countedSequence_finite
 
 theorem countedSequence_nonempty : ∀ p q : ℕ, (countedSequence p q).Nonempty
@@ -211,7 +211,7 @@ theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p
       count_injective_image List.cons_injective, count_countedSequence _ _]
     · norm_cast
       rw [add_assoc, add_comm 1 q, ← Nat.choose_succ_succ, Nat.succ_eq_add_one, add_right_comm]
-termination_by _ p q => p + q -- Porting note: Added `termination_by`
+termination_by p q => p + q -- Porting note: Added `termination_by`
 #align ballot.count_counted_sequence Ballot.count_countedSequence
 
 theorem first_vote_pos :

Mathlib/Algebra/EuclideanDomain/Defs.lean

@@ -186,7 +186,7 @@ theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
   else
     have _ := mod_lt b a0
     H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
-termination_by _ => a
+termination_by => a
 #align euclidean_domain.gcd.induction EuclideanDomain.GCD.induction
 
 end
@@ -202,7 +202,7 @@ def gcd (a b : R) : R :=
   else
     have _ := mod_lt b a0
     gcd (b % a) a
-termination_by _ => a
+termination_by => a
 #align euclidean_domain.gcd EuclideanDomain.gcd
 
 @[simp]
@@ -226,7 +226,7 @@ def xgcdAux (r s t r' s' t' : R) : R × R × R :=
     let q := r' / r
     have _ := mod_lt r' _hr
     xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
-termination_by _ => r
+termination_by => r
 #align euclidean_domain.xgcd_aux EuclideanDomain.xgcdAux
 
 @[simp]

Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

@@ -53,7 +53,7 @@ local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y
 and outputs a set of orthogonal vectors which have the same span. -/
 noncomputable def gramSchmidt [IsWellOrder ι (· < ·)] (f : ι → E) (n : ι) : E :=
   f n - ∑ i : Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
-termination_by _ n => n
+termination_by n => n
 decreasing_by exact mem_Iio.1 i.2
 #align gram_schmidt gramSchmidt
 
@@ -152,7 +152,7 @@ theorem gramSchmidt_mem_span (f : ι → E) :
   let hkj : k < j := (Finset.mem_Iio.1 hk).trans_le hij
   exact smul_mem _ _
     (span_mono (image_subset f <| Iic_subset_Iic.2 hkj.le) <| gramSchmidt_mem_span _ le_rfl)
-termination_by _ => j
+termination_by => j
 decreasing_by exact hkj
 #align gram_schmidt_mem_span gramSchmidt_mem_span
 

Mathlib/Data/BinaryHeap.lean

@@ -35,7 +35,7 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
       rw [a.size_swap i j]; exact Nat.sub_lt_sub_left i.2 <| Nat.lt_of_le_of_ne j.2 h
     let ⟨a₂, h₂⟩ := heapifyDown lt a' j'
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
-termination_by _ => a.size - i
+termination_by => a.size - i
 decreasing_by assumption
 
 @[simp] theorem size_heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
@@ -69,7 +69,7 @@ if i0 : i.1 = 0 then ⟨a, rfl⟩ else
     let ⟨a₂, h₂⟩ := heapifyUp lt a' ⟨j.1, by rw [a.size_swap i j]; exact j.2⟩
     ⟨a₂, h₂.trans (a.size_swap i j)⟩
   else ⟨a, rfl⟩
-termination_by _ => i.1
+termination_by => i.1
 decreasing_by assumption
 
 @[simp] theorem size_heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
@@ -172,6 +172,6 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
       have : a.popMax.size < a.size := by
         simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
       loop a.popMax (out.push x)
+    termination_by => a.size
+    decreasing_by assumption
   loop (a.toBinaryHeap gt) #[]
-termination_by _ => a.size
-decreasing_by assumption

Mathlib/Data/ByteArray.lean

@@ -58,7 +58,7 @@ def forIn.loop [Monad m] (f : UInt8 → β → m (ForInStep β))
     | ForInStep.done b => pure b
     | ForInStep.yield b => have := Nat.Up.next h; loop f arr off _end (i+1) b
   else pure b
-termination_by _ => _end - i
+termination_by => _end - i
 
 instance : ForIn m ByteSlice UInt8 :=
   ⟨fun ⟨arr, off, len⟩ b f ↦ forIn.loop f arr off (off + len) off b⟩
@@ -83,7 +83,7 @@ def String.toAsciiByteArray (s : String) : ByteArray :=
         (Nat.lt_add_of_pos_right (String.csize_pos _))
     loop (s.next p) (out.push c.toUInt8)
   loop 0 ByteArray.empty
-termination_by _ => utf8ByteSize s - p.byteIdx
+termination_by => utf8ByteSize s - p.byteIdx
 
 /-- Convert a byte slice into a string. This does not handle non-ASCII characters correctly:
 every byte will become a unicode character with codepoint < 256. -/

Mathlib/Data/Finset/LocallyFinite.lean

@@ -1215,7 +1215,7 @@ lemma transGen_wcovby_of_le [Preorder α] [LocallyFiniteOrder α] {x y : α} (hx
       refine ⟨(mem_Ico.mp z_mem).2.le, fun c hzc hcy ↦ hz c ?_ hzc⟩
       exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩
     exact .tail h₁ h₂
-termination_by _ => (Icc x y).card
+termination_by => (Icc x y).card
 
 /-- In a locally finite preorder, `≤` is the transitive closure of `⩿`. -/
 lemma le_iff_transGen_wcovby [Preorder α] [LocallyFiniteOrder α] {x y : α} :
@@ -1253,7 +1253,7 @@ lemma transGen_covby_of_lt [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy
   `x ≤ z`), and since `z ⋖ y` we conclude that `x ⋖ y` , then `Relation.TransGen.single`. -/
   · simp only [lt_iff_le_not_le, not_and, not_not] at hxz
     exact .single (hzy.of_le_of_lt (hxz (mem_Ico.mp z_mem).1) hxy)
-termination_by _ => (Ico x y).card
+termination_by => (Ico x y).card
 
 /-- In a locally finite preorder, `<` is the transitive closure of `⋖`. -/
 lemma lt_iff_transGen_covby [Preorder α] [LocallyFiniteOrder α] {x y : α} :

Mathlib/Data/List/Basic.lean

@@ -956,7 +956,7 @@ def reverseRecOn {C : List α → Sort*} (l : List α) (H0 : C [])
     let ih := reverseRecOn (reverse tail) H0 H1
     rw [reverse_cons]
     exact H1 _ _ ih
-termination_by _ _ l _ _ => l.length
+termination_by _ l _ _ => l.length
 #align list.reverse_rec_on List.reverseRecOn
 
 /-- Bidirectional induction principle for lists: if a property holds for the empty list, the
@@ -973,7 +973,7 @@ def bidirectionalRec {C : List α → Sort*} (H0 : C []) (H1 : ∀ a : α, C [a]
     rw [← dropLast_append_getLast (cons_ne_nil b l)]
     have : C l' := bidirectionalRec H0 H1 Hn l'
     exact Hn a l' b' this
-termination_by _ l => l.length
+termination_by l => l.length
 #align list.bidirectional_rec List.bidirectionalRecₓ -- universe order
 
 /-- Like `bidirectionalRec`, but with the list parameter placed first. -/

Mathlib/Data/List/Defs.lean

@@ -227,8 +227,8 @@ def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C []
   | [], is => H0 is
   | t :: ts, is =>
       H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
-  termination_by _ ts is => (length ts + length is, length ts)
-  decreasing_by simp_wf; simp [Nat.succ_add]; decreasing_tactic
+  termination_by ts is => (length ts + length is, length ts)
+  decreasing_by all_goals (simp_wf; simp [Nat.succ_add]; decreasing_tactic)
 #align list.permutations_aux.rec List.permutationsAux.rec
 
 /-- An auxiliary function for defining `permutations`. `permutationsAux ts is` is the set of all

Mathlib/Data/List/Sym.lean

@@ -159,7 +159,7 @@ protected def sym : (n : ℕ) → List α → List (Sym α n)
   | 0, _ => [.nil]
   | _, [] => []
   | n + 1, x :: xs => ((x :: xs).sym n |>.map fun p => x ::ₛ p) ++ xs.sym (n + 1)
-  termination_by _ n xs => n + xs.length
+  termination_by n xs => n + xs.length
 
 variable {xs ys : List α} {n : ℕ}
 
@@ -187,7 +187,7 @@ theorem sym_map {β : Type*} (f : α → β) (n : ℕ) (xs : List α) :
     congr
     ext s
     simp only [Function.comp_apply, Sym.map_cons]
-  termination_by _ n xs => n + xs.length
+  termination_by n xs => n + xs.length
 
 protected theorem Sublist.sym (n : ℕ) {xs ys : List α} (h : xs <+ ys) : xs.sym n <+ ys.sym n :=
   match n, h with
@@ -202,7 +202,7 @@ protected theorem Sublist.sym (n : ℕ) {xs ys : List α} (h : xs <+ ys) : xs.sy
     apply Sublist.append
     · exact ((cons₂ a h).sym n).map _
     · exact h.sym (n + 1)
-  termination_by _ n xs ys h => n + xs.length + ys.length
+  termination_by n xs ys h => n + xs.length + ys.length
 
 theorem sym_sublist_sym_cons {a : α} : xs.sym n <+ (a :: xs).sym n :=
   (sublist_cons a xs).sym n
@@ -224,7 +224,7 @@ theorem mem_of_mem_of_mem_sym {n : ℕ} {xs : List α} {a : α} {z : Sym α n}
     · rw [mem_cons]
       right
       exact mem_of_mem_of_mem_sym ha hz
-  termination_by _ n xs _ _ _ _ => n + xs.length
+  termination_by n xs _ _ _ _ => n + xs.length
 
 theorem first_mem_of_cons_mem_sym {xs : List α} {n : ℕ} {a : α} {z : Sym α n}
     (h : a ::ₛ z ∈ xs.sym (n + 1)) : a ∈ xs :=
@@ -246,7 +246,7 @@ protected theorem Nodup.sym (n : ℕ) {xs : List α} (h : xs.Nodup) : (xs.sym n)
       obtain ⟨z, _hz, rfl⟩ := hz
       have := first_mem_of_cons_mem_sym hz'
       simp only [nodup_cons, this, not_true_eq_false, false_and] at h
-  termination_by _ n xs _ => n + xs.length
+  termination_by n xs _ => n + xs.length
 
 theorem length_sym {n : ℕ} {xs : List α} :
     (xs.sym n).length = Nat.multichoose xs.length n :=
@@ -257,7 +257,7 @@ theorem length_sym {n : ℕ} {xs : List α} :
     rw [List.sym, length_append, length_map, length_cons]
     rw [@length_sym n (x :: xs), @length_sym (n + 1) xs]
     rw [Nat.multichoose_succ_succ, length_cons, add_comm]
-  termination_by _ n xs => n + xs.length
+  termination_by n xs => n + xs.length
 
 end Sym
 

Mathlib/Data/Matroid/Basic.lean

@@ -270,7 +270,7 @@ theorem encard_diff_le_aux (exch : ExchangeProperty Base) (hB₁ : Base B₁) (h
 
   rw [← encard_diff_singleton_add_one he, ← encard_diff_singleton_add_one hf]
   exact add_le_add_right hencard 1
-termination_by _ => (B₂ \ B₁).encard
+termination_by => (B₂ \ B₁).encard
 
 /-- For any two sets `B₁`, `B₂` in a family with the exchange property, the differences `B₁ \ B₂`
 and `B₂ \ B₁` have the same `ℕ∞`-cardinality. -/

Mathlib/Data/Multiset/Basic.lean

@@ -850,7 +850,7 @@ def strongInductionOn {p : Multiset α → Sort*} (s : Multiset α) (ih : ∀ s,
     p s :=
     (ih s) fun t _h =>
       strongInductionOn t ih
-termination_by _ => card s
+termination_by => card s
 decreasing_by exact card_lt_of_lt _h
 #align multiset.strong_induction_on Multiset.strongInductionOnₓ -- Porting note: reorderd universes
 
@@ -877,7 +877,7 @@ def strongDownwardInduction {p : Multiset α → Sort*} {n : ℕ}
     card s ≤ n → p s :=
   H s fun {t} ht _h =>
     strongDownwardInduction H t ht
-termination_by _ => n - card s
+termination_by => n - card s
 decreasing_by exact (tsub_lt_tsub_iff_left_of_le ht).2 (card_lt_of_lt _h)
 -- Porting note: reorderd universes
 #align multiset.strong_downward_induction Multiset.strongDownwardInductionₓ

Mathlib/Data/Nat/Cast/Defs.lean

@@ -159,7 +159,7 @@ protected def binCast [Zero R] [One R] [Add R] : ℕ → R
   | n + 1 => if (n + 1) % 2 = 0
     then (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2))
     else (Nat.binCast ((n + 1) / 2)) + (Nat.binCast ((n + 1) / 2)) + 1
-decreasing_by (exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2))
+decreasing_by all_goals exact Nat.div_lt_self (Nat.succ_pos n) (Nat.le_refl 2)
 #align nat.bin_cast Nat.binCast
 
 @[simp]

Mathlib/Data/Nat/Choose/Basic.lean

@@ -362,7 +362,7 @@ def multichoose : ℕ → ℕ → ℕ
   | 0, _ + 1 => 0
   | n + 1, k + 1 =>
     multichoose n (k + 1) + multichoose (n + 1) k
-  termination_by multichoose a b => (a, b)
+  termination_by a b => (a, b)
 #align nat.multichoose Nat.multichoose
 
 @[simp]
@@ -405,8 +405,8 @@ theorem multichoose_eq : ∀ n k : ℕ, multichoose n k = (n + k - 1).choose k
     have : (n + 1) + k < (n + 1) + (k + 1) := add_lt_add_left (Nat.lt_succ_self _) _
     erw [multichoose_succ_succ, add_comm, Nat.succ_add_sub_one, ← add_assoc, Nat.choose_succ_succ]
     simp [multichoose_eq n (k+1), multichoose_eq (n+1) k]
-  termination_by multichoose_eq a b => a + b
-  decreasing_by { assumption }
+  termination_by a b => a + b
+  decreasing_by all_goals assumption
 #align nat.multichoose_eq Nat.multichoose_eq
 
 end Nat

Mathlib/Data/Nat/Hyperoperation.lean

@@ -39,7 +39,7 @@ def hyperoperation : ℕ → ℕ → ℕ → ℕ
   | 2, _, 0 => 0
   | _ + 3, _, 0 => 1
   | n + 1, m, k + 1 => hyperoperation n m (hyperoperation (n + 1) m k)
-  termination_by hyperoperation a b c => (a, b, c)
+  termination_by a b c => (a, b, c)
 #align hyperoperation hyperoperation
 
 -- Basic hyperoperation lemmas

Mathlib/Data/Nat/Order/Basic.lean

@@ -350,8 +350,8 @@ theorem diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ a, P (a + 1) (a + 1)
     have _ : a + (b + 1) < (a + 1) + (b + 1) := by simp
     apply diag_induction P ha hb hd a (b + 1)
     apply lt_of_le_of_lt (Nat.le_succ _) h
-  termination_by _ a b c => a + b
-  decreasing_by { assumption }
+  termination_by a b c => a + b
+  decreasing_by all_goals assumption
 #align nat.diag_induction Nat.diag_induction
 
 /-- A subset of `ℕ` containing `k : ℕ` and closed under `Nat.succ` contains every `n ≥ k`. -/

Mathlib/Data/Nat/Prime.lean

@@ -255,7 +255,7 @@ def minFacAux (n : ℕ) : ℕ → ℕ
       else
         have := minFac_lemma n k h
         minFacAux n (k + 2)
-termination_by _ n k => sqrt n + 2 - k
+termination_by n k => sqrt n + 2 - k
 #align nat.min_fac_aux Nat.minFacAux
 
 /-- Returns the smallest prime factor of `n ≠ 1`. -/
@@ -306,7 +306,7 @@ theorem minFacAux_has_prop {n : ℕ} (n2 : 2 ≤ n) :
       have := a _ le_rfl (dvd_of_mul_right_dvd d')
       rw [e] at this
       exact absurd this (by contradiction)
-  termination_by _ n _ k => sqrt n + 2 - k
+  termination_by n _ k => sqrt n + 2 - k
 #align nat.min_fac_aux_has_prop Nat.minFacAux_has_prop
 
 theorem minFac_has_prop {n : ℕ} (n1 : n ≠ 1) : minFacProp n (minFac n) := by

Mathlib/Data/Nat/Squarefree.lean

@@ -127,7 +127,7 @@ def minSqFacAux : ℕ → ℕ → Option ℕ
         lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt <| Nat.div_le_self _ _) k) this
         if k ∣ n' then some k else minSqFacAux n' (k + 2)
       else minSqFacAux n (k + 2)
-termination_by _ n k => sqrt n + 2 - k
+termination_by n k => sqrt n + 2 - k
 #align nat.min_sq_fac_aux Nat.minSqFacAux
 
 /-- Returns the smallest prime factor `p` of `n` such that `p^2 ∣ n`, or `none` if there is no
@@ -202,7 +202,7 @@ theorem minSqFacAux_has_prop {n : ℕ} (k) (n0 : 0 < n) (i) (e : k = 2 * i + 3)
   · specialize IH (n / k) (div_dvd_of_dvd dk) dkk
     exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff dk).2 dkk) IH
   · exact IH n (dvd_refl _) dk
-termination_by _ => n.sqrt + 2 - k
+termination_by => n.sqrt + 2 - k
 #align nat.min_sq_fac_aux_has_prop Nat.minSqFacAux_has_prop
 
 theorem minSqFac_has_prop (n : ℕ) : MinSqFacProp n (minSqFac n) := by

Mathlib/Data/PNat/Defs.lean

@@ -207,7 +207,7 @@ instance : WellFoundedRelation ℕ+ :=
 /-- Strong induction on `ℕ+`. -/
 def strongInductionOn {p : ℕ+ → Sort*} (n : ℕ+) : (∀ k, (∀ m, m < k → p m) → p k) → p n
   | IH => IH _ fun a _ => strongInductionOn a IH
-termination_by _ => n.1
+termination_by => n.1
 #align pnat.strong_induction_on PNat.strongInductionOn
 
 /-- We define `m % k` and `m / k` in the same way as for `ℕ`

Mathlib/Data/Polynomial/Inductions.lean

@@ -163,7 +163,7 @@ noncomputable def recOnHorner {M : R[X] → Sort*} (p : R[X]) (M0 : M 0)
         MC _ _ (coeff_mul_X_zero _) hcp0
           (if hpX0 : divX p = 0 then show M (divX p * X) by rw [hpX0, zero_mul]; exact M0
           else MX (divX p) hpX0 (recOnHorner _ M0 MC MX))
-termination_by _ => p.degree
+termination_by => p.degree
 #align polynomial.rec_on_horner Polynomial.recOnHorner
 
 /-- A property holds for all polynomials of positive `degree` with coefficients in a semiring `R`

Mathlib/Data/Polynomial/RingDivision.lean

@@ -527,7 +527,7 @@ theorem exists_multiset_roots [DecidableEq R] :
       ⟨0, (degree_eq_natDegree hp).symm ▸ WithBot.coe_le_coe.2 (Nat.zero_le _), by
         intro a
         rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]⟩
-termination_by _ p _ => natDegree p
+termination_by p _ => natDegree p
 decreasing_by {
   simp_wf
   apply (Nat.cast_lt (α := WithBot ℕ)).mp

Mathlib/Data/Set/Card.lean

@@ -437,7 +437,7 @@ theorem Finite.exists_injOn_of_encard_le [Nonempty β] {s : Set α} {t : Set β}
   refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
   · rintro x hx; split_ifs with h; assumption; exact (hf₀s x hx h).1
   exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_noteq])
-termination_by _ => encard s
+termination_by => encard s
 
 theorem Finite.exists_bijOn_of_encard_eq [Nonempty β] (hs : s.Finite) (h : s.encard = t.encard) :
     ∃ (f : α → β), BijOn f s t := by

Mathlib/Data/UnionFind.lean

@@ -241,7 +241,7 @@ def findAux (self : UnionFind α) (x : Fin self.size) :
       ⟨root.2, ?_⟩, le_of_lt this⟩
     have : x.1 ≠ root := mt (congrArg _) (ne_of_lt this); dsimp only at this
     simp [UFModel.setParent, this, hr]
-termination_by _ α self x => self.rankMax - self.rank x
+termination_by α self x => self.rankMax - self.rank x
 
 def find (self : UnionFind α) (x : Fin self.size) :
     (s : UnionFind α) × (root : Fin s.size) ×'

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -544,7 +544,7 @@ theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ f.support
           card_support_swap_mul hx.1
         rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
         simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]
-termination_by _ => f.support.card
+termination_by => f.support.card
 #align equiv.perm.is_cycle.sign Equiv.Perm.IsCycle.sign
 
 theorem IsCycle.of_pow {n : ℕ} (h1 : IsCycle (f ^ n)) (h2 : f.support ⊆ (f ^ n).support) :

Mathlib/Order/RelClasses.lean

@@ -289,7 +289,7 @@ instance WellFoundedRelation.isWellFounded [h : WellFoundedRelation α] :
 theorem WellFoundedRelation.asymmetric {α : Sort*} [WellFoundedRelation α] {a b : α} :
     WellFoundedRelation.rel a b → ¬ WellFoundedRelation.rel b a :=
   fun hab hba => WellFoundedRelation.asymmetric hba hab
-termination_by _ => a
+termination_by => a
 
 lemma WellFounded.prod_lex {ra : α → α → Prop} {rb : β → β → Prop} (ha : WellFounded ra)
     (hb : WellFounded rb) : WellFounded (Prod.Lex ra rb) :=

Mathlib/RingTheory/Polynomial/Hermite/Basic.lean

@@ -199,7 +199,7 @@ theorem coeff_hermite_explicit :
     · rw [coeff_hermite_explicit (n + 1) k]
     · rw [(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)), coeff_hermite_explicit n (k + 2)]
 -- porting note: Lean 3 worked this out automatically
-termination_by _ n k => (n, k)
+termination_by n k => (n, k)
 #align polynomial.coeff_hermite_explicit Polynomial.coeff_hermite_explicit
 
 theorem coeff_hermite_of_even_add {n k : ℕ} (hnk : Even (n + k)) :