chore: bump to v4.3.0-rc2 (#8366)

# PR contents

This is the supremum of

- #8284
- #8056
- #8023
- #8332
- #8226 (already approved)
- #7834 (already approved)

along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it.

Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380.

I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime.

# Lean PRs involved in this bump

In particular this includes adjustments for the Lean PRs

* leanprover/lean4#2778 
* leanprover/lean4#2790
* leanprover/lean4#2783
* leanprover/lean4#2825
* leanprover/lean4#2722

## leanprover/lean4#2778

We can get rid of all the 
```
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
```
macros across Mathlib (and in any projects that want to write natural number powers of reals).

## leanprover/lean4#2722

Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. 

## leanprover/lean4#2783

This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes:
* switching to using explicit lemmas that have the intended level of application
* `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour
* Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`.

This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes!



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mauricio Collares <mauricio@collares.org>

.gitignore

@@ -2,10 +2,10 @@
 .DS_Store
 # Created by `lake exe cache get` if no home directory is available
 /.cache
-# Prior to https://github.com/leanprover/lean4/pull/2749 lake stored files in these locations.
+# Prior to v4.3.0-rc2 lake stored files in these locations.
 # We'll leave them in the `.gitignore` for a while for users switching between toolchains.
 /build/
 /lake-packages/
 /lakefile.olean
-# After https://github.com/leanprover/lean4/pull/2749 lake stores its files here:
+# After v4.3.0-rc2 lake stores its files here:
 /.lake/

Archive/Examples/IfNormalization/Result.lean

@@ -29,20 +29,13 @@ attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjo
 /-!
 Adding these lemmas to the simp set allows Lean to handle the termination proof automatically.
 -/
-attribute [local simp] Nat.lt_add_one_iff le_add_of_le_right
+attribute [local simp] Nat.lt_add_one_iff le_add_of_le_right max_add_add_right max_mul_mul_left
 
 /-!
 Some further simp lemmas for handling if-then-else statements.
 -/
 attribute [local simp] apply_ite ite_eq_iff'
 
--- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
--- rather than finding it by typeclass search.
--- See https://github.com/leanprover/lean4/pull/2816
-@[simp] theorem decide_eq_true_eq {i : Decidable p} : (@decide p i = true) = p :=
-  _root_.decide_eq_true_eq
-
-
 /-!
 Simp lemmas for `eval`.
 We don't want a `simp` lemma for `(ite i t e).eval` in general, only once we know the shape of `i`.

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -22,12 +22,6 @@ namespace IfExpr
 attribute [local simp] eval normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
   List.disjoint max_add_add_right max_mul_mul_left Nat.lt_add_one_iff le_add_of_le_right
 
--- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
--- rather than finding it by typeclass search.
--- See https://github.com/leanprover/lean4/pull/2816
-@[simp] theorem decide_eq_true_eq' {i : Decidable p} : (@decide p i = true) = p :=
-  _root_.decide_eq_true_eq
-
 theorem eval_ite_ite' :
     (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
   cases h : eval f a <;> simp_all
@@ -106,8 +100,8 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
             simp_all
           · simp_all? says simp_all only [ne_eq, hasNestedIf, Bool.or_self, hasConstantIf,
               and_self, hasRedundantIf, Bool.or_false, beq_eq_false_iff_ne, not_false_eq_true,
-              disjoint, List.disjoint, Bool.and_true, Bool.and_eq_true, decide_eq_true_eq',
-              true_and]
+              disjoint, List.disjoint, decide_not, Bool.and_true, Bool.and_eq_true,
+              Bool.not_eq_true', decide_eq_false_iff_not, true_and]
             constructor <;> assumption
         · have := ht₃ w
           have := he₃ w

Archive/Imo/Imo1960Q1.lean

@@ -95,7 +95,12 @@ theorem right_direction {n : ℕ} : ProblemPredicate n → SolutionPredicate n :
   have := searchUpTo_start
   iterate 82
     replace :=
-      searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num)
+      searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) (by norm_num1; rfl)
+        (by -- This used to be just `norm_num`, but after leanprover/lean4#2790,
+            -- that triggers a max recursion depth exception. As a workaround, we
+            -- manually rewrite with `Nat.digits_of_two_le_of_pos` first.
+            rw [Nat.digits_of_two_le_of_pos (by norm_num) (by norm_num)]
+            norm_num <;> decide)
   exact searchUpTo_end this
 #align imo1960_q1.right_direction Imo1960Q1.right_direction
 

