From 95ac688266b378b80615fc9c08df134a21983e5f Mon Sep 17 00:00:00 2001
From: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Date: Sun, 1 Dec 2024 19:26:27 +0000
Subject: [PATCH 1/2] finish `adicCompletionTensorComapContinuousAlgHom` (#251)

---
 FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index a366d654..a3ad747e 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -277,11 +277,22 @@ attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 variable (v : HeightOneSpectrum A) in
 instance : TopologicalSpace (L ⊗[K] adicCompletion K v) := moduleTopology (adicCompletion K v) _
 
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
+variable (v : HeightOneSpectrum A) in
+instance : IsModuleTopology (adicCompletion K v) (L ⊗[K] adicCompletion K v) :=
+  ⟨rfl⟩
+
+attribute [local instance] Algebra.TensorProduct.rightAlgebra in
 noncomputable def adicCompletionTensorComapContinuousAlgHom (v : HeightOneSpectrum A) :
     L ⊗[K] adicCompletion K v →A[L]
       Π w : {w : HeightOneSpectrum B // v = comap A w}, adicCompletion L w.1 where
   __ := adicCompletionTensorComapAlgHom A K L B v
-  cont := sorry -- #237
+  cont := by
+    apply IsModuleTopology.continuous_of_ringHom (R := adicCompletion K v)
+    show Continuous (RingHom.comp _ (Algebra.TensorProduct.includeRight.toRingHom))
+    convert (adicCompletionContinuousComapAlgHom A K L B v).cont using 1
+    ext
+    simp [adicCompletionTensorComapAlgHom, adicCompletionContinuousComapAlgHom]
 
 noncomputable def adicCompletionComapAlgEquiv (v : HeightOneSpectrum A) :
   (L ⊗[K] (HeightOneSpectrum.adicCompletion K v)) ≃ₐ[L]

From 60fcaf3e8f33658d0fb473b3fd8de6e595024931 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 2 Dec 2024 11:08:16 +1100
Subject: [PATCH 2/2] chore: |x| < 1 implies x = 0 for x : Int (#260)

---
 FLT/NumberField/AdeleRing.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
index 4cf2fdf0..7f09a6f8 100644
--- a/FLT/NumberField/AdeleRing.lean
+++ b/FLT/NumberField/AdeleRing.lean
@@ -18,7 +18,6 @@ section BaseChange
 
 end BaseChange
 
-
 section Discrete
 
 open NumberField DedekindDomain
@@ -64,11 +63,13 @@ theorem Rat.AdeleRing.zero_discrete : ∃ U : Set (AdeleRing ℚ),
         -- and then h says it's not an integer
         sorry
       obtain ⟨y, rfl⟩ := intx
-      simp at h1
-      -- mathematically this is trivial:
-      -- h1 says that the integer y satisfies |y| < 1
-      -- and the goal is that y = 0
-      sorry
+      simp only [abs_lt] at h1
+      norm_cast at h1 ⊢
+      -- We need the next line because `norm_cast` is for some reason producing a `negSucc 0`.
+      -- I haven't been able to isolate this behaviour even in a standalone lemma.
+      -- We could also make `omega` more robust against accidental appearances of `negSucc`.
+      rw [Int.negSucc_eq] at h1
+      omega
     · intro x
       simp only [Set.mem_singleton_iff, Set.mem_preimage]
       rintro rfl