From 61669a7aa2252f54f4d546df3dbe9a87986e924b Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sun, 6 Oct 2024 20:25:37 +0200
Subject: [PATCH] Fix and silence some warnings

This makes it somewhat easier to spot legitimate output.
---
 FLT/AutomorphicForm/QuaternionAlgebra.lean     | 18 +++++++++---------
 .../ContinuousSMul_topology.lean               |  2 +-
 FLT/HIMExperiments/FGModuleTopology.lean       |  2 ++
 FLT/HIMExperiments/dual_topology.lean          |  6 +++---
 FLT/HIMExperiments/module_topology.lean        |  2 ++
 FLT/HIMExperiments/right_module_topology.lean  |  2 ++
 FLT/MathlibExperiments/Frobenius.lean          |  2 ++
 FLT/MathlibExperiments/Frobenius2.lean         |  1 +
 8 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/FLT/AutomorphicForm/QuaternionAlgebra.lean b/FLT/AutomorphicForm/QuaternionAlgebra.lean
index a046282e..ca56d6ac 100644
--- a/FLT/AutomorphicForm/QuaternionAlgebra.lean
+++ b/FLT/AutomorphicForm/QuaternionAlgebra.lean
@@ -20,7 +20,7 @@ suppress_compilation
 
 variable (F : Type*) [Field F] [NumberField F]
 
-variable (D : Type*) [Ring D] [Algebra F D] [FiniteDimensional F D]
+variable (D : Type*) [Ring D] [Algebra F D]
 
 open DedekindDomain
 
