From e7cb995dc96519daaf2afd4bbf99dc3f55c80b87 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Sat, 18 May 2024 07:32:13 +0900
Subject: [PATCH 1/7] Composite HVertexOperators

---
 Mathlib/Algebra/Vertex/HVertexOperator.lean   | 81 ++++++++++++++++---
 Mathlib/RingTheory/HahnSeries/Addition.lean   | 44 +++++++---
 .../RingTheory/HahnSeries/Multiplication.lean | 78 ++++++++++++------
 3 files changed, 158 insertions(+), 45 deletions(-)

diff --git a/Mathlib/Algebra/Vertex/HVertexOperator.lean b/Mathlib/Algebra/Vertex/HVertexOperator.lean
index 3e99c7f2ea6569..61f6ce5d832a69 100644
--- a/Mathlib/Algebra/Vertex/HVertexOperator.lean
+++ b/Mathlib/Algebra/Vertex/HVertexOperator.lean
@@ -15,11 +15,10 @@ here allows us to consider composites and scalar-multiply by multivariable Laure
 ## Definitions
 * `HVertexOperator` : An `R`-linear map from an `R`-module `V` to `HahnModule Γ W`.
 * The coefficient function as an `R`-linear map.
+* Composition of heterogeneous vertex operators - values are Hahn series on lex order product.
 ## Main results
 * Ext
 ## To do:
-* Composition of heterogeneous vertex operators - values are Hahn series on lex order product
-  (needs PR#10781).
 * `HahnSeries Γ R`-module structure on `HVertexOperator Γ R V W` (needs PR#10846).  This means we
   can consider products of the form `(X-Y)^n A(X)B(Y)` for all integers `n`, where `(X-Y)^n` is
   expanded as `X^n(1-Y/X)^n` in `R((X))((Y))`.
@@ -42,25 +41,27 @@ abbrev HVertexOperator (Γ : Type*) [PartialOrder Γ] (R : Type*) [CommRing R]
     (V : Type*) (W : Type*) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] :=
   V →ₗ[R] (HahnModule Γ R W)
 
-namespace VertexAlg
+namespace HVertexOperator
+
+section Coeff
+
+open HahnModule
 
 @[ext]
-theorem HetVertexOperator.ext (A B : HVertexOperator Γ R V W) (h : ∀(v : V), A v = B v) :
+theorem ext (A B : HVertexOperator Γ R V W) (h : ∀(v : V), A v = B v) :
     A = B := LinearMap.ext h
 
 /-- The coefficient of a heterogeneous vertex operator, viewed as a formal power series with
 coefficients in linear maps. -/
 @[simps]
 def coeff (A : HVertexOperator Γ R V W) (n : Γ) : V →ₗ[R] W where
-  toFun := fun (x : V) => (A x).coeff n
+  toFun := fun (x : V) => ((of R).symm (A x)).coeff n
   map_add' := by
       intro x y
-      simp only [map_add, HahnSeries.add_coeff', Pi.add_apply, forall_const]
-      exact rfl
+      simp
   map_smul' := by
       intro r x
-      simp only [map_smul, HahnSeries.smul_coeff, RingHom.id_apply, forall_const]
-      exact rfl
+      simp
 
 theorem coeff_isPWOsupport (A : HVertexOperator Γ R V W) (v : V) : (A v).coeff.support.IsPWO :=
   (A v).isPWO_support'
@@ -87,3 +88,65 @@ def HetVertexOperator.of_coeff (f : Γ → V →ₗ[R] W)
     intros
     simp only [map_smul, RingHom.id_apply]
     exact rfl
+
+end Coeff
+
+section Products
+
+variable {Γ Γ' : Type*} [OrderedCancelAddCommMonoid Γ] [OrderedCancelAddCommMonoid Γ'] {R : Type*}
+  [CommRing R] {U V W : Type*} [AddCommGroup U] [Module R U][AddCommGroup V] [Module R V]
+  [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V)
+
+open HahnModule
+
+/-- The composite of two heterogeneous vertex operators acting on a vector, as an iterated Hahn
+  series.-/
+@[simps]
+def CompHahnSeries (u : U) : HahnSeries Γ' (HahnSeries Γ W) where
+  coeff g' := A (coeff B g' u)
+  isPWO_support' := by
+    refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_
+    simp_all only [coeff_apply, Function.support_subset_iff, ne_eq, Function.mem_support]
+    intro g' hg' hAB
+    apply hg'
+    simp_rw [hAB]
+    simp_all only [map_zero, HahnSeries.zero_coeff, not_true_eq_false]
+
+@[simp]
+theorem CompHahnSeries.add (u v : U) :
+    CompHahnSeries A B (u + v) = CompHahnSeries A B u + CompHahnSeries A B v := by
+  ext
+  simp only [CompHahnSeries_coeff, map_add, coeff_apply, HahnSeries.add_coeff', Pi.add_apply]
+  rw [← @HahnSeries.add_coeff]
+
+@[simp]
+theorem CompHahnSeries.sMul (r : R) (u : U) :
+    CompHahnSeries A B (r • u) = r • CompHahnSeries A B u := by
+  ext
+  simp only [CompHahnSeries_coeff, LinearMapClass.map_smul, coeff_apply, HahnSeries.smul_coeff]
+  exact rfl
+
+/-- The composite of two heterogeneous vertex operators, as a heterogeneous vertex operator. -/
+@[simps]
+def hComp : HVertexOperator (Γ' ×ₗ Γ) R U W where
+  toFun u := HahnModule.of R (HahnSeries.ofIterate (CompHahnSeries A B u))
+  map_add' := by
+    intro u v
+    ext g
+    simp only [HahnSeries.ofIterate, CompHahnSeries.add, Equiv.symm_apply_apply,
+      HahnModule.of_symm_add, HahnSeries.add_coeff', Pi.add_apply]
+  map_smul' := by
+    intro r x
+    ext g
+    simp only [HahnSeries.ofIterate, CompHahnSeries.sMul, Equiv.symm_apply_apply, RingHom.id_apply,
+      HahnSeries.smul_coeff, CompHahnSeries_coeff, coeff_apply]
+    exact rfl
+
+@[simp]
+theorem coeff_hetComp (g : Γ' ×ₗ Γ) :
+    (hComp A B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1 := by
+  rfl
+
+end Products
+
+end HVertexOperator
diff --git a/Mathlib/RingTheory/HahnSeries/Addition.lean b/Mathlib/RingTheory/HahnSeries/Addition.lean
index 5a57de828ad492..6b24a5bdeef8eb 100644
--- a/Mathlib/RingTheory/HahnSeries/Addition.lean
+++ b/Mathlib/RingTheory/HahnSeries/Addition.lean
@@ -185,9 +185,9 @@ instance [AddCommGroup R] : AddCommGroup (HahnSeries Γ R) :=
 
 end Addition
 
-section DistribMulAction
+section SMulZeroClass
 
-variable [PartialOrder Γ] {V : Type*} [Monoid R] [AddMonoid V] [DistribMulAction R V]
+variable [PartialOrder Γ] {V : Type*} [Zero V] [SMulZeroClass R V]
 
 instance : SMul R (HahnSeries Γ V) :=
   ⟨fun r x =>
@@ -199,6 +199,37 @@ theorem smul_coeff {r : R} {x : HahnSeries Γ V} {a : Γ} : (r • x).coeff a =
   rfl
 #align hahn_series.smul_coeff HahnSeries.smul_coeff
 
+instance : SMulZeroClass R (HahnSeries Γ V) :=
+  { inferInstanceAs (SMul R (HahnSeries Γ V)) with
+    smul_zero := by
+      intro
+      ext
+      simp only [smul_coeff, zero_coeff, smul_zero]}
+
+theorem orderTop_smul_not_lt (r : R) (x : HahnSeries Γ V) : ¬ (r • x).orderTop < x.orderTop := by
+  by_cases hrx : r • x = 0
+  · rw [hrx, orderTop_zero]
+    exact not_top_lt
+  · have hx : x ≠ 0 := right_ne_zero_of_smul hrx
+    simp [orderTop_of_ne hx, orderTop_of_ne hrx]
+    exact Set.IsWF.min_of_subset_not_lt_min
+      (Function.support_smul_subset_right (fun _ => r) x.coeff)
+
+theorem order_smul_not_lt [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :
+    ¬ (r • x).order < x.order := by
+  have hx : x ≠ 0 := right_ne_zero_of_smul h
+  simp_all only [order, dite_false]
+  exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right (fun _ => r) x.coeff)
+
+theorem le_order_smul {Γ} [Zero Γ] [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :
+    x.order ≤ (r • x).order := le_of_not_lt (order_smul_not_lt r x h)
+
+end SMulZeroClass
+
+section DistribMulAction
+
+variable [PartialOrder Γ] {V : Type*} [Monoid R] [AddMonoid V] [DistribMulAction R V]
+
 instance : DistribMulAction R (HahnSeries Γ V) where
   smul := (· • ·)
   one_smul _ := by
@@ -214,15 +245,6 @@ instance : DistribMulAction R (HahnSeries Γ V) where
     ext
     simp [mul_smul]
 
-theorem order_smul_not_lt [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :
-    ¬ (r • x).order < x.order := by
-  have hx : x ≠ 0 := right_ne_zero_of_smul h
-  simp_all only [order, dite_false]
-  exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right (fun _ => r) x.coeff)
-
-theorem le_order_smul {Γ} [Zero Γ] [LinearOrder Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :
-    x.order ≤ (r • x).order := le_of_not_lt (order_smul_not_lt r x h)
-
 variable {S : Type*} [Monoid S] [DistribMulAction S V]
 
 instance [SMul R S] [IsScalarTower R S V] : IsScalarTower R S (HahnSeries Γ V) :=
diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
index 131e9aeea13ec1..f8e0d727a2c64d 100644
--- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean
+++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
@@ -34,7 +34,7 @@ open BigOperators Pointwise
 
 noncomputable section
 
-variable {Γ Γ' R : Type*}
+variable {Γ Γ' R V : Type*}
 
 section Multiplication
 
@@ -80,25 +80,30 @@ def HahnModule (Γ R V : Type*) [PartialOrder Γ] [Zero V] [SMul R V] :=
 
 namespace HahnModule
 
-section
-
-variable {Γ R V : Type*} [PartialOrder Γ] [Zero V] [SMul R V]
-
 /-- The casting function to the type synonym. -/
-def of {Γ : Type*} (R : Type*) {V : Type*} [PartialOrder Γ] [Zero V] [SMul R V] :
+def of (R : Type*) [PartialOrder Γ] [Zero V] [SMul R V] :
     HahnSeries Γ V ≃ HahnModule Γ R V := Equiv.refl _
 
 /-- Recursion principle to reduce a result about the synonym to the original type. -/
 @[elab_as_elim]
-def rec {motive : HahnModule Γ R V → Sort*} (h : ∀ x : HahnSeries Γ V, motive (of R x)) :
-    ∀ x, motive x :=
+def rec [PartialOrder Γ] [Zero V] [SMul R V] {motive : HahnModule Γ R V → Sort*}
+    (h : ∀ x : HahnSeries Γ V, motive (of R x)) : ∀ x, motive x :=
   fun x => h <| (of R).symm x
 
 @[ext]
-theorem ext (x y : HahnModule Γ R V) (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y :=
+theorem ext [PartialOrder Γ] [Zero V] [SMul R V] (x y : HahnModule Γ R V)
+    (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y :=
   (of R).symm.injective <| HahnSeries.coeff_inj.1 h
 
-variable {V : Type*} [AddCommMonoid V] [SMul R V]
+theorem ext_iff [PartialOrder Γ] [Zero V] [SMul R V] (x y : HahnModule Γ R V) :
+    ((of R).symm x).coeff = ((of R).symm y).coeff ↔ x = y := by
+  simp_all only [HahnSeries.coeff_inj, EmbeddingLike.apply_eq_iff_eq]
+
+section SMul
+
+section
+
+variable [PartialOrder Γ] [AddCommMonoid V] [SMul R V]
 
 instance instAddCommMonoid : AddCommMonoid (HahnModule Γ R V) :=
   inferInstanceAs <| AddCommMonoid (HahnSeries Γ V)
@@ -118,24 +123,24 @@ instance instBaseModule [Semiring R] [Module R V] : Module R (HahnModule Γ R V)
 
 end
 
-variable {Γ R V : Type*} [OrderedCancelAddCommMonoid Γ] [AddCommMonoid V] [SMul R V]
+variable [OrderedCancelAddCommMonoid Γ] [AddCommMonoid V] [SMul R V]
 
 instance instSMul [Zero R] : SMul (HahnSeries Γ R) (HahnModule Γ R V) where
-  smul x y := {
+  smul x y := (of R) ({
     coeff := fun a =>
-      ∑ ij in addAntidiagonal x.isPWO_support y.isPWO_support a,
+      ∑ ij in addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
         x.coeff ij.fst • ((of R).symm y).coeff ij.snd
     isPWO_support' :=
         haveI h :
           { a : Γ |
-              (∑ ij : Γ × Γ in addAntidiagonal x.isPWO_support y.isPWO_support a,
-                  x.coeff ij.fst • y.coeff ij.snd) ≠
-                0 } ⊆
-            { a : Γ | (addAntidiagonal x.isPWO_support y.isPWO_support a).Nonempty } := by
+              (∑ ij : Γ × Γ in addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
+                  x.coeff ij.fst • y.coeff ij.snd) ≠ 0 } ⊆
+            { a : Γ |
+                (addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a).Nonempty } := by
           intro a ha
           contrapose! ha
           simp [not_nonempty_iff_eq_empty.1 ha]
-        isPWO_support_addAntidiagonal.mono h }
+        isPWO_support_addAntidiagonal.mono h } )
 
 theorem smul_coeff [Zero R] (x : HahnSeries Γ R) (y : HahnModule Γ R V) (a : Γ) :
     ((of R).symm <| x • y).coeff a =
@@ -145,14 +150,35 @@ theorem smul_coeff [Zero R] (x : HahnSeries Γ R) (y : HahnModule Γ R V) (a : 
 
 variable {W : Type*} [Zero R] [AddCommMonoid W]
 
-instance instSMulZeroClass [SMulZeroClass R W] :
-    SMulZeroClass (HahnSeries Γ R) (HahnModule Γ R W) where
+end SMul
+
+section SMulZeroClass
+
+section
+
+variable [PartialOrder Γ] [Zero R] [AddCommMonoid V] [SMulZeroClass R V]
+
+instance instBaseSMulZeroClass [PartialOrder Γ] [SMulZeroClass R V] :
+    SMulZeroClass R (HahnModule Γ R V) :=
+  inferInstanceAs <| SMulZeroClass R (HahnSeries Γ V)
+
+@[simp] theorem of_smul [PartialOrder Γ] [SMulZeroClass R V] (r : R) (x : HahnSeries Γ V) :
+  (of R) (r • x) = r • (of R) x := rfl
+@[simp] theorem of_symm_smul [PartialOrder Γ] [SMulZeroClass R V] (r : R) (x : HahnModule Γ R V) :
+  (of R).symm (r • x) = r • (of R).symm x := rfl
+
+end
+
+variable [OrderedCancelAddCommMonoid Γ] [Zero R] [AddCommMonoid V]
+
+instance instSMulZeroClass [SMulZeroClass R V] :
+    SMulZeroClass (HahnSeries Γ R) (HahnModule Γ R V) where
   smul_zero x := by
     ext
     simp [smul_coeff]
 
-theorem smul_coeff_right [SMulZeroClass R W] {x : HahnSeries Γ R}
-    {y : HahnModule Γ R W} {a : Γ} {s : Set Γ} (hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) :
+theorem smul_coeff_right [SMulZeroClass R V] {x : HahnSeries Γ R}
+    {y : HahnModule Γ R V} {a : Γ} {s : Set Γ} (hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) :
     ((of R).symm <| x • y).coeff a =
       ∑ ij in addAntidiagonal x.isPWO_support hs a,
         x.coeff ij.fst • ((of R).symm y).coeff ij.snd := by
@@ -162,11 +188,11 @@ theorem smul_coeff_right [SMulZeroClass R W] {x : HahnSeries Γ R}
   simp only [not_and, mem_sdiff, mem_addAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
   rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]
 
-theorem smul_coeff_left [SMulWithZero R W] {x : HahnSeries Γ R}
-    {y : HahnModule Γ R W} {a : Γ} {s : Set Γ}
+theorem smul_coeff_left [SMulWithZero R V] {x : HahnSeries Γ R}
+    {y : HahnModule Γ R V} {a : Γ} {s : Set Γ}
     (hs : s.IsPWO) (hxs : x.support ⊆ s) :
     ((of R).symm <| x • y).coeff a =
-      ∑ ij in addAntidiagonal hs y.isPWO_support a,
+      ∑ ij in addAntidiagonal hs ((of R).symm y).isPWO_support a,
         x.coeff ij.fst • ((of R).symm y).coeff ij.snd := by
   rw [smul_coeff]
   apply sum_subset_zero_on_sdiff (addAntidiagonal_mono_left hxs) _ fun _ _ => rfl
@@ -174,6 +200,8 @@ theorem smul_coeff_left [SMulWithZero R W] {x : HahnSeries Γ R}
   simp only [not_and', mem_sdiff, mem_addAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb
   rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]
 
+end SMulZeroClass
+
 end HahnModule
 
 variable [OrderedCancelAddCommMonoid Γ]

From c8ff1520527fa4ffb53273594b0b7df8bd7c698b Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Mon, 27 May 2024 06:10:41 +0900
Subject: [PATCH 2/7] naming conventions

---
 Mathlib/Algebra/Vertex/HVertexOperator.lean | 30 ++++++++++-----------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Algebra/Vertex/HVertexOperator.lean b/Mathlib/Algebra/Vertex/HVertexOperator.lean
index 61f6ce5d832a69..543e24c919bfd7 100644
--- a/Mathlib/Algebra/Vertex/HVertexOperator.lean
+++ b/Mathlib/Algebra/Vertex/HVertexOperator.lean
@@ -75,7 +75,7 @@ theorem coeff_inj : Function.Injective (coeff : HVertexOperator Γ R V W → Γ
 /-- Given a coefficient function valued in linear maps satisfying a partially well-ordered support
 condition, we produce a heterogeneous vertex operator. -/
 @[simps]
-def HetVertexOperator.of_coeff (f : Γ → V →ₗ[R] W)
+def of_coeff (f : Γ → V →ₗ[R] W)
     (hf : ∀(x : V), (Function.support (f · x)).IsPWO) : HVertexOperator Γ R V W where
   toFun := fun x =>
   { coeff := fun g => f g x
@@ -102,7 +102,7 @@ open HahnModule
 /-- The composite of two heterogeneous vertex operators acting on a vector, as an iterated Hahn
   series.-/
 @[simps]
-def CompHahnSeries (u : U) : HahnSeries Γ' (HahnSeries Γ W) where
+def compHahnSeries (u : U) : HahnSeries Γ' (HahnSeries Γ W) where
   coeff g' := A (coeff B g' u)
   isPWO_support' := by
     refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_
@@ -113,38 +113,38 @@ def CompHahnSeries (u : U) : HahnSeries Γ' (HahnSeries Γ W) where
     simp_all only [map_zero, HahnSeries.zero_coeff, not_true_eq_false]
 
 @[simp]
-theorem CompHahnSeries.add (u v : U) :
-    CompHahnSeries A B (u + v) = CompHahnSeries A B u + CompHahnSeries A B v := by
+theorem compHahnSeries_add (u v : U) :
+    compHahnSeries A B (u + v) = compHahnSeries A B u + compHahnSeries A B v := by
   ext
-  simp only [CompHahnSeries_coeff, map_add, coeff_apply, HahnSeries.add_coeff', Pi.add_apply]
+  simp only [compHahnSeries_coeff, map_add, coeff_apply, HahnSeries.add_coeff', Pi.add_apply]
   rw [← @HahnSeries.add_coeff]
 
 @[simp]
-theorem CompHahnSeries.sMul (r : R) (u : U) :
-    CompHahnSeries A B (r • u) = r • CompHahnSeries A B u := by
+theorem compHahnSeries_smul (r : R) (u : U) :
+    compHahnSeries A B (r • u) = r • compHahnSeries A B u := by
   ext
-  simp only [CompHahnSeries_coeff, LinearMapClass.map_smul, coeff_apply, HahnSeries.smul_coeff]
+  simp only [compHahnSeries_coeff, LinearMapClass.map_smul, coeff_apply, HahnSeries.smul_coeff]
   exact rfl
 
 /-- The composite of two heterogeneous vertex operators, as a heterogeneous vertex operator. -/
 @[simps]
-def hComp : HVertexOperator (Γ' ×ₗ Γ) R U W where
-  toFun u := HahnModule.of R (HahnSeries.ofIterate (CompHahnSeries A B u))
+def comp : HVertexOperator (Γ' ×ₗ Γ) R U W where
+  toFun u := HahnModule.of R (HahnSeries.ofIterate (compHahnSeries A B u))
   map_add' := by
     intro u v
     ext g
-    simp only [HahnSeries.ofIterate, CompHahnSeries.add, Equiv.symm_apply_apply,
+    simp only [HahnSeries.ofIterate, compHahnSeries_add, Equiv.symm_apply_apply,
       HahnModule.of_symm_add, HahnSeries.add_coeff', Pi.add_apply]
   map_smul' := by
     intro r x
     ext g
-    simp only [HahnSeries.ofIterate, CompHahnSeries.sMul, Equiv.symm_apply_apply, RingHom.id_apply,
-      HahnSeries.smul_coeff, CompHahnSeries_coeff, coeff_apply]
+    simp only [HahnSeries.ofIterate, compHahnSeries_smul, Equiv.symm_apply_apply, RingHom.id_apply,
+      HahnSeries.smul_coeff, compHahnSeries_coeff, coeff_apply]
     exact rfl
 
 @[simp]
-theorem coeff_hetComp (g : Γ' ×ₗ Γ) :
-    (hComp A B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1 := by
+theorem comp_coeff (g : Γ' ×ₗ Γ) :
+    (comp A B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1 := by
   rfl
 
 end Products

From ea61670e9865884211a26996781e806169278f9b Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Tue, 28 May 2024 17:36:27 +0900
Subject: [PATCH 3/7] put \in in

---
 Mathlib/RingTheory/HahnSeries/Multiplication.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
index cf96ee5a5d9f90..f0844a02d82e9a 100644
--- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean
+++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
@@ -128,12 +128,12 @@ variable [OrderedCancelAddCommMonoid Γ] [AddCommMonoid V] [SMul R V]
 instance instSMul [Zero R] : SMul (HahnSeries Γ R) (HahnModule Γ R V) where
   smul x y := (of R) ({
     coeff := fun a =>
-      ∑ ij in addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
+      ∑ ij ∈ addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
         x.coeff ij.fst • ((of R).symm y).coeff ij.snd
     isPWO_support' :=
         haveI h :
           { a : Γ |
-              (∑ ij : Γ × Γ in addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
+              (∑ ij : Γ × Γ ∈ addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
                   x.coeff ij.fst • y.coeff ij.snd) ≠ 0 } ⊆
             { a : Γ |
                 (addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a).Nonempty } := by
@@ -192,7 +192,7 @@ theorem smul_coeff_left [SMulWithZero R V] {x : HahnSeries Γ R}
     {y : HahnModule Γ R V} {a : Γ} {s : Set Γ}
     (hs : s.IsPWO) (hxs : x.support ⊆ s) :
     ((of R).symm <| x • y).coeff a =
-      ∑ ij in addAntidiagonal hs ((of R).symm y).isPWO_support a,
+      ∑ ij ∈ addAntidiagonal hs ((of R).symm y).isPWO_support a,
         x.coeff ij.fst • ((of R).symm y).coeff ij.snd := by
   rw [smul_coeff]
   apply sum_subset_zero_on_sdiff (addAntidiagonal_mono_left hxs) _ fun _ _ => rfl

From 1fe6524a313559a0c51de65b6cb4203c9b3be223 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Tue, 28 May 2024 20:58:46 +0900
Subject: [PATCH 4/7] fix replace

---
 Mathlib/RingTheory/HahnSeries/Multiplication.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
index f0844a02d82e9a..e95e39d76b26b4 100644
--- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean
+++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
@@ -133,7 +133,7 @@ instance instSMul [Zero R] : SMul (HahnSeries Γ R) (HahnModule Γ R V) where
     isPWO_support' :=
         haveI h :
           { a : Γ |
-              (∑ ij : Γ × Γ ∈ addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
+              (∑ ij ∈ addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
                   x.coeff ij.fst • y.coeff ij.snd) ≠ 0 } ⊆
             { a : Γ |
                 (addAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a).Nonempty } := by

From bdea2dd71147d6620f293990a885800ab236ba39 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Sun, 14 Jul 2024 18:28:32 +0900
Subject: [PATCH 5/7] fix parens

---
 Mathlib/RingTheory/HahnSeries/Multiplication.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
index 46350f764e7706..3c51bc31dbb903 100644
--- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean
+++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
@@ -145,7 +145,7 @@ instance instSMul [Zero R] : SMul (HahnSeries Γ R) (HahnModule Γ R V) where
           intro a ha
           contrapose! ha
           simp [not_nonempty_iff_eq_empty.1 ha]
-        isPWO_support_addAntidiagonal.mono h } )
+        isPWO_support_addAntidiagonal.mono h }
 
 theorem smul_coeff [Zero R] (x : HahnSeries Γ R) (y : HahnModule Γ R V) (a : Γ) :
     ((of R).symm <| x • y).coeff a =

From e96585adba28ec085f06fc08888667e2c3971f3e Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Wed, 17 Jul 2024 15:59:13 +0900
Subject: [PATCH 6/7] match HahnSeries file with current mathlib

---
 Mathlib/Algebra/Vertex/HVertexOperator.lean       |  1 +
 Mathlib/RingTheory/HahnSeries/Multiplication.lean | 11 +++--------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/Vertex/HVertexOperator.lean b/Mathlib/Algebra/Vertex/HVertexOperator.lean
index f8ae5133d6aae1..b3f30ba4982a65 100644
--- a/Mathlib/Algebra/Vertex/HVertexOperator.lean
+++ b/Mathlib/Algebra/Vertex/HVertexOperator.lean
@@ -20,6 +20,7 @@ here allows us to consider composites and scalar-multiply by multivariable Laure
 * `HahnSeries Γ R`-module structure on `HVertexOperator Γ R V W` (needs PR#10846).  This means we
   can consider products of the form `(X-Y)^n A(X)B(Y)` for all integers `n`, where `(X-Y)^n` is
   expanded as `X^n(1-Y/X)^n` in `R((X))((Y))`.
+* curry for tensor product inputs
 * more API to make ext comparisons easier.
 * formal variable API, e.g., like the `T` function for Laurent polynomials.
 ## References
diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
index 0983cdd29af9d4..0aa9dcc34948e5 100644
--- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean
+++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
@@ -93,19 +93,14 @@ def of (R : Type*) [SMul R V] :
 
 /-- Recursion principle to reduce a result about the synonym to the original type. -/
 @[elab_as_elim]
-def rec [PartialOrder Γ] [Zero V] [SMul R V] {motive : HahnModule Γ R V → Sort*}
-    (h : ∀ x : HahnSeries Γ V, motive (of R x)) : ∀ x, motive x :=
+def rec {motive : HahnModule Γ R V → Sort*} (h : ∀ x : HahnSeries Γ V, motive (of R x)) :
+    ∀ x, motive x :=
   fun x => h <| (of R).symm x
 
 @[ext]
-theorem ext [PartialOrder Γ] [Zero V] [SMul R V] (x y : HahnModule Γ R V)
-    (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y :=
+theorem ext (x y : HahnModule Γ R V) (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y :=
   (of R).symm.injective <| HahnSeries.coeff_inj.1 h
 
-theorem ext_iff [PartialOrder Γ] [Zero V] [SMul R V] (x y : HahnModule Γ R V) :
-    ((of R).symm x).coeff = ((of R).symm y).coeff ↔ x = y := by
-  simp_all only [HahnSeries.coeff_inj, EmbeddingLike.apply_eq_iff_eq]
-
 end
 
 section SMul

From fe48b68adaf330b50cb242d275d71a9fde136921 Mon Sep 17 00:00:00 2001
From: Scott Carnahan <128885296+ScottCarnahan@users.noreply.github.com>
Date: Thu, 18 Jul 2024 05:14:58 +0900
Subject: [PATCH 7/7] follow reviewer's suggestion

---
 Mathlib/Algebra/Vertex/HVertexOperator.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Vertex/HVertexOperator.lean b/Mathlib/Algebra/Vertex/HVertexOperator.lean
index b3f30ba4982a65..6cb129ebc3c5d4 100644
--- a/Mathlib/Algebra/Vertex/HVertexOperator.lean
+++ b/Mathlib/Algebra/Vertex/HVertexOperator.lean
@@ -35,7 +35,7 @@ variable {Γ : Type*} [PartialOrder Γ] {R : Type*} {V W : Type*} [CommRing R]
   [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W]
 
 /-- A heterogeneous `Γ`-vertex operator over a commutator ring `R` is an `R`-linear map from an
-`R`-module `V` to `Γ`-Hahn series with coefficients in an `R`-module `W`.-/
+`R`-module `V` to `Γ`-Hahn series with coefficients in an `R`-module `W`. -/
 abbrev HVertexOperator (Γ : Type*) [PartialOrder Γ] (R : Type*) [CommRing R]
     (V : Type*) (W : Type*) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] :=
   V →ₗ[R] (HahnModule Γ R W)
@@ -105,7 +105,7 @@ variable {Γ Γ' : Type*} [OrderedCancelAddCommMonoid Γ] [OrderedCancelAddCommM
 open HahnModule
 
 /-- The composite of two heterogeneous vertex operators acting on a vector, as an iterated Hahn
-  series.-/
+series. -/
 @[simps]
 def compHahnSeries (u : U) : HahnSeries Γ' (HahnSeries Γ W) where
   coeff g' := A (coeff B g' u)