apply suggestion

LorenzoLuccioli · Aug 6, 2024 · 1b1f98c · 1b1f98c
1 parent 54ec946
commit 1b1f98c
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean
@@ -969,10 +969,10 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_mutuallySingular [IsFiniteMeasure μ
         · rw [h_top, EReal.top_sub_coe, EReal.toENNReal_top,
             StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop]
           exact hf_cvx'.derivAtTop_eq_top_iff.mp h_top
-        · have ⟨x, hx⟩ := EReal.eq_coe_of_ne_top_of_ne_bot h_top hf_cvx'.derivAtTop_ne_bot
-          rw [hx, StieltjesFunction.measure_Ioi _ ?_ 1 (l := x)]
+        · lift (derivAtTop f) to ℝ using ⟨h_top, hf_cvx'.derivAtTop_ne_bot⟩ with x hx
+          rw [StieltjesFunction.measure_Ioi _ ?_ 1 (l := x)]
           · norm_cast
-          exact (hx ▸ hf_cvx'.tendsto_toReal_derivAtTop h_top :)
+          exact (hx ▸ hf_cvx'.tendsto_toReal_derivAtTop (hx ▸ h_top) :)
   simp_rw [fDiv_of_mutuallySingular h_ms, h1]
   push_cast
   rw [lintegral_statInfoFun_one_zero hf_cvx hf_cont, h2, EReal.coe_toENNReal]

diff --git a/TestingLowerBounds/ForMathlib/EReal.lean b/TestingLowerBounds/ForMathlib/EReal.lean
@@ -288,12 +288,12 @@ lemma toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x
   induction x <;> norm_num
 
 lemma sub_nonneg {x y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) : 0 ≤ x - y ↔ y ≤ x := by
-  obtain ⟨_, ha⟩ := eq_coe_of_ne_top_of_ne_bot hy hy'
-  induction x <;> simp [← EReal.coe_sub, ha]
+  lift y to ℝ using ⟨hy, hy'⟩
+  induction x <;> simp [← EReal.coe_sub]
 
 lemma sub_nonpos {x y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) : x - y ≤ 0 ↔ x ≤ y := by
-  obtain ⟨_, ha⟩ := eq_coe_of_ne_top_of_ne_bot hy hy'
-  induction x <;> simp [← EReal.coe_sub, ha]
+  lift y to ℝ using ⟨hy, hy'⟩
+  induction x <;> simp [← EReal.coe_sub]
 
 @[simp]
 lemma nsmul_eq_mul {n : ℕ} {x : EReal} : n • x = n * x := by