diff --git a/Mathlib.lean b/Mathlib.lean
index 9e76ea4fd233b..d0dfe0535c1e1 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1258,6 +1258,7 @@ import Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
 import Mathlib.Analysis.LocallyConvex.Polar
 import Mathlib.Analysis.LocallyConvex.StrongTopology
 import Mathlib.Analysis.LocallyConvex.WeakDual
+import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 import Mathlib.Analysis.LocallyConvex.WeakSpace
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
 import Mathlib.Analysis.Matrix
@@ -1332,7 +1333,6 @@ import Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
 import Mathlib.Analysis.Normed.Operator.Compact
 import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
 import Mathlib.Analysis.Normed.Operator.LinearIsometry
-import Mathlib.Analysis.Normed.Operator.WeakOperatorTopology
 import Mathlib.Analysis.Normed.Order.Basic
 import Mathlib.Analysis.Normed.Order.Lattice
 import Mathlib.Analysis.Normed.Order.UpperLower
diff --git a/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean b/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
index 52173af64e2c0..29ec80a409d57 100644
--- a/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
+++ b/Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean
@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis
 -/
 
 import Mathlib.Analysis.InnerProductSpace.Dual
-import Mathlib.Analysis.Normed.Operator.WeakOperatorTopology
+import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 
 /-!
 # The weak operator topology in Hilbert spaces
@@ -33,14 +33,9 @@ open Filter in
 lemma tendsto_iff_forall_inner_apply_tendsto [CompleteSpace F] {α : Type*} {l : Filter α}
     {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F} :
     Tendsto f l (𝓝 A) ↔ ∀ x y, Tendsto (fun a => ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜) := by
-  simp only [← InnerProductSpace.toDual_apply]
-  refine ⟨fun h x y => ?_, fun h => ?_⟩
-  · exact (tendsto_iff_forall_dual_apply_tendsto.mp h) _ _
-  · have h' : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F),
-        Tendsto (fun a => y (f a x)) l (𝓝 (y (A x))) := by
-      intro x y
-      convert h x ((InnerProductSpace.toDual 𝕜 F).symm y) <;> simp
-    exact tendsto_iff_forall_dual_apply_tendsto.mpr h'
+  simp_rw [tendsto_iff_forall_dual_apply_tendsto, ← InnerProductSpace.toDual_apply]
+  exact .symm <| forall_congr' fun _ ↦
+    Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl
 
 lemma le_nhds_iff_forall_inner_apply_le_nhds [CompleteSpace F] {l : Filter (E →WOT[𝕜] F)}
     {A : E →WOT[𝕜] F} : l ≤ 𝓝 A ↔ ∀ x y, l.map (fun T => ⟪y, T x⟫_𝕜) ≤ 𝓝 (⟪y, A x⟫_𝕜) :=
diff --git a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean b/Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
similarity index 68%
rename from Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean
rename to Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
index 52bae3c5d3cee..6f8c84c347d69 100644
--- a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@@ -5,22 +5,23 @@ Authors: Frédéric Dupuis
 -/
 
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
-import Mathlib.Analysis.Normed.Module.Dual
+import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
 
 /-!
 # The weak operator topology
 
-This file defines a type copy of `E →L[𝕜] F` (where `F` is a normed space) which is
-endowed with the weak operator topology (WOT) rather than the topology induced by the operator norm.
+This file defines a type copy of `E →L[𝕜] F` (where `E` and `F` are topological vector spaces)
+which is endowed with the weak operator topology (WOT) rather than the topology of bounded
+convergence (which is the usual one induced by the operator norm in the normed setting).
 The WOT is defined as the coarsest topology such that the functional `fun A => y (A x)` is
-continuous for any `x : E` and `y : NormedSpace.Dual 𝕜 F`. Equivalently, a function `f` tends to
+continuous for any `x : E` and `y : F →L[𝕜] 𝕜`. Equivalently, a function `f` tends to
 `A : E →WOT[𝕜] F` along filter `l` iff `y (f a x)` tends to `y (A x)` along the same filter.
 
 Basic non-topological properties of `E →L[𝕜] F` (such as the module structure) are copied over to
 the type copy.
 
 We also prove that the WOT is induced by the family of seminorms `‖y (A x)‖` for `x : E` and
