From 4a31859e2ea46127a8d7f01b1c7a61004b2c1f7e Mon Sep 17 00:00:00 2001 From: Fabrizio Barroero Date: Tue, 3 Dec 2024 22:39:44 +0100 Subject: [PATCH] Update Mathlib/NumberTheory/NumberField/FinitePlaces.lean Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com> --- Mathlib/NumberTheory/NumberField/FinitePlaces.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/NumberTheory/NumberField/FinitePlaces.lean b/Mathlib/NumberTheory/NumberField/FinitePlaces.lean index c618f4243d20d..b28df607336b4 100644 --- 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