@@ -56,7 +56,7 @@ end missing_instances
 
 instance : TopologicalSpace (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := actionTopology (FiniteAdeleRing (𝓞 F) F) _
 instance : IsActionTopology (FiniteAdeleRing (𝓞 F) F) (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) := ⟨rfl⟩
-instance : TopologicalRing (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) :=
+instance [FiniteDimensional F D] : TopologicalRing (D ⊗[F] (FiniteAdeleRing (𝓞 F) F)) :=
   -- this def would be a dangerous instance
   -- (it can't guess R) but it's just a Prop so we can easily add it here
   ActionTopology.Module.topologicalRing (FiniteAdeleRing (𝓞 F) F) _
@@ -93,16 +93,16 @@ attribute [coe] AutomorphicForm.toFun
 theorem ext (φ ψ : AutomorphicForm F D M) (h : ∀ x, φ x = ψ x) : φ = ψ := by
   cases φ; cases ψ; simp only [mk.injEq]; ext; apply h
 
-def zero : (AutomorphicForm F D M) where
+def zero [FiniteDimensional F D] : (AutomorphicForm F D M) where
   toFun := 0
   left_invt := by simp
   loc_cst := by use ⊤; simp
 
-instance : Zero (AutomorphicForm F D M) where
+instance [FiniteDimensional F D] : Zero (AutomorphicForm F D M) where
   zero := zero
 
 @[simp]
-theorem zero_apply (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
+theorem zero_apply [FiniteDimensional F D] (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
     (0 : AutomorphicForm F D M) x = 0 := rfl
 
 def neg (φ : AutomorphicForm F D M) : AutomorphicForm F D M where
@@ -147,7 +147,7 @@ instance : Add (AutomorphicForm F D M) where
 theorem add_apply (φ ψ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
     (φ + ψ) x = (φ x) + (ψ x) := rfl
 
-instance addCommGroup : AddCommGroup (AutomorphicForm F D M) where
+instance addCommGroup [FiniteDimensional F D] : AddCommGroup (AutomorphicForm F D M) where
   add := (· + ·)
   add_assoc := by intros; ext; simp [add_assoc];
   zero := 0
@@ -184,7 +184,7 @@ theorem toConjAct_open {G : Type*} [Group G] [TopologicalSpace G] [TopologicalGr
     group
     exact hu
 
-instance : SMul (Dfx F D) (AutomorphicForm F D M) where
+instance [FiniteDimensional F D] : SMul (Dfx F D) (AutomorphicForm F D M) where
   smul g φ :=   { -- (g • f) (x) := f(xg) -- x(gf)=(xg)f
     toFun := fun x => φ (x * g)
     left_invt := by
@@ -204,10 +204,10 @@ instance : SMul (Dfx F D) (AutomorphicForm F D M) where
   }
 
 @[simp]
-theorem sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
+theorem sMul_eval [FiniteDimensional F D] (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteAdeleRing (𝓞 F) F)ˣ) :
   (g • f) x = f (x * g) := rfl
 
-instance : MulAction (Dfx F D) (AutomorphicForm F D M) where
+instance [FiniteDimensional F D] : MulAction (Dfx F D) (AutomorphicForm F D M) where
   smul := (· • ·)
   one_smul := by intros; ext; simp only [sMul_eval, mul_one]
   mul_smul := by intros; ext; simp only [sMul_eval, mul_assoc]
diff --git a/FLT/HIMExperiments/ContinuousSMul_topology.lean b/FLT/HIMExperiments/ContinuousSMul_topology.lean
index 6729cd6d..1804f9a4 100644
--- a/FLT/HIMExperiments/ContinuousSMul_topology.lean
+++ b/FLT/HIMExperiments/ContinuousSMul_topology.lean
@@ -94,7 +94,7 @@ lemma induced_continuous_smul [τA : TopologicalSpace A] [ContinuousSMul R A] (h
     @ContinuousSMul S B _ _ (TopologicalSpace.induced g τA) := by
   convert Inducing.continuousSMul (inducing_induced g) hf (fun {c} {x} ↦ map_smulₛₗ g c x)
 
-#check Prod.continuousSMul -- exists and is an instance :-)
+-- #check Prod.continuousSMul -- exists and is an instance :-)
 --#check Induced.continuousSMul -- doesn't exist
 
 end continuous_smul
diff --git a/FLT/HIMExperiments/FGModuleTopology.lean b/FLT/HIMExperiments/FGModuleTopology.lean
index 2e13c380..c322ac28 100644
--- a/FLT/HIMExperiments/FGModuleTopology.lean
+++ b/FLT/HIMExperiments/FGModuleTopology.lean
@@ -31,6 +31,8 @@ or $p$-adics).
 
 -/
 
+set_option linter.unusedSectionVars false
+
 section basics
 
 variable (R : Type*) [TopologicalSpace R] [Semiring R]
diff --git a/FLT/HIMExperiments/dual_topology.lean b/FLT/HIMExperiments/dual_topology.lean
index 6bad28c6..cb9193c8 100644
--- a/FLT/HIMExperiments/dual_topology.lean
+++ b/FLT/HIMExperiments/dual_topology.lean
@@ -94,7 +94,7 @@ namespace dual_topology
 
 section basics
 
-variable (R : Type*) [Monoid R] [TopologicalSpace R] [ContinuousMul R]
+variable (R : Type*) [Monoid R] [TopologicalSpace R]
 variable (A : Type*) [SMul R A]
 
 abbrev dualTopology : TopologicalSpace A :=
@@ -121,10 +121,10 @@ lemma isDualTopology [τA : TopologicalSpace A] [IsDualTopology R A] :
 end basics
 
 -- Non-commutative variables
-variable (R : Type*) [Monoid R] [τR: TopologicalSpace R] [ContinuousMul R]
+variable (R : Type*) [Monoid R] [τR: TopologicalSpace R]
 
 
-lemma Module.topology_self : τR = dualTopology R R := by
+lemma Module.topology_self [ContinuousMul R] : τR = dualTopology R R := by
   refine le_antisymm (le_iInf (fun i ↦ ?_)) <| sInf_le ⟨MulActionHom.id R, induced_id⟩
   rw [← continuous_iff_le_induced,
     show i = ⟨fun r ↦ r • i 1, fun _ _ ↦ mul_assoc _ _ _⟩ by
diff --git a/FLT/HIMExperiments/module_topology.lean b/FLT/HIMExperiments/module_topology.lean
index 88241835..ecf0450e 100644
--- a/FLT/HIMExperiments/module_topology.lean
+++ b/FLT/HIMExperiments/module_topology.lean
@@ -26,6 +26,8 @@ and target.
 
 -/
 
+set_option linter.unusedSectionVars false
+
 -- This was an early theorem I proved when I didn't know what was true or not, and
 -- was just experimenting.
 
diff --git a/FLT/HIMExperiments/right_module_topology.lean b/FLT/HIMExperiments/right_module_topology.lean
index 2aedf476..52cc7a80 100644
--- a/FLT/HIMExperiments/right_module_topology.lean
+++ b/FLT/HIMExperiments/right_module_topology.lean
@@ -35,6 +35,8 @@ functions from `M` (now considered only as an index set, so with no topology) to
 
 -/
 
+set_option linter.unusedSectionVars false
+
 -- See FLT.ForMathlib.ActionTopology for a parallel development.
 namespace right_module_topology
 
diff --git a/FLT/MathlibExperiments/Frobenius.lean b/FLT/MathlibExperiments/Frobenius.lean
index 0e8aab7e..9741921f 100644
--- a/FLT/MathlibExperiments/Frobenius.lean
+++ b/FLT/MathlibExperiments/Frobenius.lean
@@ -116,6 +116,8 @@ for "helping me to understand the math proof and to formalize it."
 
 -/
 
+set_option linter.unusedSectionVars false
+
 open Classical
 
 section FiniteFrobeniusDef
diff --git a/FLT/MathlibExperiments/Frobenius2.lean b/FLT/MathlibExperiments/Frobenius2.lean
index 2c08eb82..6f0d7d1d 100644
--- a/FLT/MathlibExperiments/Frobenius2.lean
+++ b/FLT/MathlibExperiments/Frobenius2.lean
@@ -181,6 +181,7 @@ open scoped algebraMap
 noncomputable local instance : Algebra A[X] B[X] :=
   RingHom.toAlgebra (Polynomial.mapRingHom (Algebra.toRingHom))
 
+omit [Fintype (B ≃ₐ[A] B)] [DecidableEq (Ideal B)] in
 @[simp, norm_cast]
 lemma coe_monomial (n : ℕ) (a : A) : ((monomial n a : A[X]) : B[X]) = monomial n (a : B) :=
   map_monomial _