Archive/Imo/Imo1962Q1.lean

@@ -131,7 +131,18 @@ Now we combine these cases to show that 153846 is the smallest solution.
 
 
 theorem satisfied_by_153846 : ProblemPredicate 153846 := by
-  norm_num [ProblemPredicate]
+  -- This proof used to be the single line `norm_num [ProblemPredicate]`.
+  -- After leanprover/lean4#2790, that triggers a max recursion depth exception.
+  -- As a workaround, we manually apply `Nat.digits_of_two_le_of_pos` a few times
+  -- before invoking `norm_num`.
+  unfold ProblemPredicate
+  have two_le_ten : 2 ≤ 10 := by norm_num
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  rw [Nat.digits_of_two_le_of_pos two_le_ten (by norm_num)]
+  norm_num
+  decide
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
 
 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by

Archive/Imo/Imo1962Q4.lean

@@ -17,8 +17,6 @@ Since Lean does not have a concept of "simplest form", we just express what is
 in fact the simplest form of the set of solutions, and then prove it equals the set of solutions.
 -/
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
-
 open Real
 
 open scoped Real

Archive/Imo/Imo1964Q1.lean

@@ -34,7 +34,7 @@ theorem two_pow_mod_seven (n : ℕ) : 2 ^ n ≡ 2 ^ (n % 3) [MOD 7] :=
   let t := n % 3
   calc 2 ^ n = 2 ^ (3 * (n / 3) + t) := by rw [Nat.div_add_mod]
     _ = (2 ^ 3) ^ (n / 3) * 2 ^ t := by rw [pow_add, pow_mul]
-    _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; norm_num
+    _ ≡ 1 ^ (n / 3) * 2 ^ t [MOD 7] := by gcongr; decide
     _ = 2 ^ t := by ring
 
 /-!
@@ -68,5 +68,5 @@ theorem imo1964_q1b (n : ℕ) : ¬7 ∣ 2 ^ n + 1 := by
   have H : 2 ^ t + 1 ≡ 0 [MOD 7]
   · calc 2 ^ t + 1 ≡ 2 ^ n + 1 [MOD 7 ] := by gcongr ?_ + 1; exact (two_pow_mod_seven n).symm
       _ ≡ 0 [MOD 7] := h.modEq_zero_nat
-  interval_cases t <;> norm_num at H
+  interval_cases t <;> contradiction
 #align imo1964_q1b imo1964_q1b

Archive/Imo/Imo1981Q3.lean

@@ -129,7 +129,7 @@ theorem imp_fib {n : ℕ} : ∀ m : ℕ, NatPredicate N m n → ∃ k : ℕ, m =
   obtain (rfl : 1 = n) | (h4 : 1 < n) := (succ_le_iff.mpr h2.n_pos).eq_or_lt
   · use 1
     have h5 : 1 ≤ m := succ_le_iff.mpr h2.m_pos
-    simpa [fib_one, fib_two] using (h3.antisymm h5 : m = 1)
+    simpa [fib_one, fib_two, (by decide : 1 + 1 = 2)] using (h3.antisymm h5 : m = 1)
   · obtain (rfl : m = n) | (h6 : m < n) := h3.eq_or_lt
     · exact absurd h2.eq_imp_1 (Nat.ne_of_gt h4)
     · have h7 : NatPredicate N (n - m) m := h2.reduction h4
@@ -205,5 +205,7 @@ theorem imo1981_q3 : IsGreatest (specifiedSet 1981) 3524578 := by
   have := fun h => @solution_greatest 1981 16 h 3524578
   norm_num at this
   apply this
-  norm_num [ProblemPredicate_iff]
+  · decide
+  · decide
+  · norm_num [ProblemPredicate_iff]; decide
 #align imo1981_q3 imo1981_q3

Archive/Imo/Imo2001Q2.lean

@@ -32,8 +32,6 @@ open Real
 
 variable {a b c : ℝ}
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
-
 namespace Imo2001Q2
 
 theorem bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :

Archive/Imo/Imo2005Q4.lean

