chore: remove using clause from convert (leanprover-community#40738)

The new `convert` is less aggressive so in many cases, the `using` clause is not needed anymore. In this PR I manually removed some of these. There are many more left to remove, ideally using some automation.

Author: JovanGerb

Archive/Imo/Imo1959Q2.lean

@@ -60,7 +60,7 @@ theorem sqrt_two_mul_sub_one_le_one : sqrt (2 * x - 1) ≤ 1 ↔ x ≤ 1 := by
 theorem isGood_iff_eq_sqrt_two (hx : x ∈ Icc (1 / 2) 1) : IsGood x A ↔ A = sqrt 2 := by
   have : sqrt (2 * x - 1) ≤ 1 := sqrt_two_mul_sub_one_le_one.2 hx.2
   simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
-  suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert! this using 2; ring
+  suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this; ring
   rw [← div_eq_iff, div_sqrt, eq_comm]
   positivity
 

Archive/Imo/Imo2024Q3.lean

@@ -938,7 +938,7 @@ lemma exists_a_apply_add_eq : ∃ b c, 0 < c ∧ ∀ n, b < n →
     have := hc.p_pos (N' a N + 2 * (b + 2))
     rcases hc.even_p (by lia) (hs (b + 2)) with ⟨_, _⟩
     lia
-  · convert! hc.apply_add_p_eq (by lia) (hs n) using 3
+  · convert hc.apply_add_p_eq (by lia) (hs n)
     rcases hc.even_p (by lia) (hs n) with ⟨_, ht⟩
     simp [ht, ← two_mul]
 
@@ -949,8 +949,8 @@ theorem result {a : ℕ → ℕ} {N : ℕ} (h : Condition a N) :
   obtain ⟨b, c, hc, hbc⟩ := h.exists_a_apply_add_eq a N
   obtain ⟨t, _⟩ | ⟨t, _⟩ := Nat.even_or_odd (Condition.N' a N)
   · refine .inl ⟨c, Condition.N' a N / 2 + b + 1, hc, fun m hm ↦ ?_⟩
-    convert! hbc (m - t) (by lia) using 1 <;> dsimp only <;> congr <;> lia
+    convert hbc (m - t) (by lia) <;> lia
   · refine .inr ⟨c, Condition.N' a N / 2 + b + 1, hc, fun m hm ↦ ?_⟩
-    convert! hbc (m - t) (by lia) using 1 <;> dsimp only <;> congr 1 <;> lia
+    convert hbc (m - t) (by lia) using 2 <;> lia
 
 end Imo2024Q3

Archive/Imo/Imo2024Q6.lean

@@ -57,7 +57,7 @@ lemma Aquaesulian.injective : Function.Injective f := by
 
 lemma Aquaesulian.apply_zero : f 0 = 0 := by
   refine h.injective ?_
-  convert! h.apply_apply_add 0 using 1 <;> simp
+  convert h.apply_apply_add 0 <;> simp
 
 @[simp]
 lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by
@@ -80,7 +80,7 @@ lemma Aquaesulian.apply_neg_of_apply_eq {x₁ x₂ : G} (hx : f x₁ = x₂) : f
 
 lemma Aquaesulian.apply_neg_eq_neg_iff {x₁ x₂ : G} : f (-x₂) = -x₁ ↔ f x₁ = x₂ := by
   refine ⟨fun hn ↦ ?_, h.apply_neg_of_apply_eq⟩
-  convert! h.apply_neg_of_apply_eq hn <;> rw [neg_neg]
+  convert h.apply_neg_of_apply_eq hn <;> rw [neg_neg]
 
 lemma Aquaesulian.pair_lemma {x u v : G} (huv : u ≠ v) (hx : f x = u ∨ f u = x)
     (hy : f x = v ∨ f v = x) : f x = v ∨ f x = u := by

Archive/MinimalSheffer.lean

@@ -121,7 +121,7 @@ lemma sup_le (h₁ : a ≤ c) (h₂ : b ≤ c) : aᶜ | bᶜ ≤ c := by
   rw [h₂]
   have l1 := (abba (aᶜ | (b | c)) (b | c | c)).symm
   rw [comm _ (aᶜ | _), ← le_def] at l1
-  convert! l1 using 1
+  convert l1
   have l2 := veroff (b | c) c a
   rw [comm _ a, ← h₁, comm, comm _ aᶜ] at l2
   nth_rw 1 [l2, comm (b | c) c, comm b, veroff]

Archive/MiuLanguage/DecisionSuf.lean

@@ -194,7 +194,7 @@ theorem der_replicate_I_of_mod3 (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2) :
       replicate ((2 ^ m - c) / 3) U ++ replicate ((2 ^ m - c) / 3 % 2) U) := by
     apply
       der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append c ((2 ^ m - c) / 3) h
-    convert! hw₂ using 4
+    convert hw₂
     -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m`
     rw [Nat.mul_div_cancel']
     · exact add_tsub_cancel_of_le hm.1
@@ -220,7 +220,7 @@ example (c : ℕ) (h : c % 3 = 1 ∨ c % 3 = 2) : Derivable (M :: replicate c I)
       replicate ((2 ^ m - c) / 3) U ++ replicate ((2 ^ m - c) / 3 % 2) U) := by
     apply
       der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append c ((2 ^ m - c) / 3) h
-    convert! hw₂ using 4
+    convert hw₂
     -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m`
     rw [Nat.mul_div_cancel']
     · exact add_tsub_cancel_of_le hm.1

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -91,7 +91,7 @@ private lemma maxIncSequencesTo_lt {i j : α} (hij : i < j) (hfij : f i < f j) :
     exact (hti.2 hx).trans_lt hij
   refine ⟨insert j t, ?_, ?_, ?_⟩
   next =>
-    convert! hti.insert j using 1
+    convert hti.insert j
     next => simp
     next => rw [max_eq_left hij.le]
   next =>

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -234,7 +234,7 @@ theorem quot_obv : α • x' - β • y' - γ • z' = 0 := by
   dsimp only [gen]
   simp_rw [← map_smul, ← map_sub, ← Submodule.Quotient.mk_smul _ (_ : K),
     ← Submodule.Quotient.mk_sub]
-  convert! LinearMap.map_zero _ using 2
+  convert LinearMap.map_zero _
   rw [Submodule.Quotient.mk_eq_zero]
   simp +decide [sub_zero]
 

Counterexamples/Phillips.lean

@@ -360,7 +360,7 @@ theorem discretePart_apply (f : BoundedAdditiveMeasure α) (s : Set α) :
 theorem continuousPart_apply_eq_zero_of_countable (f : BoundedAdditiveMeasure α) (s : Set α)
     (hs : s.Countable) : f.continuousPart s = 0 := by
   simp only [continuousPart, restrict_apply]
-  convert! f.apply_countable s hs using 2
+  convert f.apply_countable s hs
   ext x
   simp [and_comm]
 

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -97,7 +97,7 @@ theorem zero_divisors_of_torsion {R A} [Nontrivial R] [Ring R] [AddMonoid A] (a
           (nsmul_ne_zero_of_lt_addOrderOf one_ne_zero (Nat.succ_le_iff.mp o2))
       simp only [a0, single_eq_of_ne', Ne, not_false_iff]
     · simpa only [single_eq_same] using zero_ne_one
-  · convert! Commute.geom_sum₂_mul (R := AddMonoidAlgebra R A) _ (addOrderOf a) using 3
+  · convert Commute.geom_sum₂_mul (R := AddMonoidAlgebra R A) _ (addOrderOf a)
     · rw [single_zero_one, one_pow, mul_one]
     · rw [single_pow, one_pow, addOrderOf_nsmul_eq_zero, single_zero_one, one_pow, sub_self]
     · simp only [single_zero_one, Commute.one_right]

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

@@ -156,13 +156,13 @@ def unitsFstOne_mulEquiv_quasiregular : unitsFstOne R A ≃* (PreQuasiregular A)
       { val := 1 + PreQuasiregular.equiv.symm x.val
         inv := 1 + PreQuasiregular.equiv.symm x⁻¹.val
         val_inv := by
-          convert! congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A)) using 1
+          convert congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A))
           · simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
               add_mul, inr_add, inr_mul]
             abel
           · simp only [inr_zero, add_zero]
         inv_val := by
-          convert! congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A)) using 1
+          convert congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A))
           · simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
               add_mul, inr_add, inr_mul]
             abel
@@ -216,8 +216,8 @@ lemma IsQuasiregular.isUnit_one_add {R : Type*} [Semiring R] {x : R} (hx : IsQua
     IsUnit (1 + x) := by
   obtain ⟨y, hy₁, hy₂⟩ := isQuasiregular_iff.mp hx
   refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩
-  · convert! congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]
-  · convert! congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]
+  · convert congr(1 + $(hy₁)) <;> [noncomm_ring; simp]
+  · convert congr(1 + $(hy₂)) <;> [noncomm_ring; simp]
 
 lemma isQuasiregular_iff_isUnit {R : Type*} [Ring R] {x : R} :
     IsQuasiregular x ↔ IsUnit (1 + x) := by
@@ -229,7 +229,7 @@ lemma isQuasiregular_iff_isUnit {R : Type*} [Ring R] {x : R} :
   case' h.right => have := congr($(hx.val_inv_mul) - 1)
   all_goals
     rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this
-    convert! this using 1
+    convert this
     noncomm_ring
 
 -- interestingly, this holds even in the semiring case.