-`y : NormedSpace.Dual 𝕜 F`.
+`y : F →L[𝕜] 𝕜`.
 
 ## Main declarations
 
@@ -32,19 +33,18 @@ We also prove that the WOT is induced by the family of seminorms `‖y (A x)‖`
 * `ContinuousLinearMap.continuous_toWOT`: the inclusion map is continuous, i.e. the WOT is coarser
   than the norm topology.
 * `ContinuousLinearMapWOT.withSeminorms`: the WOT is induced by the family of seminorms
-  `‖y (A x)‖` for `x : E` and `y : NormedSpace.Dual 𝕜 F`.
+  `‖y (A x)‖` for `x : E` and `y : F →L[𝕜] 𝕜`.
 
 ## Notation
 
 * The type copy of `E →L[𝕜] F` endowed with the weak operator topology is denoted by
   `E →WOT[𝕜] F`.
-* We locally use the notation `F⋆` for `NormedSpace.Dual 𝕜 F`.
+* We locally use the notation `F⋆` for `F →L[𝕜] 𝕜`.
 
 ## Implementation notes
 
-In the literature, the WOT is only defined on maps between Banach spaces. Here, we generalize this
-a bit to `E →L[𝕜] F` where `F` is an normed space, and `E` actually only needs to be a vector
-space with some topology for most results in this file.
+In most of the literature, the WOT is defined on maps between Banach spaces. Here, we only assume
+that the domain and codomains are topological vector spaces over a normed field.
 -/
 
 open scoped Topology
