From f89f2af80506ee6bbfd3705aebcecb85ec0f4d61 Mon Sep 17 00:00:00 2001 From: Geno Racklin Asher Date: Wed, 21 Jun 2023 12:55:40 +0100 Subject: [PATCH] chore: Fix norm_lt --- Mathlib/NumberTheory/ClassNumber/Finite.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean index e63847208d0f93..c3d36189f14c99 100644 --- a/Mathlib/NumberTheory/ClassNumber/Finite.lean +++ b/Mathlib/NumberTheory/ClassNumber/Finite.lean @@ -114,10 +114,10 @@ theorem norm_lt {T : Type _} [LinearOrderedRing T] (a : S) {y : T} set y' : ℤ := Finset.max' _ him with y'_def have hy' : ∀ k, abv (bS.repr a k) ≤ y' := by intro k - exact Finset.le_max' _ _ (Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩) + exact @Finset.le_max' ℤ _ _ _ (Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩) have : (y' : T) < y := by rw [y'_def, ← - Finset.max'_image (show Monotone (coe : ℤ → T) from fun x y h => Int.cast_le.mpr h)] + Finset.max'_image (show Monotone (_ : ℤ → T) from fun x y h => Int.cast_le.mpr h)] apply (Finset.max'_lt_iff _ (him.image _)).mpr simp only [Finset.mem_image, exists_prop] rintro _ ⟨x, ⟨k, -, rfl⟩, rfl⟩