diff --git a/Interval/Fixed.lean b/Interval/Fixed.lean
index 1777572..46b01e4 100644
--- a/Interval/Fixed.lean
+++ b/Interval/Fixed.lean
@@ -902,7 +902,9 @@ lemma Real.cast_natCast (n : ℤ) (n0 : 0 ≤ n) : (n : ℝ) = (n.toNat : ℝ) :
   simp only [Nat.log2_lt n0', ← Nat.cast_lt (α := ℤ), Nat.cast_pow, Nat.cast_two, Nat.cast_natAbs] at nn
   rw [Int64.toInt_ofInt' nn]
 
-@[simp] lemma Fixed.ofInt0_natCast (n : ℕ) : ofInt0 (n : ℤ) = ofNat0 n := by simp [ofInt0, ofNat0]
+@[simp] lemma Fixed.ofInt0_natCast (n : ℕ) : ofInt0 (n : ℤ) = ofNat0 n := by
+  simp [ofInt0, ofNat0]
+  rfl
 
 /-- `Fixed.ofNat0` is conservative -/
 @[approx] lemma Fixed.approx_ofNat0 (n : ℕ) : approx (ofNat0 n) (n : ℝ) := by
diff --git a/Interval/Interval/Mul.lean b/Interval/Interval/Mul.lean
index 8e945e8..a4b6884 100644
--- a/Interval/Interval/Mul.lean
+++ b/Interval/Interval/Mul.lean
@@ -141,7 +141,7 @@ variable {x y : Interval} {x' y' : ℝ}
 
 /-- Multiply two intervals -/
 @[irreducible] def mul (x : Interval) (y : Interval) : Interval :=
-  (x.premul y).mix' (approx_premul x.lo_mem y.lo_mem)
+  (x.premul y).mix' ⟨_, approx_premul x.lo_mem y.lo_mem⟩
 
 /-- `* = mul` -/
 instance : Mul Interval where
diff --git a/Interval/Interval/Preinterval.lean b/Interval/Interval/Preinterval.lean
index e03b80f..99865e6 100644
--- a/Interval/Interval/Preinterval.lean
+++ b/Interval/Interval/Preinterval.lean
@@ -55,8 +55,9 @@ instance : ApproxNan Preinterval ℝ where
   Interval.mix x.lo x.hi le
 
 /-- If a `Preinterval` is nonempty`, it can be turned into an `Interval` -/
-@[irreducible, inline] def mix' (x : Preinterval) {a : ℝ} (m : approx x a) : Interval :=
+@[irreducible, inline] def mix' (x : Preinterval) (m : ∃ a : ℝ, approx x a) : Interval :=
   x.mix (by
+    obtain ⟨a, m⟩ := m
     intro ln hn
     simp only [approx, ln, hn, mem_Icc, false_or] at m
     linarith)
@@ -73,7 +74,7 @@ instance : ApproxNan Preinterval ℝ where
   simp only [approx, ln, hn, or_self, dite_false, false_or, mem_Icc]
 
 /-- `mix'` commutes with `approx` -/
-@[simp] lemma approx_mix' (x : Preinterval) {a b : ℝ} (m : approx x a) :
+@[simp] lemma approx_mix' (x : Preinterval) {b : ℝ} (m : ∃ a : ℝ, approx x a) :
     approx (x.mix' m) b = approx x b := by
   rw [mix', approx_mix]
 
@@ -84,5 +85,5 @@ instance : ApproxNan Preinterval ℝ where
   rw [mix]; simp only [lo_nan, hi_nan, Interval.mix_self, Interval.coe_nan]
 
 /-- `mix'` propagates `nan` -/
-@[simp] lemma mix_nan' {a : ℝ} (m : approx (nan : Preinterval) a) : mix' nan m = nan := by
+@[simp] lemma mix_nan' (m : ∃ a : ℝ, approx (nan : Preinterval) a) : mix' nan m = nan := by
   rw [mix', mix_nan]