cleanup

Author: kim-em

Mathlib/Combinatorics/Additive/VerySmallDoubling.lean

@@ -141,31 +141,10 @@ lemma mul_inv_eq_inv_mul_of_doubling_lt_two (h : #(A * A) < 2 * #A) : A * A⁻¹
   simpa using
     mul_inv_eq_inv_mul_of_doubling_lt_two_aux (A := A⁻¹) (by simpa [← mul_inv_rev] using h)
 
--- theorem Nat.cast_rat_nonneg (n : Nat) : 0 ≤ (n : Rat) := Nat.cast_nonneg n
-
--- grind_pattern Nat.cast_rat_nonneg => (n : Rat)
-
--- grind_pattern Nat.cast_nonneg' => (n : α)
-
-section
-open Std Lean.Grind
-attribute [local instance] Semiring.natCast
-
-theorem Nat.cast_nonneg''
-    {α : Type _} [Lean.Grind.Semiring α] [LE α] [LT α] [IsPreorder α] [OrderedRing α]
-    (n : Nat) : 0 ≤ (n : α) :=
-  sorry
-
-grind_pattern Nat.cast_nonneg'' => (n : α)
-
-end
-
-example (p q : Nat) (h : (p : Rat) < 3 / 2 * q) : (p : Rat) < 2 * q := by grind
-
 private lemma weaken_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : #(A * A) < 2 * #A := by
   rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]
-  grind
-#exit
+  linarith
+
 private lemma nonempty_of_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : A.Nonempty := by
   by_contra! rfl
   simp at h