feat: lemmas towards showing gaussNorm on MvPowerSeries is an absolute value (leanprover-community#38049)

We prove lemmas: ``gaussNorm_mul_le`` and ``gaussNorm_le_mul`` which will allow us to show it is an absolute value on Mv restricted power series.

Co-authored-by: WilliamCoram <williamecoram@gmail.com>

Author: WilliamCoram

Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean

@@ -19,6 +19,9 @@ nonarchimedean functions.
 
 public section
 
+/- TODO: Remove the Funlike hypothesis on these statements and turn them all into the form
+  {f : α → R} + properties on f. -/
+
 namespace IsNonarchimedean
 
 variable {R : Type*} [Semiring R] [LinearOrder R] {a b : R} {m n : ℕ}
@@ -112,6 +115,37 @@ theorem add_eq_max_of_ne {F α : Type*} [AddGroup α] [FunLike F α R]
   · rw [add_eq_left_of_lt hna h_lt]
     exact (max_eq_left_of_lt h_lt).symm
 
+/- TODO: Remove the funlike conditions on the lemmas required for add_max_of_ne, this will allow us
+  to remove the CommGroup part in the below which is unnecessary. -/
+
+lemma add_eq_max_of_ne' {α S : Type*} [Semiring S] [LinearOrder S] [AddCommGroup α]
+    (f : α → S) (fna : IsNonarchimedean f) (Neg : ∀ a, f a = f (-a)) {a b : α}
+    (hne : f a ≠ f b) : f (a + b) = max (f a) (f b) := by
+  wlog hab : f a > f b generalizing a b with H
+  · simpa [add_comm, max_comm] using (H hne.symm ((not_lt.mp hab).lt_of_ne hne))
+  apply le_antisymm (fna a b)
+  rcases le_max_iff.mp (fna (a + b) (-b)) with h | h
+  · simpa [max_eq_left (le_of_lt hab)] using h
+  · exact absurd h (not_le.mpr (by simpa [Neg b] using hab))
+
+omit [Semiring R] in
+open Finset in
+/-- Ultrametric inequality with `Finset.sum`. -/
+lemma apply_sum_le_sup {α β : Type*} [AddCommMonoid α] {f : α → R}
+    (nonarch : IsNonarchimedean f) {s : Finset β} (hnonempty : s.Nonempty) {l : β → α} :
+    f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun i => f (l i) := by
+  induction hnonempty using Nonempty.cons_induction with
+  | singleton i => simp
+  | cons i s _ hs hind =>
+    simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
+    rw [← le_sup'_iff hs]
+    rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
+    · exact .inl h₁
+    · exact .inr <| le_trans h₂ hind
+
+@[deprecated (since := "2026-04-27")]
+alias apply_sum_le_sup_of_isNonarchimedean := apply_sum_le_sup
+
 omit [Semiring R] in
 /-- Given a nonarchimedean function `α → R`, a function `g : β → α` and a nonempty multiset
   `s : Multiset β`, we can always find `b : β` belonging to `s` such that
@@ -133,11 +167,10 @@ theorem multiset_image_add_of_nonempty {α β : Type*} [AddCommMonoid α] [Nonem
 omit [Semiring R] in
 /-- Given a nonarchimedean function `α → R`, a function `g : β → α` and a nonempty finset
   `t : Finset β`, we can always find `b : β` belonging to `t` such that `f (t.sum g) ≤ f (g b)` . -/
-theorem finset_image_add_of_nonempty {α β : Type*} [AddCommMonoid α] [Nonempty β] {f : α → R}
+theorem finset_image_add_of_nonempty {α β : Type*} [AddCommMonoid α] {f : α → R}
     (hna : IsNonarchimedean f) (g : β → α) {t : Finset β} (ht : t.Nonempty) :
     ∃ b ∈ t, f (t.sum g) ≤ f (g b) := by
-  apply multiset_image_add_of_nonempty hna
-  simp_all [Finset.nonempty_iff_ne_empty]
+  simpa [Finset.le_sup'_iff] using IsNonarchimedean.apply_sum_le_sup hna ht
 
 /-- Given a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, a function `g : β → α`
   and a multiset `s : Multiset β`, we can always find `b : β`, belonging to `s` if `s` is nonempty,
@@ -155,13 +188,13 @@ theorem multiset_image_add {F α β : Type*} [AddCommMonoid α] [FunLike F α R]
 /-- Given a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, a function `g : β → α`
   and a finset `t : Finset β`, we can always find `b : β`, belonging to `t` if `t` is nonempty,
   such that `f (t.sum g) ≤ f (g b)` . -/
-theorem finset_image_add {F α β : Type*} [AddCommMonoid α] [FunLike F α R]
-    [ZeroHomClass F α R] [NonnegHomClass F α R] [Nonempty β] {f : F} (hna : IsNonarchimedean f)
-    (g : β → α) (t : Finset β) :
-    ∃ b : β, (t.Nonempty → b ∈ t) ∧ f (t.sum g) ≤ f (g b) := by
-  have h1 : t.Nonempty ↔ t.val ≠ 0 := by simp [Finset.nonempty_iff_ne_empty]
-  rw [h1]
-  exact multiset_image_add hna g t.val
+lemma finset_image_add {α β : Type*} [AddCommMonoid α] [Nonempty β] {f : α → R} (f_zero : f 0 = 0)
+    (f_nonneg : ∀ x, 0 ≤ f x) (hna : IsNonarchimedean f) (g : β → α) (t : Finset β) :
+    ∃ i, (t.Nonempty → i ∈ t) ∧ f (t.sum g) ≤ f (g i) := by
+  rcases t.eq_empty_or_nonempty with rfl | ht
+  · simp [f_zero, f_nonneg]
+  · exact (fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <|
+      IsNonarchimedean.finset_image_add_of_nonempty hna g ht
 
 open Multiset in
 theorem multiset_powerset_image_add [IsStrictOrderedRing R]
@@ -186,50 +219,30 @@ theorem finset_powerset_image_add [IsStrictOrderedRing R]
       f ((powersetCard (s.card - m) s).sum fun t : Finset β ↦
         t.prod fun i : β ↦ -b i) ≤ f (u.val.prod fun i : β ↦ -b i) := by
   set g := fun t : Finset β ↦ t.prod fun i : β ↦ - b i
-  obtain ⟨b, hb_in, hb⟩ := hf_na.finset_image_add g (powersetCard (s.card - m) s)
+  obtain ⟨b, hb_in, hb⟩ := hf_na.finset_image_add (by grind) (apply_nonneg f)
+    g (powersetCard (s.card - m) s)
   exact ⟨⟨b, hb_in (powersetCard_nonempty.mpr (Nat.sub_le s.card m))⟩, hb⟩
 
-omit [Semiring R] in
-open Finset in
-/-- Ultrametric inequality with `Finset.sum`. -/
-lemma apply_sum_le_sup {α β : Type*} [AddCommMonoid α] {f : α → R}
-    (nonarch : IsNonarchimedean f) {s : Finset β} (hnonempty : s.Nonempty) {l : β → α} :
-    f (∑ i ∈ s, l i) ≤ s.sup' hnonempty fun i => f (l i) := by
-  induction hnonempty using Nonempty.cons_induction with
-  | singleton i => simp
-  | cons i s _ hs hind =>
-    simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]
-    rw [← le_sup'_iff hs]
-    rcases le_max_iff.mp <| nonarch (l i) (∑ i ∈ s, l i) with h₁ | h₂
-    · exact .inl h₁
-    · exact .inr <| le_trans h₂ hind
-
-@[deprecated (since := "2026-04-27")]
-alias apply_sum_le_sup_of_isNonarchimedean := apply_sum_le_sup
-
-open Finset in
-lemma apply_sum_eq_of_lt {α β F : Type*} [AddCommGroup α] [FunLike F α R]
-    [AddGroupSeminormClass F α R] {f : F} (nonarch : IsNonarchimedean f) {s : Finset β} {l : β → α}
-    {k : β} (hk : k ∈ s) (hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)) :
-    f (∑ i ∈ s, l i) = f (l k) := by
-  have : s.Nonempty := by use k
-  induction this using Nonempty.cons_induction generalizing k with
-  | singleton a => simp_all
-  | cons a s _ hs _ =>
-    by_cases ha : k = a
-    · rw [sum_cons, ha]
-      apply add_eq_left_of_lt nonarch
-      grw [apply_sum_le_sup nonarch hs]
-      grind [sup'_lt_iff]
-    · grind [add_eq_right_of_lt nonarch]
+lemma apply_sum_eq_of_lt {α β : Type*} [AddCommGroup α] {f : α → R} (fna : IsNonarchimedean f)
+    (f_neg : ∀ a, f a = f (-a)) {s : Finset β} {l : β → α} {k : β} (hk : k ∈ s)
+    (hmax : ∀ j ∈ s, j ≠ k → f (l j) < f (l k)) : f (∑ i ∈ s, l i) = f (l k) := by
+  by_cases hcard : s.card = 1
+  · grind [Finset.card_eq_one.mp hcard]
+  · classical
+    rw [← Finset.add_sum_erase _ _ hk]
+    have hNonempty : (s.erase k).Nonempty :=
+      Finset.Nontrivial.erase_nonempty (Finset.one_lt_card_iff_nontrivial.mp (by grind))
+    have hrest_le := IsNonarchimedean.apply_sum_le_sup fna hNonempty (l := l)
+    simp only [Finset.le_sup'_iff, Finset.mem_erase, ne_eq] at hrest_le
+    rw [add_eq_max_of_ne' f fna f_neg (by grind), max_eq_left (le_of_lt (by grind))]
 
 /-- If `f` is a nonarchimedean additive group seminorm on a commutative ring `α`, `n : ℕ`, and
   `a b : α`, then we can find `m : ℕ` such that `m ≤ n` and
   `f ((a + b) ^ n) ≤ (f (a ^ m)) * (f (b ^ (n - m)))`. -/
 theorem add_pow_le {F α : Type*} [CommRing α] [FunLike F α R] [ZeroHomClass F α R]
     [NonnegHomClass F α R] [SubmultiplicativeHomClass F α R] {f : F} (hna : IsNonarchimedean f)
     (n : ℕ) (a b : α) : ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m)) := by
-  obtain ⟨m, hm_lt, hM⟩ := finset_image_add hna
+  obtain ⟨m, hm_lt, hM⟩ := finset_image_add (by aesop) (by aesop) hna
     (fun m => a ^ m * b ^ (n - m) * ↑(n.choose m)) (Finset.range (n + 1))
   simp only [Finset.nonempty_range_iff, ne_eq, Nat.succ_ne_zero, not_false_iff, Finset.mem_range,
     forall_true_left] at hm_lt

Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

@@ -120,7 +120,7 @@ theorem norm_mul_le_const_mul_norm {i : ι} (hBi : B i = (1 : L))
     obtain ⟨k, -, (hk : ‖∑ i : ι, (B.repr x i • ∑ i_1 : ι,
       B.repr y i_1 • B.repr (B i * B i_1)) ixy‖ ≤
       ‖(B.repr x k • ∑ j : ι, B.repr y j • B.repr (B k * B j)) ixy‖)⟩ :=
-      IsNonarchimedean.finset_image_add hna'
+      IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hna'
         (fun i ↦ (B.repr x i • ∑ i_1 : ι, B.repr y i_1 • B.repr (B i * B i_1)) ixy)
         (univ : Finset ι)
     simp only [Finsupp.coe_smul, Finsupp.coe_finsetSum, Pi.smul_apply, Finset.sum_apply,
@@ -130,7 +130,7 @@ theorem norm_mul_le_const_mul_norm {i : ι} (hBi : B i = (1 : L))
     obtain ⟨k', hk'⟩ : ∃ (k' : ι),
         ‖∑ j : ι, B.repr y j • B.repr (B k * B j) ixy‖ ≤
           ‖B.repr y k' • B.repr (B k * B k') ixy‖ := by
-      obtain ⟨k, hk0, hk⟩ := IsNonarchimedean.finset_image_add hna'
+      obtain ⟨k, hk0, hk⟩ := IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hna'
         (fun i ↦ B.repr y i • B.repr (B k * B i) ixy) (univ : Finset ι)
       exact ⟨k, hk⟩
     apply le_trans (mul_le_mul_of_nonneg_left hk' (norm_nonneg _))

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

@@ -271,7 +271,8 @@ theorem norm_root_le_spectralValue {f : AlgebraNorm K L} (hf_pm : IsPowMul f)
       set g := fun i : ℕ ↦ p.coeff i • x ^ i
       obtain ⟨m, hm_in, hm⟩ : ∃ (m : ℕ) (_ : 0 < p.natDegree → m < p.natDegree),
           f ((Finset.range p.natDegree).sum g) ≤ f (g m) := by
-        obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add hf_na g (Finset.range p.natDegree)
+        obtain ⟨m, hm, h⟩ := IsNonarchimedean.finset_image_add (map_zero _) (apply_nonneg _) hf_na g
+          (Finset.range p.natDegree)
         rw [Finset.nonempty_range_iff, ← zero_lt_iff, Finset.mem_range] at hm
         exact ⟨m, hm, h⟩
       exact lt_of_le_of_lt hm (hn' m (hm_in h_deg))

Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean

@@ -8,6 +8,8 @@ module
 public import Mathlib.Analysis.Normed.Ring.Basic
 public import Mathlib.RingTheory.MvPowerSeries.Basic
 
+public import Mathlib.Algebra.Order.Ring.IsNonarchimedean
+
 /-!
 # Gauss norm for multivariate power series
 
@@ -37,7 +39,11 @@ the set of all values of `v (coeff t f) * ∏ i : t.support, c i` for all `t : 
 
 namespace MvPowerSeries
 
-variable {R σ : Type*} [Semiring R] (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R)
+variable {R σ : Type*} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R)
+
+section Semiring
+
+variable [Semiring R]
 
 /-- Given a multivariate power series `f` in, a function `v : R → ℝ` and a tuple `c` of real
   numbers, the Gauss norm is defined as the supremum of the set of all values of
@@ -81,7 +87,7 @@ lemma gaussNorm_eq_zero_iff (vZero : v 0 = 0) (vNonneg : ∀ a, v a ≥ 0)
   _ ≤ _ := le_gaussNorm v c f hbd n
 
 lemma gaussNorm_add_le_max (f g : MvPowerSeries σ R) (hc : 0 ≤ c)
-    (vNonneg : ∀ a, v a ≥ 0) (hv : ∀ x y, v (x + y) ≤ max (v x) (v y))
+    (vNonneg : ∀ a, v a ≥ 0) (hv : IsNonarchimedean v)
     (hbfd : HasGaussNorm v c f) (hbgd : HasGaussNorm v c g) :
     gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g) := by
   have H (t : σ →₀ ℕ) : 0 ≤ ∏ i ∈ t.support, c i ^ t i :=
@@ -120,4 +126,106 @@ lemma gaussNorm_add_le_max (f g : MvPowerSeries σ R) (hc : 0 ≤ c)
     left
     exact gaussNorm_nonneg v c f vNonneg
 
+private lemma c_prod_nonneg (hc : 0 ≤ c) (t : σ →₀ ℕ) : 0 ≤ t.prod (c · ^ ·) :=
+  Finset.prod_nonneg (fun i _ ↦ pow_nonneg (hc i) (t i))
+
+lemma gaussNorm_mul_le (f g : MvPowerSeries σ R) (hc : 0 ≤ c) (vNonneg : ∀ a, v a ≥ 0)
+    (vMul : ∀ a b, v (a * b) ≤ v a * v b) (vna : IsNonarchimedean v)
+    (vZero : v 0 = 0) (hbfd : HasGaussNorm v c f) (hbgd : HasGaussNorm v c g) :
+    gaussNorm v c (f * g) ≤ gaussNorm v c f * gaussNorm v c g := by
+  classical
+  refine Real.iSup_le ?_ ?_
+  · intro t
+    obtain ⟨k, hk, hsum⟩ := IsNonarchimedean.finset_image_add vZero vNonneg vna
+      (fun a ↦ coeff a.1 f * coeff a.2 g) (Finset.antidiagonal t)
+    have hk' : k.1 + k.2 = t := by
+      simpa [Finset.mem_antidiagonal] using hk (Finset.nonempty_def.mpr ⟨(t, 0), by simp⟩)
+    have hprod : t.prod (c · ^ ·) = k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·) := by
+      simp [← hk', Finsupp.prod_add_index' (h := (c · ^ ·)) (by grind) (by grind)]
+    rw [hprod]
+    refine (mul_le_mul hsum (by rfl) (mul_nonneg (c_prod_nonneg c hc k.1) (c_prod_nonneg c hc k.2))
+      (vNonneg _)).trans ?_
+    have : v ((coeff k.1) f * (coeff k.2) g) * (k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·)) ≤
+        (v (coeff k.1 f) * k.1.prod (c · ^ ·)) * (v (coeff k.2 g) * k.2.prod (c · ^ ·)) := by
+      calc
+      _ ≤ v (coeff k.1 f) * v (coeff k.2 g) * (k.1.prod (c · ^ ·) * k.2.prod (c · ^ ·)) :=
+        mul_le_mul (vMul _ _) (by rfl) (mul_nonneg (c_prod_nonneg c hc k.1)
+          (c_prod_nonneg c hc k.2)) (mul_nonneg (vNonneg _) (vNonneg _))
+      _ = _ := by ring
+    exact this.trans (mul_le_mul (le_gaussNorm v c f hbfd k.1) (le_gaussNorm v c g hbgd k.2)
+      (mul_nonneg (vNonneg _) (c_prod_nonneg c hc k.2)) (gaussNorm_nonneg v c f vNonneg))
+  · exact mul_nonneg (gaussNorm_nonneg v c f vNonneg) (gaussNorm_nonneg v c g vNonneg)
+
+end Semiring
+
+variable [Ring R]
+
+/-- Predicate for when the gaussNorm is achieved by an index. -/
+abbrev AchievesGaussNorm (i : σ →₀ ℕ) : Prop :=
+  v (coeff i f) * i.prod (c · ^ ·) = gaussNorm v c f
+
+section absoluteValue
+
+variable {α S : Type*} [LinearOrder S] [AddCommGroup α] (f : α → S)
+
+lemma ultrametric_strict (na : IsNonarchimedean f)
+    (Neg : ∀ a, f a = f (-a)) {a b : α} (hne : f a ≠ f b) : f (a + b) = max (f a) (f b) := by
+  wlog hab : f a > f b generalizing a b with H
+  · simpa [add_comm, max_comm] using (H hne.symm ((not_lt.mp hab).lt_of_ne hne))
+  apply le_antisymm (na a b)
+  rcases le_max_iff.mp (na (a + b) (-b)) with h | h
+  · simpa [max_eq_left (le_of_lt hab)] using h
+  · exact absurd h (not_le.mpr (by simpa [Neg b] using hab))
+
+variable [Semiring S]
+
+lemma Finset.Nonempty.map_sum_le_sup'_map
+    {α S : Type*} [Semiring S] [LinearOrder S] [AddCommMonoid α] (g : α → S)
+    {ι : Type*} {s : Finset ι} (hs : s.Nonempty) (f : ι → α)
+    (na : ∀ a b, g (a + b) ≤ max (g a) (g b)) :
+    g (∑ i ∈ s, f i) ≤ s.sup' hs fun x ↦ g (f x) := by
+  simp only [Finset.le_sup'_iff]
+  induction hs using Finset.Nonempty.cons_induction with
+  | singleton j => simp only [Finset.mem_singleton, Finset.sum_singleton, exists_eq_left, le_refl]
+  | cons j s hj _ IH =>
+      simp only [Finset.sum_cons, Finset.mem_cons, exists_eq_or_imp]
+      refine (le_total (g (∑ i ∈ s, f i)) (g (f j))).imp ?_ ?_ <;> intro h
+      · exact (na _ _).trans (max_eq_left h).le
+      · exact ⟨_, IH.choose_spec.left, (na _ _).trans <|
+          ((max_eq_right h).le.trans IH.choose_spec.right)⟩
+
+variable [DecidableEq σ] (f g : MvPowerSeries σ R)
+
+lemma antidiagonal_dominant (i j : σ →₀ ℕ) (vna : IsNonarchimedean v)
+    (vMulEq : ∀ a b, v (a * b) = v a * v b) (vNeg : ∀ a, v a = v (-a))
+    (hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) →
+      v (coeff p.1 f * coeff p.2 g) < v (coeff i f) * v (coeff j g)) :
+    v (coeff (i + j) (f * g))  = v (coeff i f * coeff j g) := by
+  rw [← vMulEq] at hdom
+  rw [coeff_mul, IsNonarchimedean.apply_sum_eq_of_lt vna (by grind) (k := (i, j))
+    (s := Finset.antidiagonal (i + j)) (Finset.mem_antidiagonal.mpr rfl) hdom]
+
+lemma gaussNorm_le_mul (vMulEq : ∀ a b, v (a * b) = v a * v b)
+    (vna : IsNonarchimedean v) (vNeg : ∀ a, v a = v (-a))
+    (hbfg : HasGaussNorm v c (f * g))
+    (hdom : ∃ i j, AchievesGaussNorm v c f i ∧ AchievesGaussNorm v c g j ∧
+      ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) →
+        v (coeff p.1 f * coeff p.2 g) < v (coeff i f) * v (coeff j g)) :
+    gaussNorm v c f * gaussNorm v c g ≤ gaussNorm v c (f * g) := by
+  obtain ⟨i₀, j₀, hi₀, hj₀, hdom'⟩ := hdom
+  unfold AchievesGaussNorm at hi₀ hj₀
+  calc
+    _  = (v (coeff i₀ f) * i₀.prod (c · ^ ·)) * (v (coeff j₀ g) * j₀.prod (c · ^ ·)) := by
+          rw [← hi₀, ← hj₀]
+    _ = v (coeff i₀ f) * v (coeff j₀ g) * ((i₀ + j₀).prod (c · ^ ·)) := by
+          have hprod : (i₀ + j₀).prod (c · ^ ·) = i₀.prod (c · ^ ·) * j₀.prod (c · ^ ·) := by
+            simp [Finsupp.prod_add_index', pow_add]
+          rw [hprod]; ring
+    _ = v (coeff i₀ f * coeff j₀ g) * (i₀ + j₀).prod (c · ^ ·) := by rw [vMulEq]
+    _ = v (coeff (i₀ + j₀) (f * g)) * (i₀ + j₀).prod (c · ^ ·) := by
+      rw [antidiagonal_dominant v f g i₀ j₀ vna vMulEq vNeg hdom']
+    _ ≤ gaussNorm v c (f * g) := le_gaussNorm v c (f * g) hbfg (i₀ + j₀)
+
+end absoluteValue
+
 end MvPowerSeries

Mathlib/RingTheory/Polynomial/GaussNorm.lean

@@ -235,7 +235,7 @@ private theorem mul_gaussNorm_le_gaussNorm_mul (p q : R[X]) :
   apply le_of_eq_of_le _ <| (p * q).le_gaussNorm v hc0 (i + j)
   -- gaussNorm v c p * gaussNorm v c q is actually equal to v ((p * q).coeff (i + j)) * c ^ (i + j)
   rw [hi_p, hj_q, coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
-    IsNonarchimedean.apply_sum_eq_of_lt hna (k := i) (by simp)]
+    IsNonarchimedean.apply_sum_eq_of_lt hna (k := i) (by simp) (by simp)]
   /- IsNonarchimedean.apply_sum_eq_of_lt makes the goal almost trivial so we are left to prove
   the hmax hypothesis -/
   · grind