fix: Re-enable two extensionality lemmas (#2859)

This fix was found when working on #2850.

A proof in `HasseDeriv` is fixed to deal with the change in `ext` behavior, by undoing some of [the changes made when porting](https://github.com/leanprover-community/mathlib4/pull/2842/files/896482e4b3af25fc5f9dac6705638d02772cb75f..74e7a69f3bebfa75a5fb5ad6ed717a76d3ba3bf3).



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/Module/LinearMap.lean

@@ -493,7 +493,7 @@ theorem toAddMonoidHom_injective :
 #align linear_map.to_add_monoid_hom_injective LinearMap.toAddMonoidHom_injective
 
 /-- If two `σ`-linear maps from `R` are equal on `1`, then they are equal. -/
-@[ext]
+@[ext high]
 theorem ext_ring {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g :=
   ext fun x ↦ by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]
 #align linear_map.ext_ring LinearMap.ext_ring
@@ -502,9 +502,7 @@ theorem ext_ring_iff {σ : R →+* R} {f g : R →ₛₗ[σ] M} : f = g ↔ f 1
   ⟨fun h ↦ h ▸ rfl, ext_ring⟩
 #align linear_map.ext_ring_iff LinearMap.ext_ring_iff
 
--- *TODO*: why are you still timing out?
-set_option maxHeartbeats 300000 in
-@[ext]
+@[ext high]
 theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f (1 : R) = g (1 : R)) :
     f = g :=
   ext fun x ↦ by

Mathlib/Data/Polynomial/HasseDeriv.lean

@@ -167,47 +167,32 @@ theorem factorial_smul_hasseDeriv : ⇑(k ! • @hasseDeriv R _ k) = @derivative
 
 theorem hasseDeriv_comp (k l : ℕ) :
     (@hasseDeriv R _ k).comp (hasseDeriv l) = (k + l).choose k • hasseDeriv (k + l) := by
-  ext i x n
+  ext i : 2
   simp only [LinearMap.smul_apply, comp_apply, LinearMap.coe_comp, smul_monomial, hasseDeriv_apply,
-    mul_one, monomial_eq_zero_iff, sum_monomial_index, MulZeroClass.mul_zero, ←
+    mul_one, monomial_eq_zero_iff, sum_monomial_index, mul_zero, ←
     tsub_add_eq_tsub_tsub, add_comm l k]
   rw_mod_cast [nsmul_eq_mul]
-  congr 1
-  congr 1
+  rw [←Nat.cast_mul]
+  congr 2
   by_cases hikl : i < k + l
-  · rw [choose_eq_zero_of_lt hikl]
+  · rw [choose_eq_zero_of_lt hikl, mul_zero]
     by_cases hil : i < l
-    · rw [choose_eq_zero_of_lt hil]
-      simp
+    · rw [choose_eq_zero_of_lt hil, mul_zero]
     · push_neg at hil
       rw [← tsub_lt_iff_right hil] at hikl
-      rw [choose_eq_zero_of_lt hikl]
-      simp
+      rw [choose_eq_zero_of_lt hikl, zero_mul]
   push_neg at hikl
-  rw [←mul_assoc]
-  rw [←mul_assoc]
-  congr 1
-  norm_cast
-  congr 1
+  apply @cast_injective ℚ
   have h1 : l ≤ i := le_of_add_le_right hikl
   have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
   have h3 : k ≤ k + l := le_self_add
-  apply @cast_injective ℚ
   push_cast
-  rw [cast_choose ℚ h1]
-  rw [cast_choose ℚ h2]
-  rw [cast_choose ℚ h3]
-  rw [cast_choose ℚ hikl]
+  rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]
   rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
   simp only [add_tsub_cancel_left]
   have H : ∀ n : ℕ, (n ! : ℚ) ≠ 0 := by exact_mod_cast factorial_ne_zero
-  have := H (i - l)
-  have := H k
-  have := H (i - l - k)
-  have := H l
-  have := H (k + l)
-  field_simp
-  ring_nf
+  field_simp [H]
+  ring
 #align polynomial.hasse_deriv_comp Polynomial.hasseDeriv_comp
 
 theorem natDegree_hasseDeriv_le (p : R[X]) (n : ℕ) : natDegree (hasseDeriv n p) ≤ natDegree p - n :=