diff --git a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean
index 4e89ebc36f7509..22abdd2f5ebe9a 100644
--- a/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean
+++ b/Mathlib/LinearAlgebra/ExteriorPower/Basis.lean
@@ -7,7 +7,6 @@ module
 
 public import Mathlib.LinearAlgebra.ExteriorPower.Basic
 public import Mathlib.LinearAlgebra.ExteriorPower.Pairing
-public import Mathlib.Order.Extension.Well
 public import Mathlib.RingTheory.Finiteness.Subalgebra
 public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
@@ -149,10 +148,11 @@ lemma basis_repr {I : Type*} [LinearOrder I] (b : Basis I R M) (s : powersetCard
 /-! ### Freeness and dimension of `⋀[R]^n M`. -/
 
 /-- If `M` is a free module, then so is its `n`th exterior power. -/
-instance instFree [Module.Free R M] : Module.Free R (⋀[R]^n M) :=
+instance instFree [Module.Free R M] : Module.Free R (⋀[R]^n M) := by
+  classical
   have ⟨I, b⟩ := Module.Free.exists_basis R M
-  letI : LinearOrder I := IsWellFounded.wellOrderExtension emptyWf.rel
-  Module.Free.of_basis (b.exteriorPower n)
+  letI : LinearOrder I := linearOrderOfSTO WellOrderingRel
+  exact Module.Free.of_basis (b.exteriorPower n)
 
 variable [Nontrivial R]
 
@@ -160,8 +160,8 @@ variable [Nontrivial R]
 the `n`th exterior power of `M` is of finrank `Nat.choose r n`. -/
 lemma finrank_eq [Module.Free R M] [Module.Finite R M] :
     Module.finrank R (⋀[R]^n M) = Nat.choose (Module.finrank R M) n := by
-  letI : LinearOrder (Module.Free.ChooseBasisIndex R M) :=
-    IsWellFounded.wellOrderExtension emptyWf.rel
+  classical
+  let : LinearOrder (Module.Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
   let B := (Module.Free.chooseBasis R M).exteriorPower n
   rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
     Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]