chore(Algebra/Module): golf proofs (leanprover-community#35192)

Author: euprunin

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -402,11 +402,7 @@ lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
   obtain ⟨x, rfl⟩ := hπ x
   rw [← LinearMap.comp_apply, ← LinearMap.comp_apply, mul_smul, LinearMap.smul_comp, ← hi,
     ← LinearMap.comp_smul, LinearMap.comp_assoc, LinearMap.comp_assoc]
-  congr 2
-  convert Submodule.liftQ_mkQ _ _ this using 2
-  ext x
-  apply (LinearMap.quotKerEquivOfSurjective _ hπ).injective
-  simp [LinearMap.quotKerEquivOfSurjective]
+  simp
 
 lemma Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule
     [hM : Module.Finite R M] (g₁ g₂ : M →ₗ[R] N) (h : f.comp g₁ = f.comp g₂) :

Mathlib/Algebra/Module/ZLattice/Summable.lean

@@ -110,23 +110,11 @@ lemma sum_piFinset_Icc_rpow_le {ι : Type*} [Fintype ι] [DecidableEq ι]
     simp [hd, hr'.ne]
   replace hd : 1 ≤ d := by rwa [Nat.one_le_iff_ne_zero]
   have hs0 : s 0 = {0} := by ext; simp [s, funext_iff]
-  have hs {a b : ℕ} (ha : a ≤ b) : s a ⊆ s b := by
-    intros x hx
-    simp only [Fintype.mem_piFinset, s] at hx ⊢
-    exact fun i ↦ Icc_subset_Icc (by simpa) (by simpa) (hx i)
+  have hs {a b : ℕ} (ha : a ≤ b) : s a ⊆ s b := by grind
   have (k : ℕ) : #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1) := by
-    -- We do not yet replace `omega` with `lia` here, as it is measurably slower.
-    trans (2 * k + 3) ^ d - (2 * k + 1) ^ d
-    · simp only [le_add_iff_nonneg_right, zero_le, hs, card_sdiff_of_subset, s]
-      simp only [Fintype.card_piFinset, Int.card_Icc, sub_neg_eq_add, prod_const, card_univ]
-      gcongr <;> norm_cast <;> omega
-    · have := abs_pow_sub_pow_le (α := ℤ) ↑(2 * k + 3) ↑(2 * k + 1) d
-      norm_num at this
-      zify
-      convert this using 3
-      · rw [abs_eq_self.mpr (sub_nonneg.mpr (by gcongr; lia)), Nat.cast_sub (by gcongr; lia)]
-        simp
-      · rw [max_eq_left (by gcongr; lia), abs_eq_self.mpr (by positivity)]
+    simp only [le_add_iff_nonneg_right, zero_le, hs, card_sdiff_of_subset, s, Fintype.card_piFinset,
+      Int.card_Icc, prod_const]
+    grind [abs_pow_sub_pow_le (α := ℤ) (2 * k + 3) (2 * k + 1) d]
   let ε := normBound b
   have hε : 0 < ε := normBound_pos b
   calc ∑ p ∈ s n, ‖∑ i, p i • b i‖ ^ r