Fill T_eq_diag sorry in Concrete.lean

FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Concrete.lean

@@ -1167,6 +1167,7 @@ namespace HeckeOperator
 
 set_option maxSynthPendingDepth 1 in
 open scoped TensorProduct.RightActions in
+omit [IsTotallyReal F] in
 /-- The T_v Hecke operator's underlying group element equals `diag r α hα`
 when α is the local uniformizer at v. -/
 lemma T_eq_diag (v : HeightOneSpectrum (𝓞 F))
@@ -1175,19 +1176,45 @@ lemma T_eq_diag (v : HeightOneSpectrum (𝓞 F))
     T r R v = AbstractHeckeOperator.HeckeOperator (R := R) (diag r α hα) (U1 r S) (U1 r S)
       (QuotientGroup.mk_image_finite_of_compact_of_open (U1_compact r S) (U1_open r S)) := by
   unfold T
-  congr 1
-  -- Show two Units in (D ⊗ 𝔸_F^∞)ˣ are equal by showing their values are equal.
-  -- Both go through r.symm applied to a GL₂(𝔸) element.
-  -- Show they produce the same D ⊗ 𝔸 element.
   unfold diag
-  -- Apply Units.ext to reduce to value equality.
-  ext : 1
-  -- Both sides map r.symm to a GL₂(𝔸_F) element.
-  -- LHS value: r.symm (diagonal ![ϖ_v, 1])
-  -- RHS value: r.symm (restrictedProduct.symm (mulSingle v (Local.diag α hα)))
-  -- These are equal because diagonal ![ϖ_v, 1] = restrictedProduct.symm (mulSingle v (Local.diag α hα))
-  -- when α coerces to the uniformizer at v.
-  sorry
+  dsimp only
+  congr 1
+  have key : Matrix.GeneralLinearGroup.diagonal
+      ![FiniteAdeleRing.localUniformiserUnit F v, 1] =
+      FiniteAdeleRing.GL2.restrictedProduct.symm
+        (RestrictedProduct.mulSingle _ v (Local.GL2.diag α hα)) := by
+    apply FiniteAdeleRing.GL2.restrictedProduct.injective
+    rw [ContinuousMulEquiv.apply_symm_apply]
+    apply RestrictedProduct.ext; intro w
+    obtain rfl | hwv := eq_or_ne w v
+    · simp only [RestrictedProduct.mulSingle_eq_same]
+      ext i j
+      change (FiniteAdeleRing.GL2.toAdicCompletion w
+        (Matrix.GeneralLinearGroup.diagonal
+          ![FiniteAdeleRing.localUniformiserUnit F w, 1])).val i j = _
+      fin_cases i <;> fin_cases j <;>
+        simp (config := { unfoldPartialApp := true }) [FiniteAdeleRing.GL2.toAdicCompletion,
+          Matrix.GeneralLinearGroup.diagonal, Matrix.diagonal,
+          Local.GL2.diag, h_eq, FiniteAdeleRing.localUniformiserUnit,
+          FiniteAdeleRing.localUniformiser,
+          IsDedekindDomain.FiniteAdeleRing.toAdicCompletion,
+          RestrictedProduct.evalRingHom, RestrictedProduct.evalMonoidHom] <;>
+        exact @Pi.mulSingle_eq_same (HeightOneSpectrum (𝓞 F))
+          (fun v => v.adicCompletion F) _ _ w (adicCompletionUniformizer F w)
+    · simp only [RestrictedProduct.mulSingle_eq_of_ne _ _ hwv]
+      ext i j
+      change (FiniteAdeleRing.GL2.toAdicCompletion w
+        (Matrix.GeneralLinearGroup.diagonal
+          ![FiniteAdeleRing.localUniformiserUnit F v, 1])).val i j = _
+      fin_cases i <;> fin_cases j <;>
+        simp (config := { unfoldPartialApp := true }) [FiniteAdeleRing.GL2.toAdicCompletion,
+          Matrix.GeneralLinearGroup.diagonal, Matrix.diagonal,
+          FiniteAdeleRing.localUniformiserUnit, FiniteAdeleRing.localUniformiser,
+          IsDedekindDomain.FiniteAdeleRing.toAdicCompletion,
+          RestrictedProduct.evalRingHom, RestrictedProduct.evalMonoidHom] <;>
+        exact Pi.mulSingle_eq_of_ne hwv (adicCompletionUniformizer F v)
+  rw [key]
+  rfl
 
 set_option maxSynthPendingDepth 1 in
 open scoped TensorProduct.RightActions in

keepalive.txt

@@ -0,0 +1,66 @@
+-- keepalive 202604232045
+-- keepalive 202604232145
+-- keepalive 202604232246
+-- keepalive 202604232346
+-- keepalive 202604240046
+-- keepalive 202604240146
+-- keepalive 202604240246
+-- keepalive 202604240346
+-- keepalive 202604240446
+-- keepalive 202604240546
+-- keepalive 202604240646
+-- keepalive 202604240746
+-- keepalive 202604240847
+-- keepalive 202604240947
+-- keepalive 202604241047
+-- keepalive 202604241147
+-- keepalive 202604241247
+-- keepalive 202604241347
+-- keepalive 202604241447
+-- keepalive 202604241547
+-- keepalive 202604241647
+-- keepalive 202604241748
+-- keepalive 202604241848
+-- keepalive 202604241948
+-- keepalive 202604242048
+-- keepalive 202604242148
+-- keepalive 202604242248
+-- keepalive 202604242348
+-- keepalive 202604250048
+-- keepalive 202604250148
+-- keepalive 202604250249
+-- keepalive 202604250349
+-- keepalive 202604250449
+-- keepalive 202604250549
+-- keepalive 202604250649
+-- keepalive 202604250749
+-- keepalive 202604250849
+-- keepalive 202604250949
+-- keepalive 202604251049
+-- keepalive 202604251150
+-- keepalive 202604251250
+-- keepalive 202604251350
+-- keepalive 202604251450
+-- keepalive 202604251550
+-- keepalive 202604251650
+-- keepalive 202604251750
+-- keepalive 202604251850
+-- keepalive 202604251950
+-- keepalive 202604252050
+-- keepalive 202604252150
+-- keepalive 202604252251
+-- keepalive 202604252351
+-- keepalive 202604260051
+-- keepalive 202604260151
+-- keepalive 202604260251
+-- keepalive 202604260351
+-- keepalive 202604260451
+-- keepalive 202604260551
+-- keepalive 202604260651
+-- keepalive 202604260752
+-- keepalive 202604260852
+-- keepalive 202604260952
+-- keepalive 202604261052
+-- keepalive 202604261152
+-- keepalive 202604261252
+-- keepalive 202604261352