feat: replace some tauto with grind

Author: kim-em

Archive/Examples/Kuratowski.lean

@@ -101,7 +101,7 @@ theorem nodup_theClosedSix_theFourteen_iff : (theClosedSix s).Nodup ↔ TheSixIn
   -- The goal becomes 6 inequalities ↔ 15 inequalities.
   constructor -- Show both implications.
   · -- One implication is almost trivial as the six inequalities are among the fifteen.
-    tauto
+    grind
   · intro h -- Introduce `TheSixIneq` as an assumption.
     repeat obtain ⟨_, h⟩ := h -- Split the hypothesis into six different inequalities.
     repeat refine .symm (.intro ?_ ?_) -- Split the goal into 15 inequalities.

Archive/Imo/Imo2001Q3.lean

@@ -79,7 +79,7 @@ lemma card_not_easy_le_210 (hG : ∀ i, #(G i) ≤ 6) (hB : ∀ i j, ¬Disjoint
     _ = ∑ i, #({p ∈ G i | ¬Easy B p}.biUnion fun p ↦ {j | p ∈ B j}) := by
       congr!; ext
       simp_rw [mem_biUnion, mem_inter, mem_filter]
-      congr! 2; tauto
+      congr! 2; grind
     _ ≤ ∑ i, ∑ p ∈ G i with ¬Easy B p, #{j | p ∈ B j} := sum_le_sum fun _ _ ↦ card_biUnion_le
     _ ≤ ∑ i, ∑ p ∈ G i with ¬Easy B p, 2 := by
       gcongr with i _ p mp

Counterexamples/Phillips.lean

@@ -287,7 +287,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
     · dsimp
       ext x
       simp only [u, not_exists, mem_iUnion, mem_diff]
-      tauto
+      grind
     · congr 1
       simp only [G, s, Function.iterate_succ', Subtype.coe_mk, union_diff_left, Function.comp]
   have I2 : ∀ n : ℕ, (n : ℝ) * (ε / 2) ≤ f ↑(s n) := by

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -98,7 +98,7 @@ theorem prod_range_div_prod_range {G : Type*} [CommGroup G] {f : ℕ → G} {n m
   congr
   apply Finset.ext
   simp only [mem_Ico, mem_filter, mem_range, *]
-  tauto
+  grind
 
 /-- The two ways of summing over `(i, j)` in the range `a ≤ i ≤ j < b` are equal. -/
 theorem sum_Ico_Ico_comm {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :

Mathlib/Algebra/CubicDiscriminant.lean

@@ -480,7 +480,7 @@ theorem disc_ne_zero_iff_roots_nodup (ha : P.a ≠ 0) (h3 : (map φ P).roots = {
   change _ ↔ (x ::ₘ y ::ₘ {z}).Nodup
   rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]
   simp only [nodup_singleton]
-  tauto
+  grind
 
 theorem card_roots_of_disc_ne_zero [DecidableEq K] (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z})
     (hd : P.disc ≠ 0) : (map φ P).roots.toFinset.card = 3 := by

Mathlib/Algebra/Group/Int/Units.lean

@@ -50,7 +50,7 @@ lemma eq_one_or_neg_one_of_mul_eq_one (h : u * v = 1) : u = 1 ∨ u = -1 :=
 lemma eq_one_or_neg_one_of_mul_eq_one' (h : u * v = 1) : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1 := by
   have h' : v * u = 1 := mul_comm u v ▸ h
   obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h <;>
-      obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h' <;> tauto
+      obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h' <;> grind
 
 lemma eq_of_mul_eq_one (h : u * v = 1) : u = v :=
   (eq_one_or_neg_one_of_mul_eq_one' h).elim

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -400,7 +400,7 @@ theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing :
     NormalizerCondition G ↔ ∀ H : Subgroup G, H.normalizer = H → H = ⊤ := by
   apply forall_congr'; intro H
   simp only [lt_iff_le_and_ne, le_normalizer, le_top, Ne]
-  tauto
+  grind
 
 variable (H)
 

Mathlib/Algebra/Group/Subgroup/Lattice.lean

@@ -185,7 +185,7 @@ theorem nontrivial_iff_ne_bot (H : Subgroup G) : Nontrivial H ↔ H ≠ ⊥ := b
 @[to_additive /-- A subgroup is either the trivial subgroup or nontrivial. -/]
 theorem bot_or_nontrivial (H : Subgroup G) : H = ⊥ ∨ Nontrivial H := by
   have := nontrivial_iff_ne_bot H
-  tauto
+  grind
 
 /-- A subgroup is either the trivial subgroup or contains a non-identity element. -/
 @[to_additive /-- A subgroup is either the trivial subgroup or contains a nonzero element. -/]

Mathlib/Algebra/GroupWithZero/Indicator.lean

@@ -67,7 +67,7 @@ lemma inter_indicator_one : (s ∩ t).indicator (1 : ι → M₀) = s.indicator
 lemma indicator_prod_one {t : Set κ} {j : κ} :
     (s ×ˢ t).indicator (1 : ι × κ → M₀) (i, j) = s.indicator 1 i * t.indicator 1 j := by
   simp_rw [indicator, mem_prod_eq]
-  split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> tauto
+  split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> grind
 
 variable (M₀) [Nontrivial M₀]
 

Mathlib/Algebra/Homology/Double.lean

@@ -205,7 +205,7 @@ noncomputable def evalCompCoyonedaCorepresentable (X : C) (j : ι) :
   · exact evalCompCoyonedaCorepresentableByDoubleId _
       (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _
   · apply evalCompCoyonedaCorepresentableBySingle
-    obtain _ | _ := c.exists_distinct_prev_or j <;> tauto
+    obtain _ | _ := c.exists_distinct_prev_or j <;> grind
 
 instance (X : C) (j : ι) : (eval C c j ⋙ coyoneda.obj (op X)).IsCorepresentable where
   has_corepresentation := ⟨_, ⟨evalCompCoyonedaCorepresentable c X j⟩⟩