Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Co-authored-by: Michael Stoll <[email protected]>
leanprover-community · Dec 3, 2024 · 4a31859 · 4a31859
1 parent 9b47052
commit 4a31859
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean
@@ -227,7 +227,7 @@ theorem mulSupport_Finite {x : K} (h_x_nezero : x ≠ 0) :
     map_div₀]
   obtain ⟨ha, hb⟩ := h_x_nezero
   simp_rw [← RingOfIntegers.coe_eq_algebraMap]
-  apply Set.Finite.subset (Set.Finite.union (mulSupport_Finite_int ha) (mulSupport_Finite_int hb))
+  apply ((mulSupport_Finite_int ha).union (mulSupport_Finite_int hb)).subset
   intro w
   contrapose!
   intro a_1