chore: mark neg_div_neg_eq as simp (#9332)

leanprover-community · Jan 8, 2024 · fe5b748 · fe5b748
1 parent 30667e2
commit fe5b748
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean
@@ -118,6 +118,7 @@ theorem neg_div (a b : K) : -b / a = -(b / a) := by
 theorem neg_div' (a b : K) : -(b / a) = -b / a := by simp [neg_div]
 #align neg_div' neg_div'
 
+@[simp]
 theorem neg_div_neg_eq (a b : K) : -a / -b = a / b := by rw [div_neg_eq_neg_div, neg_div, neg_neg]
 #align neg_div_neg_eq neg_div_neg_eq
 

diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean
@@ -100,9 +100,11 @@ theorem jacobiTheta_S_smul (τ : ℍ) :
   rw [mul_comm ((1 : ℂ) / _) _, mul_one_div, eq_div_iff ha', mul_comm _ (_ ^ _), eq_comm] at this
   have expo1 : ∀ n : ℤ, -↑π / (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * (-↑τ)⁻¹ := by
     intro n
-    field_simp [hτ, I_ne_zero]
+    simp only [neg_mul, neg_div_neg_eq, div_mul_eq_mul_div, inv_eq_one_div, mul_div_assoc', mul_one,
+      ne_eq, neg_eq_zero, hτ, not_false_eq_true, eq_div_iff, I_ne_zero,
+      mul_ne_zero, div_eq_iff]
     ring_nf
-    rw [I_sq, mul_neg, mul_one, neg_neg]
+    rw [I_sq, mul_neg, mul_one]
   simp_rw [expo1] at this
   have expo2 : ∀ n : ℤ, -↑π * (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * ↑τ := by
     intro n