@@ -29,7 +29,7 @@ def a (n : ℕ) : ℤ :=
 theorem find_specified_factor {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hp3 : p ≠ 3) :
     ↑p ∣ a (p - 2) := by
   -- Since `p` is neither `2` nor `3`, it is coprime with `2`, `3`, and `6`
-  rw [Ne.def, ← Nat.prime_dvd_prime_iff_eq hp (by norm_num), ← Nat.Prime.coprime_iff_not_dvd hp]
+  rw [Ne.def, ← Nat.prime_dvd_prime_iff_eq hp (by decide), ← Nat.Prime.coprime_iff_not_dvd hp]
     at hp2 hp3
   have : Int.gcd p 6 = 1 := Nat.coprime_mul_iff_right.2 ⟨hp2, hp3⟩
   -- Nat arithmetic needed to deal with powers
@@ -71,10 +71,10 @@ theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → IsCoprime
   -- For `p = 2` and `p = 3`, take `n = 1` and `n = 2`, respectively
   by_cases hp2 : p = 2
   · rw [hp2] at h
-    apply h 1 <;> norm_num
+    apply h 1 <;> decide
   by_cases hp3 : p = 3
   · rw [hp3] at h
-    apply h 2 <;> norm_num
+    apply h 2 <;> decide
   -- Otherwise, take `n = p - 2`
   refine h (p - 2) ?_ (find_specified_factor hp hp2 hp3)
   calc

Archive/Imo/Imo2008Q3.lean

@@ -31,8 +31,6 @@ Then `p = 2n + k ≥ 2n + √(p - 4) = 2n + √(2n + k - 4) > √(2n)` and we ar
 
 open Real
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
-
 namespace Imo2008Q3
 
 theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) :

Archive/Imo/Imo2013Q5.lean

@@ -31,8 +31,6 @@ https://www.imo-official.org/problems/IMO2013SL.pdf
 
 open scoped BigOperators
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
-
 namespace Imo2013Q5
 
 theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)

Archive/Imo/Imo2019Q1.lean

@@ -27,7 +27,7 @@ theorem imo2019_q1 (f : ℤ → ℤ) :
     (∀ a b : ℤ, f (2 * a) + 2 * f b = f (f (a + b))) ↔ f = 0 ∨ ∃ c, f = fun x => 2 * x + c := by
   constructor; swap
   -- easy way: f(x)=0 and f(x)=2x+c work.
-  · rintro (rfl | ⟨c, rfl⟩) <;> intros <;> simp only [Pi.zero_apply]; ring
+  · rintro (rfl | ⟨c, rfl⟩) <;> intros <;> norm_num; ring
   -- hard way.
   intro hf
   -- functional equation

Archive/Imo/Imo2019Q2.lean

@@ -442,7 +442,7 @@ theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set P
   have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
     refine' cfg.triangleABC.circumsphere.cospherical.subset _
     simp only [Set.insert_subset_iff, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere,
-      cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff]
+      cfg.A₂_mem_circumsphere, Sphere.mem_coe, Set.singleton_subset_iff, and_true]
   exact h.affineIndependent_of_ne cfg.A_ne_B.symm cfg.A₂_ne_B.symm cfg.A₂_ne_A.symm
 #align imo2019_q2.imo2019q2_cfg.not_collinear_QPA₂ Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂
 

Archive/Imo/Imo2019Q4.lean

@@ -29,8 +29,6 @@ individually.
 
 open scoped Nat BigOperators
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
-
 open Nat hiding zero_le Prime
 
 open Finset multiplicity
@@ -65,7 +63,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
     _ ≤ k ! := by gcongr
   clear h h2
   induction' n, hn using Nat.le_induction with n' hn' IH
-  · norm_num
+  · decide
   let A := ∑ i in range n', i
   have le_sum : ∑ i in range 6, i ≤ A
   · apply sum_le_sum_of_subset
@@ -87,8 +85,7 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
   -- The implication `←` holds.
   constructor
   swap
-  · rintro (h | h) <;> simp [Prod.ext_iff] at h <;> rcases h with ⟨rfl, rfl⟩ <;>
-    norm_num [prod_range_succ, succ_mul]
+  · rintro (h | h) <;> simp [Prod.ext_iff] at h <;> rcases h with ⟨rfl, rfl⟩ <;> decide
   intro h
   -- We know that n < 6.
   have := Imo2019Q4.upper_bound hk h
