chore(ring_theory/hahn_series): golf a proof (#14054)

leanprover-community · May 10, 2022 · 87069e9 · 87069e9
1 parent c5e0299
commit 87069e9
Showing 1 changed file with 2 additions and 4 deletions.
diff --git 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,