From 57fce93dad82c9de4141e9b7b9e2ea51ccb4d0af Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>
Date: Fri, 20 Sep 2024 11:06:25 +0200
Subject: [PATCH] add classical

---
 Mathlib/RingTheory/MvPowerSeries/PiTopology.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean b/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
index 51efabb7429b9..9475a3ac08ca5 100644
--- a/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
+++ b/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
@@ -134,6 +134,7 @@ theorem continuous_C [Ring R] [TopologicalRing R] :
 
 theorem variables_tendsto_zero [Semiring R] :
     Filter.Tendsto (X · : σ → MvPowerSeries σ R) Filter.cofinite (nhds 0) := by
+  classical
   rw [tendsto_pi_nhds]
   simp_rw [apply_eq_coeff]
   intro d s hs