@@ -57,14 +57,15 @@ def ContinuousLinearMapWOT (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 𝕜
   E →L[𝕜] F
 
 @[inherit_doc]
-notation:25 E " →WOT[" 𝕜 "]" F => ContinuousLinearMapWOT 𝕜 E F
+notation:25 E " →WOT[" 𝕜 "] " F => ContinuousLinearMapWOT 𝕜 E F
 
 namespace ContinuousLinearMapWOT
 
-variable {𝕜 : Type*} {E : Type*} {F : Type*} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E]
-  [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {𝕜 : Type*} {E : Type*} {F : Type*} [NormedField 𝕜]
+  [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E]
+  [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F]
 
-local postfix:max "⋆" => NormedSpace.Dual 𝕜
+local notation X "⋆" => X →L[𝕜] 𝕜
 
 /-!
 ### Basic properties common with `E →L[𝕜] F`
@@ -74,19 +75,38 @@ the module structure, `FunLike`, etc.
 -/
 section Basic
 
+/-
+Warning : Due to the irreducibility of `ContinuousLinearMapWOT`, one has to be careful when
+declaring instances with data. For example, adding
+```
+unseal ContinuousLinearMapWOT in
+instance instAddCommMonoid [ContinuousAdd F] : AddCommMonoid (E →WOT[𝕜] F) :=
+  inferInstanceAs <| AddCommMonoid (E →L[𝕜] F)
+```
+would cause the following to fail :
+```
+example [TopologicalAddGroup F] :
+  (instAddCommMonoid : AddCommMonoid (E →WOT[𝕜] F)) =
+    instAddCommGroup.toAddCommMonoid := rfl
+```
+-/
+
 unseal ContinuousLinearMapWOT in
-instance instAddCommGroup : AddCommGroup (E →WOT[𝕜] F) :=
+instance instAddCommGroup [TopologicalAddGroup F] : AddCommGroup (E →WOT[𝕜] F) :=
   inferInstanceAs <| AddCommGroup (E →L[𝕜] F)
 
 unseal ContinuousLinearMapWOT in
-instance instModule : Module 𝕜 (E →WOT[𝕜] F) := inferInstanceAs <| Module 𝕜 (E →L[𝕜] F)
+instance instModule [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : Module 𝕜 (E →WOT[𝕜] F) :=
+  inferInstanceAs <| Module 𝕜 (E →L[𝕜] F)
 
-variable (𝕜) (E) (F)
+variable (𝕜) (E) (F) [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
 
 unseal ContinuousLinearMapWOT in
 /-- The linear equivalence that sends a continuous linear map to the type copy endowed with the
 weak operator topology. -/
-def _root_.ContinuousLinearMap.toWOT : (E →L[𝕜] F) ≃ₗ[𝕜] (E →WOT[𝕜] F) := LinearEquiv.refl 𝕜 _
+def _root_.ContinuousLinearMap.toWOT :
+    (E →L[𝕜] F) ≃ₗ[𝕜] (E →WOT[𝕜] F) :=
+  LinearEquiv.refl 𝕜 _
 
 variable {𝕜} {E} {F}
 
@@ -112,11 +132,10 @@ lemma ext_iff {A B : E →WOT[𝕜] F} : A = B ↔ ∀ x, A x = B x := Continuou
 -- version with an inner product (`ContinuousLinearMapWOT.ext_inner`) takes precedence
 -- in the case of Hilbert spaces.
 @[ext 900]
-lemma ext_dual {A B : E →WOT[𝕜] F} (h : ∀ x (y : F⋆), y (A x) = y (B x)) : A = B := by
-  rw [ext_iff]
-  intro x
-  specialize h x
-  rwa [← NormedSpace.eq_iff_forall_dual_eq 𝕜] at h
+lemma ext_dual [H : SeparatingDual 𝕜 F] {A B : E →WOT[𝕜] F}
+    (h : ∀ x (y : F⋆), y (A x) = y (B x)) : A = B := by
+  simp_rw [ext_iff, ← (separatingDual_iff_injective.mp H).eq_iff, LinearMap.ext_iff]
+  exact h
 
 @[simp] lemma zero_apply (x : E) : (0 : E →WOT[𝕜] F) x = 0 := by simp only [DFunLike.coe]; rfl
 
@@ -146,6 +165,8 @@ of this topology. In particular, we show that it is a topological vector space.
 -/
 section Topology
 
+variable [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
+
 variable (𝕜) (E) (F) in
 /-- The function that induces the topology on `E →WOT[𝕜] F`, namely the function that takes
 an `A` and maps it to `fun ⟨x, y⟩ => y (A x)` in `E × F⋆ → 𝕜`, bundled as a linear map to make
@@ -155,6 +176,11 @@ def inducingFn : (E →WOT[𝕜] F) →ₗ[𝕜] (E × F⋆ → 𝕜) where
   map_add' := fun x y => by ext; simp
   map_smul' := fun x y => by ext; simp
 
+@[simp]
+lemma inducingFn_apply {f : E →WOT[𝕜] F} {x : E} {y : F⋆} :
+    inducingFn 𝕜 E F f (x, y) = y (f x) :=
+  rfl
+
 /-- The weak operator topology is the coarsest topology such that `fun A => y (A x)` is
 continuous for all `x, y`. -/
 instance instTopologicalSpace : TopologicalSpace (E →WOT[𝕜] F) :=
@@ -172,7 +198,9 @@ lemma continuous_of_dual_apply_continuous {α : Type*} [TopologicalSpace α] {g
     (h : ∀ x (y : F⋆), Continuous fun a => y (g a x)) : Continuous g :=
   continuous_induced_rng.2 (continuous_pi_iff.mpr fun p => h p.1 p.2)
 
-lemma isEmbedding_inducingFn : IsEmbedding (inducingFn 𝕜 E F) := by
+lemma isInducing_inducingFn : IsInducing (inducingFn 𝕜 E F) := ⟨rfl⟩
+
+lemma isEmbedding_inducingFn [SeparatingDual 𝕜 F] : IsEmbedding (inducingFn 𝕜 E F) := by
   refine Function.Injective.isEmbedding_induced fun A B hAB => ?_
   rw [ContinuousLinearMapWOT.ext_dual_iff]
   simpa [funext_iff] using hAB
@@ -186,17 +214,13 @@ open Filter in
 lemma tendsto_iff_forall_dual_apply_tendsto {α : Type*} {l : Filter α} {f : α → E →WOT[𝕜] F}
     {A : E →WOT[𝕜] F} :
     Tendsto f l (𝓝 A) ↔ ∀ x (y : F⋆), Tendsto (fun a => y (f a x)) l (𝓝 (y (A x))) := by
-  have hmain : (∀ x (y : F⋆), Tendsto (fun a => y (f a x)) l (𝓝 (y (A x))))
-      ↔ ∀ (p : E × F⋆), Tendsto (fun a => p.2 (f a p.1)) l (𝓝 (p.2 (A p.1))) :=
-    ⟨fun h p => h p.1 p.2, fun h x y => h ⟨x, y⟩⟩
-  rw [hmain, ← tendsto_pi_nhds, isEmbedding_inducingFn.tendsto_nhds_iff]
-  rfl
+  simp [isInducing_inducingFn.tendsto_nhds_iff, tendsto_pi_nhds]
 
 lemma le_nhds_iff_forall_dual_apply_le_nhds {l : Filter (E →WOT[𝕜] F)} {A : E →WOT[𝕜] F} :
     l ≤ 𝓝 A ↔ ∀ x (y : F⋆), l.map (fun T => y (T x)) ≤ 𝓝 (y (A x)) :=
   tendsto_iff_forall_dual_apply_tendsto (f := id)
 
-instance instT3Space : T3Space (E →WOT[𝕜] F) := isEmbedding_inducingFn.t3Space
+instance instT3Space [SeparatingDual 𝕜 F] : T3Space (E →WOT[𝕜] F) := isEmbedding_inducingFn.t3Space
 
 instance instContinuousAdd : ContinuousAdd (E →WOT[𝕜] F) := .induced (inducingFn 𝕜 E F)
 instance instContinuousNeg : ContinuousNeg (E →WOT[𝕜] F) := .induced (inducingFn 𝕜 E F)
@@ -213,6 +237,8 @@ end Topology
 /-! ### The WOT is induced by a family of seminorms -/
 section Seminorms
 
+variable [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F]
+
 /-- The family of seminorms that induce the weak operator topology, namely `‖y (A x)‖` for
 all `x` and `y`. -/
 def seminorm (x : E) (y : F⋆) : Seminorm 𝕜 (E →WOT[𝕜] F) where
@@ -228,56 +254,38 @@ all `x` and `y`. -/
 def seminormFamily : SeminormFamily 𝕜 (E →WOT[𝕜] F) (E × F⋆) :=
   fun ⟨x, y⟩ => seminorm x y
 
-lemma hasBasis_seminorms : (𝓝 (0 : E →WOT[𝕜] F)).HasBasis (seminormFamily 𝕜 E F).basisSets id := by
-  let p := seminormFamily 𝕜 E F
-  rw [nhds_induced, nhds_pi]
-  simp only [map_zero, Pi.zero_apply]
-  have h := Filter.hasBasis_pi (fun _ : (E × F⋆) ↦ Metric.nhds_basis_ball (x := 0)) |>.comap
-    (inducingFn 𝕜 E F)
-  refine h.to_hasBasis' ?_ ?_
-  · rintro ⟨s, U₂⟩ ⟨hs, hU₂⟩
-    lift s to Finset (E × F⋆) using hs
-    by_cases hU₃ : s.Nonempty
-    · refine ⟨(s.sup p).ball 0 <| s.inf' hU₃ U₂, p.basisSets_mem _ <| (Finset.lt_inf'_iff _).2 hU₂,
-        fun x hx y hy => ?_⟩
-      simp only [Set.mem_preimage, Set.mem_pi, mem_ball_zero_iff]
-      rw [id, Seminorm.mem_ball_zero] at hx
-      have hp : p y ≤ s.sup p := Finset.le_sup hy
-      refine lt_of_le_of_lt (hp x) (lt_of_lt_of_le hx ?_)
-      exact Finset.inf'_le _ hy
-    · rw [Finset.not_nonempty_iff_eq_empty.mp hU₃]
-      exact ⟨(p 0).ball 0 1, p.basisSets_singleton_mem 0 one_pos, by simp⟩
-  · suffices ∀ U ∈ p.basisSets, U ∈ 𝓝 (0 : E →WOT[𝕜] F) by simpa [nhds_induced, nhds_pi]
-    exact p.basisSets_mem_nhds fun ⟨x, y⟩ ↦ continuous_dual_apply x y |>.norm
-
 lemma withSeminorms : WithSeminorms (seminormFamily 𝕜 E F) :=
-  SeminormFamily.withSeminorms_of_hasBasis _ hasBasis_seminorms
+  let e : E × F⋆ ≃ (Σ _ : E × F⋆, Fin 1) := .symm <| .sigmaUnique _ _
+  have : Nonempty (Σ _ : E × F⋆, Fin 1) := e.symm.nonempty
+  isInducing_inducingFn.withSeminorms <| withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜 𝕜)
+    |>.congr_equiv e
+
+lemma hasBasis_seminorms : (𝓝 (0 : E →WOT[𝕜] F)).HasBasis (seminormFamily 𝕜 E F).basisSets id :=
+  withSeminorms.hasBasis
 
-instance instLocallyConvexSpace [Module ℝ (E →WOT[𝕜] F)] [IsScalarTower ℝ 𝕜 (E →WOT[𝕜] F)] :
+instance instLocallyConvexSpace [NormedSpace ℝ 𝕜] [Module ℝ (E →WOT[𝕜] F)]
+    [IsScalarTower ℝ 𝕜 (E →WOT[𝕜] F)] :
     LocallyConvexSpace ℝ (E →WOT[𝕜] F) :=
   withSeminorms.toLocallyConvexSpace
 
 end Seminorms
 
-end ContinuousLinearMapWOT
-
-section NormedSpace
+section toWOT_continuous
 
-variable {𝕜 : Type*} {E : Type*} {F : Type*} [RCLike 𝕜] [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [ContinuousSMul 𝕜 E]
 
-/-- The weak operator topology is coarser than the norm topology, i.e. the inclusion map is
-continuous. -/
+/-- The weak operator topology is coarser than the bounded convergence topology, i.e. the inclusion
+map is continuous. -/
 @[continuity, fun_prop]
 lemma ContinuousLinearMap.continuous_toWOT :
-    Continuous (ContinuousLinearMap.toWOT 𝕜 E F) := by
-  refine ContinuousLinearMapWOT.continuous_of_dual_apply_continuous fun x y => ?_
-  simp_rw [ContinuousLinearMap.toWOT_apply]
-  change Continuous fun a => y <| (ContinuousLinearMap.id 𝕜 (E →L[𝕜] F)).flip x a
-  fun_prop
+    Continuous (ContinuousLinearMap.toWOT 𝕜 E F) :=
+  ContinuousLinearMapWOT.continuous_of_dual_apply_continuous fun x y ↦
+    y.cont.comp <| continuous_eval_const x
 
 /-- The inclusion map from `E →[𝕜] F` to `E →WOT[𝕜] F`, bundled as a continuous linear map. -/
 def ContinuousLinearMap.toWOTCLM : (E →L[𝕜] F) →L[𝕜] (E →WOT[𝕜] F) :=
   ⟨LinearEquiv.toLinearMap (ContinuousLinearMap.toWOT 𝕜 E F), ContinuousLinearMap.continuous_toWOT⟩
 
-end NormedSpace
+end toWOT_continuous
+
+end ContinuousLinearMapWOT
diff --git a/Mathlib/Condensed/Discrete/Colimit.lean b/Mathlib/Condensed/Discrete/Colimit.lean
index 9e6930f3aa849..b5f5decb0e322 100644
--- a/Mathlib/Condensed/Discrete/Colimit.lean
+++ b/Mathlib/Condensed/Discrete/Colimit.lean
@@ -188,34 +188,33 @@ def fintypeCatAsCofan (X : Profinite) :
   Cofan.mk X (fun x ↦ (ContinuousMap.const _ x))
 
 /-- A finite set is the coproduct of its points in `Profinite`. -/
-def fintypeCatAsCofanIsColimit (X : Profinite) [Fintype X] :
+def fintypeCatAsCofanIsColimit (X : Profinite) [Finite X] :
     IsColimit (fintypeCatAsCofan X) := by
   refine mkCofanColimit _ (fun t ↦ ⟨fun x ↦ t.inj x PUnit.unit, ?_⟩) ?_
     (fun _ _ h ↦ by ext x; exact ContinuousMap.congr_fun (h x) _)
-  · convert continuous_bot
-    exact (inferInstanceAs (DiscreteTopology X)).1
+  · apply continuous_of_discreteTopology (α := X)
   · aesop
 
 variable [PreservesFiniteProducts F]
 
-noncomputable instance (X : Profinite) [Fintype X] :
+noncomputable instance (X : Profinite) [Finite X] :
     PreservesLimitsOfShape (Discrete X) F :=
   let X' := (Countable.toSmall.{0} X).equiv_small.choose
   let e : X ≃ X' := (Countable.toSmall X).equiv_small.choose_spec.some
-  have : Fintype X' := Fintype.ofEquiv X e
+  have : Finite X' := .of_equiv X e
   preservesLimitsOfShapeOfEquiv (Discrete.equivalence e.symm) F
 
 /-- Auxiliary definition for `isoFinYoneda`. -/
-def isoFinYonedaComponents (X : Profinite.{u}) [Fintype X] :
+def isoFinYonedaComponents (X : Profinite.{u}) [Finite X] :
     F.obj ⟨X⟩ ≅ (X → F.obj ⟨Profinite.of PUnit.{u+1}⟩) :=
   (isLimitFanMkObjOfIsLimit F _ _
     (Cofan.IsColimit.op (fintypeCatAsCofanIsColimit X))).conePointUniqueUpToIso
       (Types.productLimitCone.{u, u+1} fun _ ↦ F.obj ⟨Profinite.of PUnit.{u+1}⟩).2
 
-lemma isoFinYonedaComponents_hom_apply (X : Profinite.{u}) [Fintype X] (y : F.obj ⟨X⟩) (x : X) :
+lemma isoFinYonedaComponents_hom_apply (X : Profinite.{u}) [Finite X] (y : F.obj ⟨X⟩) (x : X) :
     (isoFinYonedaComponents F X).hom y x = F.map ((Profinite.of PUnit.{u+1}).const x).op y := rfl
 
-lemma isoFinYonedaComponents_inv_comp {X Y : Profinite.{u}} [Fintype X] [Fintype Y]
+lemma isoFinYonedaComponents_inv_comp {X Y : Profinite.{u}} [Finite X] [Finite Y]
     (f : Y → F.obj ⟨Profinite.of PUnit⟩) (g : X ⟶ Y) :
     (isoFinYonedaComponents F X).inv (f ∘ g) = F.map g.op ((isoFinYonedaComponents F Y).inv f) := by
   apply injective_of_mono (isoFinYonedaComponents F X).hom
@@ -461,12 +460,11 @@ def fintypeCatAsCofan (X : LightProfinite) :
   Cofan.mk X (fun x ↦ (ContinuousMap.const _ x))
 
 /-- A finite set is the coproduct of its points in `LightProfinite`. -/
-def fintypeCatAsCofanIsColimit (X : LightProfinite) [Fintype X] :
+def fintypeCatAsCofanIsColimit (X : LightProfinite) [Finite X] :
     IsColimit (fintypeCatAsCofan X) := by
   refine mkCofanColimit _ (fun t ↦ ⟨fun x ↦ t.inj x PUnit.unit, ?_⟩) ?_
     (fun _ _ h ↦ by ext x; exact ContinuousMap.congr_fun (h x) _)
-  · convert continuous_bot
-    exact (inferInstanceAs (DiscreteTopology X)).1
+  · apply continuous_of_discreteTopology (α := X)
   · aesop
 
 variable [PreservesFiniteProducts F]
@@ -478,17 +476,17 @@ noncomputable instance (X : FintypeCat.{u}) : PreservesLimitsOfShape (Discrete X
   preservesLimitsOfShapeOfEquiv (Discrete.equivalence e.symm) F
 
 /-- Auxiliary definition for `isoFinYoneda`. -/
-def isoFinYonedaComponents (X : LightProfinite.{u}) [Fintype X] :
+def isoFinYonedaComponents (X : LightProfinite.{u}) [Finite X] :
     F.obj ⟨X⟩ ≅ (X → F.obj ⟨LightProfinite.of PUnit.{u+1}⟩) :=
   (isLimitFanMkObjOfIsLimit F _ _
     (Cofan.IsColimit.op (fintypeCatAsCofanIsColimit X))).conePointUniqueUpToIso
       (Types.productLimitCone.{u, u} fun _ ↦ F.obj ⟨LightProfinite.of PUnit.{u+1}⟩).2
 
-lemma isoFinYonedaComponents_hom_apply (X : LightProfinite.{u}) [Fintype X] (y : F.obj ⟨X⟩)
+lemma isoFinYonedaComponents_hom_apply (X : LightProfinite.{u}) [Finite X] (y : F.obj ⟨X⟩)
     (x : X) : (isoFinYonedaComponents F X).hom y x =
       F.map ((LightProfinite.of PUnit.{u+1}).const x).op y := rfl
 
-lemma isoFinYonedaComponents_inv_comp {X Y : LightProfinite.{u}} [Fintype X] [Fintype Y]
+lemma isoFinYonedaComponents_inv_comp {X Y : LightProfinite.{u}} [Finite X] [Finite Y]
     (f : Y → F.obj ⟨LightProfinite.of PUnit⟩) (g : X ⟶ Y) :
     (isoFinYonedaComponents F X).inv (f ∘ g) = F.map g.op ((isoFinYonedaComponents F Y).inv f) := by
   apply injective_of_mono (isoFinYonedaComponents F X).hom
diff --git a/Mathlib/GroupTheory/Perm/DomMulAct.lean b/Mathlib/GroupTheory/Perm/DomMulAct.lean
index 37e7b1a23eb39..3ba4638ac8dab 100644
--- a/Mathlib/GroupTheory/Perm/DomMulAct.lean
+++ b/Mathlib/GroupTheory/Perm/DomMulAct.lean
@@ -105,10 +105,12 @@ theorem stabilizer_card [DecidableEq α] [DecidableEq ι] [Fintype ι] :
   · exact Finset.prod_congr rfl fun i _ ↦ by rw [Nat.card_eq_fintype_card, Fintype.card_perm]
   · rfl
 
+omit [Fintype α] in
 /-- The cardinality of the set of permutations preserving a function -/
-theorem stabilizer_ncard [Fintype ι] :
+theorem stabilizer_ncard [Finite α] [Fintype ι] :
     Set.ncard {g : Perm α | f ∘ g = f} = ∏ i, (Set.ncard {a | f a = i})! := by
   classical
+  cases nonempty_fintype α
   simp only [← Set.Nat.card_coe_set_eq, Set.coe_setOf, card_eq_fintype_card]
   exact stabilizer_card f
 
diff --git a/Mathlib/LinearAlgebra/Matrix/Ideal.lean b/Mathlib/LinearAlgebra/Matrix/Ideal.lean
index f251e331989ae..1faf6acf79f30 100644
--- a/Mathlib/LinearAlgebra/Matrix/Ideal.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Ideal.lean
@@ -123,7 +123,7 @@ theorem asIdeal_matricesOver [DecidableEq n] (I : TwoSidedIdeal R) :
     asIdeal (I.matricesOver n) = (asIdeal I).matricesOver n := by
   ext; simp
 
-variable {n : Type*} [Fintype n] [DecidableEq n]
+variable {n : Type*} [Fintype n]
 
 /--
 Two-sided ideals in $R$ correspond bijectively to those in $Mₙ(R)$.
@@ -139,12 +139,15 @@ def equivMatricesOver (i j : n) : TwoSidedIdeal R ≃ TwoSidedIdeal (Matrix n n
     (by rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩; exact ⟨x + y, J.add_mem hx hy, rfl⟩)
     (by rintro _ ⟨x, hx, rfl⟩; exact ⟨-x, J.neg_mem hx, rfl⟩)
     (by
+      classical
       rintro x _ ⟨y, hy, rfl⟩
       exact ⟨diagonal (fun _ ↦ x) * y, J.mul_mem_left _ _ hy, by simp⟩)
     (by
+      classical
       rintro _ y ⟨x, hx, rfl⟩
       exact ⟨x * diagonal (fun _ ↦ y), J.mul_mem_right _ _ hx, by simp⟩)
   right_inv J := SetLike.ext fun x ↦ by
+    classical
     simp only [mem_mk', Set.mem_image, SetLike.mem_coe, mem_matricesOver]
     constructor
     · intro h