merge leanprover-community#31929

Author: kim-em

Mathlib/Algebra/Polynomial/Reverse.lean

@@ -100,7 +100,7 @@ theorem coeff_reflect (N : ℕ) (f : R[X]) (i : ℕ) : coeff (reflect N f) i = f
   calc
     Finsupp.embDomain (revAt N) f i = Finsupp.embDomain (revAt N) f (revAt N (revAt N i)) := by
       rw [revAt_invol]
-    _ = f (revAt N i) := Finsupp.embDomain_apply _ _ _
+    _ = f (revAt N i) := Finsupp.embDomain_apply_self _ _ _
 
 @[simp]
 theorem reflect_zero {N : ℕ} : reflect N (0 : R[X]) = 0 :=

Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

@@ -140,7 +140,7 @@ lemma star_mem_range_charAlgHom (he : Continuous e) (hL : Continuous fun p : V 
   refine ⟨z.embDomain f, ?_⟩
   ext1 u
   simp only [charAlgHom_apply, Finsupp.support_embDomain, Finset.sum_map,
-    Finsupp.embDomain_apply, star_apply, star_sum, star_mul', Circle.star_addChar]
+    Finsupp.embDomain_apply_self, star_apply, star_sum, star_mul', Circle.star_addChar]
   rw [Finsupp.support_mapRange_of_injective (star_zero _) y star_injective]
   simp [z, f]
 

Mathlib/Data/Finsupp/Basic.lean

@@ -1097,7 +1097,7 @@ theorem subtypeDomain_not_piecewise (f : Subtype P →₀ M) (g : {a // ¬ P a}
   Finsupp.ext fun a => dif_neg a.prop
 
 /-- Extend the domain of a `Finsupp` by using `0` where `P x` does not hold. -/
-@[simps! support toFun]
+@[simps! (attr := grind =) support toFun]
 def extendDomain (f : Subtype P →₀ M) : α →₀ M := piecewise f 0
 
 theorem extendDomain_eq_embDomain_subtype (f : Subtype P →₀ M) :

Mathlib/Data/Finsupp/Defs.lean

@@ -113,7 +113,7 @@ instance instFunLike : FunLike (α →₀ M) α M :=
     ext a
     exact (hf _).trans (hg _).symm⟩
 
-@[ext]
+@[ext, grind ext]
 theorem ext {f g : α →₀ M} (h : ∀ a, f a = g a) : f = g :=
   DFunLike.ext _ _ h
 
@@ -299,7 +299,7 @@ def mapRange (f : M → N) (hf : f 0 = 0) (g : α →₀ M) : α →₀ N :=
   onFinset g.support (f ∘ g) fun a => by
     rw [mem_support_iff, not_imp_not]; exact fun H => (congr_arg f H).trans hf
 
-@[simp]
+@[simp, grind =]
 theorem mapRange_apply {f : M → N} {hf : f 0 = 0} {g : α →₀ M} {a : α} :
     mapRange f hf g a = f (g a) :=
   rfl
@@ -427,7 +427,7 @@ theorem embDomain_apply (f : α ↪ β) (v : α →₀ M) (b : β) :
   -- TODO: investigate why `grind` needs `split_ifs` first; this should never happen.
   split_ifs <;> grind
 
-@[simp]
+@[simp, grind =]
 theorem embDomain_apply_self (f : α ↪ β) (v : α →₀ M) (a : α) : embDomain f v (f a) = v a := by
   classical
     simp_rw [embDomain, coe_mk, mem_map']
@@ -455,12 +455,7 @@ theorem embDomain_eq_zero {f : α ↪ β} {l : α →₀ M} : embDomain f l = 0
   (embDomain_injective f).eq_iff' <| embDomain_zero f
 
 theorem embDomain_mapRange (f : α ↪ β) (g : M → N) (p : α →₀ M) (hg : g 0 = 0) :
-    embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p) := by
-  ext a
-  by_cases h : a ∈ Set.range f
-  · rcases h with ⟨a', rfl⟩
-    rw [mapRange_apply, embDomain_apply_self, embDomain_apply_self, mapRange_apply]
-  · rw [mapRange_apply, embDomain_notin_range, embDomain_notin_range, ← hg] <;> assumption
+    embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p) := by grind
 
 end EmbDomain
 

Mathlib/Data/Finsupp/Option.lean

@@ -110,7 +110,7 @@ theorem sum_option_index_smul [Semiring R] [AddCommMonoid M] [Module R M] (f : O
   f.sum_option_index _ (fun _ => zero_smul _ _) fun _ _ _ => add_smul _ _ _
 
 @[simp] lemma some_embDomain_some [Zero M] (f : α →₀ M) : (f.embDomain .some).some = f := by
-  ext; rw [some_apply]; exact embDomain_apply _ _ _
+  ext; rw [some_apply]; exact embDomain_apply_self _ _ _
 
 @[simp] lemma embDomain_some_none [Zero M] (f : α →₀ M) : f.embDomain .some none = 0 :=
   embDomain_notin_range _ _ _ (by simp)

Mathlib/Data/Finsupp/Single.lean

@@ -60,6 +60,7 @@ def single (a : α) (b : M) : α →₀ M where
       · simp [hb, Pi.single, update]
       simp [ha]
 
+@[grind =]
 theorem single_apply [Decidable (a = a')] : single a b a' = if a = a' then b else 0 := by
   classical
   simp_rw [@eq_comm _ a a', single, coe_mk, Pi.single_apply]
@@ -469,11 +470,7 @@ theorem single_of_embDomain_single (l : α →₀ M) (f : α ↪ β) (a : β) (b
     constructor
     · ext d
       rw [← embDomain_apply_self f l, h]
-      by_cases h_cases : c = d
-      · simp only [Eq.symm h_cases, hc₂, single_eq_same]
-      · rw [single_apply, single_apply, if_neg, if_neg h_cases]
-        by_contra hfd
-        exact h_cases (f.injective (hc₂.trans hfd))
+      grind
     · exact hc₂
 
 @[simp]

Mathlib/Data/List/ToFinsupp.lean

@@ -101,7 +101,7 @@ theorem toFinsupp_append {R : Type*} [AddZeroClass R] (l₁ l₂ : List R)
   | inr h =>
     rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
     rw [getD_append_right _ _ _ _ h, Nat.add_sub_cancel_left, getD_eq_default _ _ h, zero_add]
-    exact Eq.symm (Finsupp.embDomain_apply _ _ _)
+    exact Eq.symm (Finsupp.embDomain_apply_self _ _ _)
 
 theorem toFinsupp_cons_eq_single_add_embDomain {R : Type*} [AddZeroClass R] (x : R) (xs : List R)
     [DecidablePred (getD (x::xs) · 0 ≠ 0)] [DecidablePred (getD xs · 0 ≠ 0)] :

Mathlib/Logic/Embedding/Basic.lean

@@ -114,7 +114,7 @@ theorem coeFn_mk {α β} (f : α → β) (i) : (@mk _ _ f i : α → β) = f :=
 theorem mk_coe {α β : Type*} (f : α ↪ β) (inj) : (⟨f, inj⟩ : α ↪ β) = f :=
   rfl
 
-@[grind! .]
+@[grind! .] -- This adds `Injective f` into the grind context for every embedding `f : α ↪ β`.
 protected theorem injective {α β} (f : α ↪ β) : Injective f :=
   EmbeddingLike.injective f
 
@@ -180,8 +180,7 @@ def setValue {α β : Sort*} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidabl
     [∀ a', Decidable (f a' = b)] : α ↪ β :=
   ⟨fun a' => if a' = a then b else if f a' = b then f a else f a', by
     intro x y h
-    simp only at h
-    split_ifs at h <;> (try subst b) <;> (try simp only [f.injective.eq_iff] at *) <;> grind⟩
+    grind⟩
 
 @[simp]
 theorem setValue_eq {α β} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' = a)]