From 87069e9134f1da4fef5cee07f8e8d676840e0ec0 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 10 May 2022 05:20:26 +0000
Subject: [PATCH] chore(ring_theory/hahn_series): golf a proof (#14054)

---
 src/ring_theory/hahn_series.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/ring_theory/hahn_series.lean b/src/ring_theory/hahn_series.lean
index 520598c492588..12ff6706e3b27 100644
--- a/src/ring_theory/hahn_series.lean
+++ b/src/ring_theory/hahn_series.lean
@@ -1472,10 +1472,8 @@ def of_finsupp (f : α →₀ (hahn_series Γ R)) :
       intros g hg,
       obtain ⟨a, ha⟩ := set.mem_Union.1 hg,
       have haf : a ∈ f.support,
-      { rw finsupp.mem_support_iff,
-        contrapose! ha,
-        rw [ha, support_zero],
-        exact set.not_mem_empty _ },
+      { rw [finsupp.mem_support_iff, ← support_nonempty_iff],
+        exact ⟨g, ha⟩ },
       have h : (λ i, (f i).support) a ≤ _ := le_sup haf,
       exact h ha,
     end,