@@ -101,9 +98,9 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
     exact h; rw [h]; norm_num
   all_goals exfalso; norm_num [prod_range_succ] at h; norm_cast at h
   -- n = 3
-  · refine' monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h <;> norm_num
+  · refine' monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h <;> decide
   -- n = 4
-  · refine' monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h <;> norm_num
+  · refine' monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h <;> decide
   -- n = 5
-  · refine' monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h <;> norm_num
+  · refine' monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h <;> decide
 #align imo2019_q4 imo2019_q4

Archive/MiuLanguage/DecisionNec.lean

@@ -61,7 +61,7 @@ theorem mod3_eq_1_or_mod3_eq_2 {a b : ℕ} (h1 : a % 3 = 1 ∨ a % 3 = 2)
   · rw [h2]; exact h1
   · cases' h1 with h1 h1
     · right; simp [h2, mul_mod, h1, Nat.succ_lt_succ]
-    · left; simp [h2, mul_mod, h1]
+    · left; simp only [h2, mul_mod, h1, mod_mod]; decide
 #align miu.mod3_eq_1_or_mod3_eq_2 Miu.mod3_eq_1_or_mod3_eq_2
 
 /-- `count_equiv_one_or_two_mod3_of_derivable` shows any derivable string must have a `count I` that
@@ -80,7 +80,7 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) :
     simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right]
     simp
   · left; rw [count_append, count_append, count_append]
-    simp only [ne_eq, count_cons_of_ne, count_nil, add_zero]
+    simp only [ne_eq, not_false_eq_true, count_cons_of_ne, count_nil, add_zero]
 #align miu.count_equiv_one_or_two_mod3_of_derivable Miu.count_equiv_one_or_two_mod3_of_derivable
 
 /-- Using the above theorem, we solve the MU puzzle, showing that `"MU"` is not derivable.
@@ -134,7 +134,7 @@ theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ ↑[I])) (h₂ : G
     exact mhead
   · change ¬M ∈ tail (xs ++ ↑([I] ++ [U]))
     rw [← append_assoc, tail_append_singleton_of_ne_nil]
-    · simp_rw [mem_append, not_or, and_true]; exact nmtail
+    · simp_rw [mem_append, mem_singleton, or_false]; exact nmtail
     · exact append_ne_nil_of_ne_nil_left _ _ this
 #align miu.goodm_of_rule1 Miu.goodm_of_rule1
 

Archive/MiuLanguage/DecisionSuf.lean

@@ -267,7 +267,7 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count
       · simpa only [count]
       · rw [mem_cons, not_or] at hm; exact hm.2
     · -- case `x = U` gives a contradiction.
-      exfalso; simp only [count, countP_cons_of_pos] at hu
+      exfalso; simp only [count, countP_cons_of_pos (· == U) _ (rfl : U == U)] at hu
       exact succ_ne_zero _ hu
 set_option linter.uppercaseLean3 false in
 #align miu.count_I_eq_length_of_count_U_zero_and_neg_mem Miu.count_I_eq_length_of_count_U_zero_and_neg_mem
@@ -277,7 +277,8 @@ set_option linter.uppercaseLean3 false in
 theorem base_case_suf (en : Miustr) (h : Decstr en) (hu : count U en = 0) : Derivable en := by
   rcases h with ⟨⟨mhead, nmtail⟩, hi⟩
   have : en ≠ nil := by
-    intro k; simp only [k, count, countP, if_false, zero_mod, zero_ne_one, false_or_iff] at hi
+    intro k
+    simp only [k, count, countP, countP.go, if_false, zero_mod, zero_ne_one, false_or_iff] at hi
   rcases exists_cons_of_ne_nil this with ⟨y, ys, rfl⟩
   rcases mhead
   rsuffices ⟨c, rfl, hc⟩ : ∃ c, replicate c I = ys ∧ (c % 3 = 1 ∨ c % 3 = 2)
@@ -331,7 +332,7 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D
     rw [cons_append, cons_append]
     dsimp [tail] at nmtail ⊢
     rw [mem_append] at nmtail
-    simpa only [mem_append, mem_cons, false_or_iff, or_false_iff] using nmtail
+    simpa only [append_assoc, cons_append, nil_append, mem_append, mem_cons, false_or] using nmtail
   · rw [count_append, count_append]; rw [← cons_append, count_append] at hic
     simp only [count_cons_self, count_nil, count_cons, if_false] at hic ⊢
     rw [add_right_comm, add_mod_right]; exact hic

Archive/Sensitivity.lean

@@ -401,7 +401,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   let img := range (g m)
   suffices 0 < dim (W ⊓ img) by
     exact_mod_cast exists_mem_ne_zero_of_rank_pos this
-  have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1) := by
+  have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1 : Cardinal) := by
     convert ← rank_submodule_le (W ⊔ img)
     rw [← Nat.cast_succ]
     apply dim_V

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -31,8 +31,6 @@ namespace AbelRuffini
 
 set_option linter.uppercaseLean3 false
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
-
 open Function Polynomial Polynomial.Gal Ideal
 
 open scoped Polynomial
