Update Dual.lean

fpvandoorn · Jul 22, 2024 · 01a2162 · 01a2162
1 parent 4f64a7a
commit 01a2162
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean
@@ -523,8 +523,7 @@ theorem int_conj_q_lt_top'_mul_self (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ}
     rw [mul_assoc, mul_comm, mul_assoc]
     congr
     rfl
-    rw [Real.self_mul_sign]
-    rw [←nnnorm_toReal_eq_abs]
+    rw [Real.self_mul_sign, ← nnnorm_toReal_eq_abs]
     rfl
 
   sorry