chore: bump Lean stack to v4.31.0

ArkLib/Commitments/Functional/KZG/Binding.lean

@@ -630,8 +630,14 @@ lemma binding_cond_le_t_sdh_cond {n : ℕ} {AuxState : Type} [SampleableType G
       ((Option.map (fun result : RunResult => result.2) result₂).getD false)
       (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ) rfl hresp hg₁ hpair
       hverify₁ hverify₂
-  simpa only [bindingGameExt, kzg, OptionT.mk, pSpec', impl, sample, body, run₁, run₂,
-      pack, gameComp, P, Q] using hmono
+  change
+    Pr[P | OptionT.mk (do
+      let τ ← sample
+      (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))]
+    ≤ Pr[Q | OptionT.mk (do
+      let τ ← sample
+      (simulateQ impl (gameComp τ)).run' (∅ : unifSpec.QueryCache))]
+  exact hmono
 
 omit [DecidableEq G₁] [Module (ZMod p) (Additive G₁)]
   [Module (ZMod p) (Additive G₂)] in
@@ -662,16 +668,16 @@ lemma t_sdh_game_eq {n : ℕ} {AuxState : Type} [SampleableType G₁]
       (bindingReduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) AuxState
         adversary) := by
   let scheme := kzg (n := n) (g₁ := g₁) (g₂ := g₂) (pairing := pairing)
-  simp only [Groups.tSdhExperiment]
+  simp only [Groups.tSdhExperiment, Groups.tSdhGame]
   congr 1
   let pSpec' : ProtocolSpec 1 := ⟨!v[.P_to_V], !v[G₁]⟩
   let impl : QueryImpl _ (StateT unifSpec.QueryCache ProbComp) :=
     QueryImpl.addLift
       (randomOracle : QueryImpl unifSpec (StateT unifSpec.QueryCache ProbComp))
       (challengeQueryImpl (pSpec := pSpec'))
-  simpa only [bindingGameExt, bindingReduction, kzg, OptionT.mk, pSpec', impl, scheme,
-      OptionT.run_map] using
-    OptionT.map_mk_bind_eq_of_body
+  dsimp only [bindingGameExt, bindingReduction, kzg, OptionT.mk, pSpec', impl, scheme,
+    OptionT.run_map]
+  convert OptionT.map_mk_bind_eq_of_body
       (sample := (Groups.sampleNonzeroZMod (p := p) : ProbComp (ZMod p)))
       (body₁ := fun τ => (simulateQ impl (do
         let srs := Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ
@@ -715,9 +721,9 @@ lemma t_sdh_game_eq {n : ℕ} {AuxState : Type} [SampleableType G₁]
       (hBody := by
         intro τ
         dsimp only
-        refine StateT.map_run'_eq_of_map_eq _ _ _ _ (∅ : unifSpec.QueryCache) ?_
+        refine StateT.map_run'_eq_of_map_eq (∅ : unifSpec.QueryCache) ?_
         simp only [simulateQ_bind, simulateQ_pure, map_eq_bind_pure_comp, bind_assoc]
-        congr 1)
+        congr 1) using 1 <;> rfl
 
 omit [DecidableEq G₁] in
 /-- The t-SDH experiment is bounded by the t-SDH error. -/
@@ -746,7 +752,8 @@ theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
   letI game := Commitment.bindingGame (init := pure ∅) (impl := randomOracle)
     (AuxState := AuxState) (scheme := scheme) (adversary := adversary)
   letI game_ext := bindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary scheme
-  convert (
+  change Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game] ≤ tSdhError
+  exact
     calc Pr[Commitment.bindingCondition (Data := Fin (n + 1) → ZMod p) | game]
     _ = Pr[bindingCondExt (p := p) (n := n) | game_ext] :=
       binding_game_ext_eq_binding_game (pairing := pairing) adversary
@@ -760,7 +767,7 @@ theorem binding {g₁ : G₁} {g₂ : G₂} (hg₁ : g₁ ≠ 1)
       (bindingReduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) AuxState adversary) :=
       t_sdh_game_eq (g₁ := g₁) (g₂ := g₂) (pairing := pairing) adversary
     _ ≤ tSdhError := t_sdh_error_bound (g₁ := g₁) (g₂ := g₂) (pairing := pairing)
-      tSdhError htSdh adversary)
+      tSdhError htSdh adversary
 
 end Binding
 

ArkLib/Commitments/Functional/KZG/Correctness.lean

@@ -172,8 +172,10 @@ theorem correctness (hpG1 : Nat.card G₁ = p) {g₁ : G₁} {g₂ : G₂}
   obtain ⟨⟨ck, vk⟩, hkeygen, hx⟩ := hx
   rw [mem_support_bind_iff] at hx
   obtain ⟨⟨cm, decomm⟩, hcommit, hx⟩ := hx
-  replace hkeygen := OracleComp.mem_support_of_mem_support_liftComp _ _ hkeygen
-  replace hcommit := OracleComp.mem_support_of_mem_support_liftComp _ _ hcommit
+  replace hkeygen := OracleComp.mem_support_of_mem_support_liftComp
+    (superSpec := _) (oa := _) (x := (ck, vk)) hkeygen
+  replace hcommit := OracleComp.mem_support_of_mem_support_liftComp
+    (superSpec := _) (oa := _) (x := (cm, decomm)) hcommit
   rw [mem_support_bind_iff] at hkeygen
   obtain ⟨τ, _hτ, hkeygen⟩ := hkeygen
   rw [mem_support_pure_iff] at hkeygen
@@ -191,8 +193,9 @@ theorem correctness (hpG1 : Nat.card G₁ = p) {g₁ : G₁} {g₂ : G₂}
       (commit (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).1 data)
       (generateOpening (Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ).1 data query)
       query (OracleInterface.answer data query) := by
-    simpa [OracleInterface.answer] using
-      (KZG.correctness (pairing := pairing) (g₁ := g₁) (g₂ := g₂) hpG1 n τ data query)
+    change verifyOpening pairing _ _ _ query ((CPolynomial.ofFn data).eval query) = true
+    simpa only [CPolynomial.ofFn] using
+      KZG.correctness (pairing := pairing) (g₁ := g₁) (g₂ := g₂) hpG1 n τ data query
   simp only [Option.elimM] at hx
   rw [mem_support_bind_iff] at hx
   obtain ⟨openingOpt, hopeningOpt, hx⟩ := hx

ArkLib/Commitments/Functional/KZG/FunctionBinding/Basic.lean

@@ -296,7 +296,7 @@ lemma function_binding_game_ext_support_srs {n L : ℕ} {AuxState : Type} [Sampl
             (τ', Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ', cm', queryOf',
               (fun i => responseOf' i), accepts, proofs))
           (Option.map (fun resultOf i => (resultOf i).2) resultPairs)) := by
-    simpa [mem_support_pure_iff] using hx
+    exact (mem_support_pure_iff _ _).mp hx
   cases hres : resultPairs with
   | none => simp [hres] at hx'
   | some resultOf =>
@@ -343,10 +343,10 @@ lemma function_binding_game_ext_support_verify_all {n L : ℕ} {AuxState : Type}
         ((Option.map (fun resultOf i => (resultOf i).1) opts_v).bind fun accepts =>
           Option.map
             (fun proofs =>
-              (τ_v, Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v, cm_v, queryOf_v,
-                (fun i => responseOf_v i), accepts, proofs))
+              (τ_v, Groups.PowerSrs.generate (g₁ := g₁) (g₂ := g₂) n τ_v, claim_v.1,
+                claim_v.2.fst, (fun i => claim_v.2.2.1 i), accepts, proofs))
             (Option.map (fun resultOf i => (resultOf i).2) opts_v)) := by
-      simpa [mem_support_pure_iff] using hx
+      exact (mem_support_pure_iff _ _).mp hx
     cases hres : opts_v with
     | none => simp [hres] at hx'
     | some resultOf =>
@@ -611,7 +611,7 @@ lemma arsdh_game_eq {n L : ℕ} {AuxState : Type} [SampleableType G₁]
       (hBody := by
         intro τ
         dsimp only
-        refine StateT.map_run'_eq_of_map_eq _ _ _ _ (∅ : unifSpec.QueryCache) ?_
+        refine StateT.map_run'_eq_of_map_eq (∅ : unifSpec.QueryCache) ?_
         simp only [simulateQ_bind, simulateQ_pure, map_eq_bind_pure_comp, bind_assoc]
         congr 1
         funext claimResult
@@ -648,7 +648,9 @@ theorem function_binding {g₁ : G₁} {g₂ : G₂}
   letI game := Commitment.functionBindingGame (init := pure ∅) (impl := randomOracle) (hn := rfl)
     (AuxState := AuxState) (scheme := scheme) (adversary := adversary)
   letI game_ext := functionBindingGameExt (g₁ := g₁) (g₂ := g₂) AuxState adversary scheme
-  convert (
+  change Pr[Commitment.functionBindingCondition (Data := Fin (n + 1) → ZMod p) | game]
+    ≤ arsdhError
+  exact
     calc Pr[Commitment.functionBindingCondition (Data := Fin (n + 1) → ZMod p) | game]
     _ = Pr[functionBindingCondExt n L | game_ext] :=
       function_binding_game_ext_eq_function_binding_game (pairing := pairing) adversary
@@ -660,7 +662,7 @@ theorem function_binding {g₁ : G₁} {g₂ : G₂}
       (reduction (g₁ := g₁) (g₂ := g₂) (pairing := pairing) L hn AuxState adversary) :=
       arsdh_game_eq (g₁ := g₁) (g₂ := g₂) (pairing := pairing) hn adversary
     _ ≤ arsdhError := arsdh_error_bound (g₁ := g₁) (g₂ := g₂) (pairing := pairing) hn
-      arsdhError hArsdh adversary)
+      arsdhError hArsdh adversary
 
 
 end FunctionBinding

ArkLib/Data/Classes/FunEquiv.lean

@@ -40,7 +40,7 @@ instance : DFunEquiv (∀ a : α, β a) α β where
 /-- The forward direction of the equivalence is a `DFunLike`. -/
 instance : DFunLike F α β where
   coe := DFunEquiv.equiv.toFun
-  coe_injective' := DFunEquiv.equiv.injective
+  coe_injective := DFunEquiv.equiv.injective
 
 /-- Coercion from the dependent function type `∀ a : α, β a` to another type `F` that has a
 `DFunEquiv` instance.

ArkLib/Data/CodingTheory/Basic/Distance.lean

@@ -686,7 +686,7 @@ theorem dist'_eq_dist : ‖C‖₀'.toNat = ‖C‖₀ := by
             (by simpa [hvals] using hVals_nonempty))
       -- `vals.min ≤ dStar` since `dStar ∈ vals`.
       have h_le : vals.min ≤ (dStar : ℕ∞) := by
-        simpa using (Finset.min_le hmem_min')
+        exact Finset.min_le hmem_min'
       -- `dStar ≤ a` for all `a ∈ vals`, hence `dStar ≤ vals.min`.
       have h_ge : (dStar : ℕ∞) ≤ vals.min := by
         -- Use the universal lower-bound property of `min'`.

ArkLib/Data/CodingTheory/Basic/LinearCode.lean

@@ -281,7 +281,9 @@ lemma projectedCode_linearCombination [Field F] (LC : LinearCode ι F) (T : Fins
     exact ⟨Submodule.sum_mem _ fun j _ => Submodule.smul_mem _ _ (hw j |>.1),
       fun t ht => by simp [show ∀ j, U j t = w j t from
         fun j => congr_fun (hw j |>.2) ⟨t, ht⟩]⟩
-  exact ⟨w, hw.1, funext fun t => by simpa using Eq.symm (hw.2 t t.2)⟩
+  exact ⟨w, hw.1, funext fun t => by
+    change (∑ j, c j * U j t.1) = w t.1
+    exact Eq.symm (hw.2 t t.2)⟩
 
 /-- A linear code is maximum distance separable (MDS) if its parameters meet the singleton bound. -/
 def IsMDS {ι : Type} [Fintype ι] [CommRing F] [DecidableEq F] (LC : LinearCode ι F) : Prop :=
@@ -384,14 +386,8 @@ lemma rank_genMatrix_eq_dim [Field F] (LC : LinearCode ι F) :
 /-- The dimension of the linear code given by a generator matrix is the rank of the matrix. -/
 lemma dim_fromRowGenMat {k n : ℕ} [Field F] {G : Matrix (Fin k) (Fin n) F} :
     dim (fromRowGenMat G) = G.rank := by
-  unfold fromRowGenMat;
-  convert congr_arg (fun s : Submodule F _ => Module.finrank F s) _;
-  rotate_left;
-  · exact Submodule.span F (Set.range (fun i => G i));
-  · ext; simp [Matrix.vecMulLinear];
-    simp +decide [funext_iff, Matrix.vecMul, Submodule.mem_span_range_iff_exists_fun];
-    rfl;
-  · convert Matrix.rank_eq_finrank_span_row G using 1
+  unfold dim fromRowGenMat
+  rw [range_vecMulLinear, Matrix.rank_eq_finrank_span_row]
 
 /-- Given a linear code of length `ι` and dimension `dim` over a field `F`, we define its `ι × dim`
 generator matrix as a matrix whose columns are an `F`-basis of the code. -/
@@ -511,8 +507,8 @@ theorem singletonBound [CommRing F] [StrongRankCondition F]
       have hxS : ∀ i ∈ S, (x : ι → F) i = 0 := by
         intro i hi
         have := congrArg (fun (f : (S → F)) => f ⟨i, hi⟩) (by simpa using hx)
-        -- simp at this
-        simpa using this
+        change (x : ι → F) i = 0 at this
+        exact this
       -- bound the weight of x by |Sᶜ|
       let A : Finset ι := Finset.univ.filter (fun i => (x : ι → F) i ≠ 0)
       have hA_subset_compl : A ⊆ Sᶜ := by

ArkLib/Data/CodingTheory/Basic/MDSCode.lean

@@ -106,8 +106,7 @@ lemma IsMDS_of_matrix_IsMDS [Field F] [DecidableEq F] {G : Matrix (Fin k) (Fin n
       refine le_trans (h_dist_ge (u - v) ?_ ?_) ?_
       · exact Submodule.sub_mem _ hu hv
       · exact sub_ne_zero_of_ne huv
-      · convert hd using 1
-        exact congr_arg Finset.card (Finset.filter_congr fun x _ => by simp [sub_eq_zero])
+      · simpa only [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero] using hd
   have h_dist_le : Code.dist (fromRowGenMat G).carrier ≤ n - k + 1 := by
     contrapose! h_singleton_bound
     rw [tsub_add_eq_add_tsub ]

ArkLib/Data/CodingTheory/Basic/RelativeDistance.lean

@@ -287,7 +287,6 @@ lemma relCloseToCode_iff_relCloseToCodeword_of_minDist [Nonempty ι] [DecidableE
       use v; constructor
       · simp only [Subtype.coe_prop]
       · rw [relDistFromPickRelClosestCodeword_of_Nonempty_Code] at h_dist_le_e
-        simp only at h_dist_le_e
         rw [←ENNReal.coe_le_coe]
         exact h_dist_le_e
   · -- Direction 2: (←)
@@ -363,14 +362,11 @@ theorem relDistFromCode_le_iff_distFromCode_toENNReal_le {C : Set (ι → F)} (u
     δᵣ(u, C) ≤ δ ↔ (Δ₀(u, C) : ENNReal) ≤ δ * (Fintype.card ι : ℝ≥0) := by
   rw [relDistFromCode_le_iff_distFromCode_le]
   constructor <;> intro h
-  · simp_all only [ENNReal.coe_natCast]
-    convert ENNReal.ofReal_le_ofReal
-      (Nat.floor_le (show 0 ≤ δ * (Fintype.card ι : ℝ≥0) by positivity)) |>
-        le_trans (ENNReal.ofReal_le_ofReal <| ?_) using 1
-    any_goals exact Nat.cast (distFromCode u C |> ENat.toNat)
-    · cases h : distFromCode u C <;> aesop
-    · simp [ENNReal.ofReal_mul]
-    · cases h' : distFromCode u C <;> aesop
+  · refine (ENat.toENNReal_le.mpr h).trans ?_
+    change ((⌊δ * (Fintype.card ι : ℝ≥0)⌋₊ : ℝ≥0) : ENNReal) ≤
+      (δ * (Fintype.card ι : ℝ≥0) : ℝ≥0)
+    exact ENNReal.coe_le_coe.mpr
+      (Nat.floor_le (show 0 ≤ δ * (Fintype.card ι : ℝ≥0) by positivity))
   · contrapose! h
     cases h' : distFromCode u C
     · simp_all only [ENat.coe_lt_top, ENNReal.coe_natCast, ENat.toENNReal_top]

ArkLib/Data/CodingTheory/DivergenceOfSets.lean

@@ -87,7 +87,9 @@ theorem Pr_uniform_eq_one_imp_forall {α : Type} [Fintype α] [Nonempty α] (P :
   by_contra hPa
   let q : PMF Prop := ($ᵖ α : PMF α).map P
   have hqTrue : q True = 1 := by
-    simpa only [q, PMF.monad_map_eq_map] using hPr
+    change (P <$> ($ᵖ α : PMF α)) True = 1 at hPr
+    rw [PMF.monad_map_eq_map] at hPr
+    exact hPr
   have hsupport : q.support = {True} := (PMF.apply_eq_one_iff q True).1 hqTrue
   have hPfalse : P a = False := by
     exact propext (iff_false_intro hPa)
@@ -228,8 +230,8 @@ theorem proximity_gap_affineSubspace {ι : Type} [Fintype ι] [Nonempty ι] [Dec
     have hx_mem_S : (x : ι → F) ∈ S := by
       dsimp [S, Affine.AffSpanFinset]
       exact (Affine.AffSpanSet.instFinite (u := C 0)).mem_toFinset.2 (by
-        dsimp [Affine.AffSpanSet]
-        simpa using hx_mem_affineSpan)
+        change (x : ι → F) ∈ affineSpan F (Finset.univ.image u : Set (ι → F))
+        exact hx_mem_affineSpan)
     exact ⟨⟨(x : ι → F), hx_mem_S⟩⟩
   have hxorS :
       Xor
@@ -261,14 +263,13 @@ theorem proximity_gap_affineSubspace {ι : Type} [Fintype ι] [Nonempty ι] [Dec
   have h_AffSpanSet : Affine.AffSpanSet (U := C 0) = (U : Set (ι → F)) := by
     unfold Affine.AffSpanSet
     dsimp [C]
-    rw [h_affineSpan]
-    rfl
+    exact congrArg (fun A : AffineSubspace F (ι → F) => (A : Set (ι → F))) h_affineSpan
   have hUS : (U : Set (ι → F)) = (S : Set (ι → F)) := by
     have hScoe : (S : Set (ι → F)) = Affine.AffSpanSet (U := C 0) := by
       dsimp [S, Affine.AffSpanFinset]
       -- coercion of `toFinset` gives back the set
       simp
-    simpa [h_AffSpanSet] using hScoe.symm
+    exact h_AffSpanSet.symm.trans hScoe.symm
   -- Build an equivalence between U and S (identity on the underlying word)
   let eUS : U ≃ S :=
     { toFun := fun x =>
@@ -345,7 +346,8 @@ theorem reedSolomon_dim_le_deg {ι : Type} [Nonempty ι]
     simpa using
       (Submodule.finrank_map_le (f := ReedSolomon.evalOnPoints (F := F) domain)
         (p := Polynomial.degreeLT F deg))
-  simpa [Polynomial.finrank_degreeLT_n] using hle
+  rw [Polynomial.finrank_degreeLT_n] at hle
+  exact hle
 
 theorem reedSolomon_rate_le_one {ι : Type} [Fintype ι] [Nonempty ι]
     {F : Type} [Field F]
@@ -830,11 +832,11 @@ theorem concentration_bounds {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq
     intro u
     simpa [δ'] using (hpred (u : ι → F) u.property)
   -- Cast lemmas from ℚ≥0 to ENNReal via NNReal
-  have cast_ennreal_eq_iff (p q : ℚ≥0) : ((p : ENNReal) = (q : ENNReal)) ↔ p = q := by
-    change (((p : ℝ≥0) : ENNReal) = ((q : ℝ≥0) : ENNReal)) ↔ p = q
+  have cast_ennreal_eq_iff (p q : ℚ≥0) :
+      (((p : ℝ≥0) : ENNReal) = ((q : ℝ≥0) : ENNReal)) ↔ p = q := by
     simp [ENNReal.coe_inj]
-  have cast_ennreal_le_iff (p q : ℚ≥0) : ((p : ENNReal) ≤ (q : ENNReal)) ↔ p ≤ q := by
-    change (((p : ℝ≥0) : ENNReal) ≤ ((q : ℝ≥0) : ENNReal)) ↔ p ≤ q
+  have cast_ennreal_le_iff (p q : ℚ≥0) :
+      (((p : ℝ≥0) : ENNReal) ≤ ((q : ℝ≥0) : ENNReal)) ↔ p ≤ q := by
     simp [ENNReal.coe_le_coe]
   -- Bridge between ENNReal relative distance and the computable ℚ≥0 version
   have hbridge : ∀ u : ι → F, Code.relDistFromCode u V = (δᵣ'(u, V) : ENNReal) := by
@@ -848,7 +850,8 @@ theorem concentration_bounds {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq
     set p : ℚ≥0 := δᵣ'((u : ι → F), V)
     have hs : p ≠ δ' ↔ p ≤ δ := by
       simpa [p] using (hpredU u)
-    have hcast : ((p : ENNReal) ≠ (δ' : ENNReal)) ↔ ((p : ENNReal) ≤ (δ : ENNReal)) := by
+    have hcast : (((p : ℝ≥0) : ENNReal) ≠ ((δ' : ℝ≥0) : ENNReal)) ↔
+        (((p : ℝ≥0) : ENNReal) ≤ ((δ : ℝ≥0) : ENNReal)) := by
       constructor
       · intro hne_cast
         have hne : p ≠ δ' := by
@@ -863,7 +866,10 @@ theorem concentration_bounds {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq
         intro hEqCast
         have hEq : p = δ' := (cast_ennreal_eq_iff p δ').1 hEqCast
         exact hne hEq
-    simpa [hbridge (u := (u : ι → F)), p] using hcast
+    rw [hbridge (u := (u : ι → F))]
+    change (((p : ℝ≥0) : ENNReal) ≠ ((δ' : ℝ≥0) : ENNReal)) ↔
+      (((p : ℝ≥0) : ENNReal) ≤ ((δ : ℝ≥0) : ENNReal))
+    exact hcast
   -- Turn the pointwise iff into an equality of probabilities
   have hPr_eq :
       Pr_{let u ← $ᵖ U}[Code.relDistFromCode u V ≠ (δ' : ENNReal)] =
@@ -891,8 +897,10 @@ theorem concentration_bounds {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq
     have hle_umax : Code.relDistFromCode u_max_sub V ≤ (δ : ℝ≥0) := hall u_max_sub
     have hnot_le : ¬ Code.relDistFromCode u_max_sub V ≤ (δ : ℝ≥0) := by
       intro hle
-      have hle' : (δᵣ'(u_max, V) : ENNReal) ≤ (δ : ENNReal) := by
-        simpa [u_max_sub, hbridge (u := u_max)] using hle
+      have hle' : ((δᵣ'(u_max, V) : ℝ≥0) : ENNReal) ≤ ((δ : ℝ≥0) : ENNReal) := by
+        rw [hbridge] at hle
+        change ((δᵣ'(u_max, V) : ℝ≥0) : ENNReal) ≤ ((δ : ℝ≥0) : ENNReal) at hle
+        exact hle
       have hle_q : δᵣ'(u_max, V) ≤ δ := (cast_ennreal_le_iff (δᵣ'(u_max, V)) δ).1 hle'
       have hδ_lt_umax : δ < δᵣ'(u_max, V) := by simpa [hu_max_eq] using hδlt'
       exact (not_le_of_gt hδ_lt_umax) hle_q