@@ -94,10 +92,11 @@ theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b)
     rw [mem_span_singleton]
     rw [degree_Phi] at hn; norm_cast at hn
     interval_cases hn : n <;>
-    simp only [Φ, coeff_X_pow, coeff_C, Int.coe_nat_dvd.mpr, hpb, if_true, coeff_C_mul, if_false,
-      coeff_X_zero, hpa, coeff_add, zero_add, mul_zero, coeff_sub, add_zero, zero_sub, dvd_neg,
-      neg_zero, dvd_mul_of_dvd_left]
+    simp (config := {decide := true}) only [Φ, coeff_X_pow, coeff_C, Int.coe_nat_dvd.mpr, hpb,
+      if_true, coeff_C_mul, if_false, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero, coeff_sub,
+      add_zero, zero_sub, dvd_neg, neg_zero, dvd_mul_of_dvd_left]
   · simp only [degree_Phi, ← WithBot.coe_zero, WithBot.coe_lt_coe, Nat.succ_pos']
+    decide
   · rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton]
     exact mt Int.coe_nat_dvd.mp hp2b
   all_goals exact Monic.isPrimitive (monic_Phi a b)
@@ -136,7 +135,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
     have hfa :=
       calc
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
-          norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow]
+          norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow (by decide : Odd 5)]
         _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by
           refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
@@ -163,7 +162,7 @@ theorem complex_roots_Phi (h : (Φ ℚ a b).Separable) : Fintype.card ((Φ ℚ a
 theorem gal_Phi (hab : b < a) (h_irred : Irreducible (Φ ℚ a b)) :
     Bijective (galActionHom (Φ ℚ a b) ℂ) := by
   apply galActionHom_bijective_of_prime_degree' h_irred
-  · norm_num [natDegree_Phi]
+  · simp only [natDegree_Phi]; decide
   · rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff]
     exact (real_roots_Phi_le a b).trans (Nat.le_succ 3)
   · simp_rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff]
@@ -181,7 +180,7 @@ theorem not_solvable_by_rad (p : ℕ) (x : ℂ) (hx : aeval x (Φ ℚ a b) = 0)
 #align abel_ruffini.not_solvable_by_rad AbelRuffini.not_solvable_by_rad
 
 theorem not_solvable_by_rad' (x : ℂ) (hx : aeval x (Φ ℚ 4 2) = 0) : ¬IsSolvableByRad ℚ x := by
-  apply not_solvable_by_rad 4 2 2 x hx <;> norm_num
+  apply not_solvable_by_rad 4 2 2 x hx <;> decide
 #align abel_ruffini.not_solvable_by_rad' AbelRuffini.not_solvable_by_rad'
 
 /-- **Abel-Ruffini Theorem** -/

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -43,9 +43,6 @@ to the n-ball.
 -/
 
 
-
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220
-
 open Set Real MeasureTheory intervalIntegral
 
 open scoped Real NNReal

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -221,7 +221,9 @@ theorem first_vote_pos :
     simp [ENNReal.div_self _ _]
   | 0, q + 1, _ => by
     rw [counted_left_zero, condCount_singleton]
-    simp
+    simp only [List.replicate, Nat.add_eq, add_zero, mem_setOf_eq, List.headI_cons, Nat.cast_zero,
+      ENNReal.zero_div, ite_eq_right_iff]
+    decide
   | p + 1, q + 1, _ => by
     simp_rw [counted_succ_succ]
     rw [← condCount_disjoint_union ((countedSequence_finite _ _).image _)