Merge branch 'MR-manifolds-boundary' into integral_curve

Author: grunweg

.github/workflows/bors.yml

@@ -125,10 +125,10 @@ jobs:
       - name: cleanup
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
-          # Delete all but the 10 most recent toolchains.
+          # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
-          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +11 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
+          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
@@ -242,14 +242,18 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
 
       - name: check environments using lean4checker
         id: lean4checker

.github/workflows/build.yml

@@ -132,10 +132,10 @@ jobs:
       - name: cleanup
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
-          # Delete all but the 10 most recent toolchains.
+          # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
-          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +11 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
+          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
@@ -249,14 +249,18 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
 
       - name: check environments using lean4checker
         id: lean4checker

.github/workflows/build.yml.in

@@ -111,10 +111,10 @@ jobs:
       - name: cleanup
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
-          # Delete all but the 10 most recent toolchains.
+          # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
-          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +11 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
+          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
@@ -228,14 +228,18 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
 
       - name: check environments using lean4checker
         id: lean4checker

.github/workflows/build_fork.yml

@@ -129,10 +129,10 @@ jobs:
       - name: cleanup
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
-          # Delete all but the 10 most recent toolchains.
+          # Delete all but the 5 most recent toolchains.
           # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
           # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
-          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +11 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
+          cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
 
       # The Hoskinson runners may not have jq installed, so do that now.
       - name: 'Setup jq'
@@ -246,14 +246,18 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
-          run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
 
       - name: check environments using lean4checker
         id: lean4checker

.vscode/settings.json

@@ -7,5 +7,8 @@
   "files.insertFinalNewline": true,
   "files.trimFinalNewlines": true,
   "files.trimTrailingWhitespace": true,
-  "githubPullRequests.ignoredPullRequestBranches": ["master"]
+  "githubPullRequests.ignoredPullRequestBranches": [
+    "master"
+  ],
+  "git.ignoreLimitWarning": true
 }

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -66,27 +66,27 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
             refine ⟨fun _ => ?_, fun _ => ?_⟩
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
           · simp only [cond_true, h, ht₁]
             refine ⟨fun _ => ?_, fun _ => ?_⟩
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
             · congr
               ext w
-              by_cases w = v <;> rename_i x
+              by_cases h : w = v <;> rename_i x
               · substs h
                 simp_all
               · simp_all
@@ -105,7 +105,7 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
             constructor <;> assumption
         · have := ht₃ w
           have := he₃ w
-          by_cases w = v
+          by_cases h : w = v
           · subst h; simp_all
           · simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
               Bool.not_eq_true', not_false_eq_true, AList.lookup_insert_ne]

Archive/Imo/Imo1981Q3.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Lacker
 -/
 import Mathlib.Data.Int.Lemmas
-import Mathlib.Data.Nat.Fib
+import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.LinearCombination
 
@@ -97,25 +97,25 @@ namespace NatPredicate
 
 variable {N}
 
-nonrec theorem m_le_n {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ n := by exact_mod_cast h1.m_le_n
+nonrec theorem m_le_n {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ n := mod_cast h1.m_le_n
 #align imo1981_q3.nat_predicate.m_le_n Imo1981Q3.NatPredicate.m_le_n
 
-nonrec theorem eq_imp_1 {n : ℕ} (h1 : NatPredicate N n n) : n = 1 := by exact_mod_cast h1.eq_imp_1
+nonrec theorem eq_imp_1 {n : ℕ} (h1 : NatPredicate N n n) : n = 1 := mod_cast h1.eq_imp_1
 #align imo1981_q3.nat_predicate.eq_imp_1 Imo1981Q3.NatPredicate.eq_imp_1
 
 nonrec theorem reduction {m n : ℕ} (h1 : NatPredicate N m n) (h2 : 1 < n) :
     NatPredicate N (n - m) m := by
   have : m ≤ n := h1.m_le_n
-  exact_mod_cast h1.reduction (by exact_mod_cast h2)
+  exact mod_cast h1.reduction (mod_cast h2)
 #align imo1981_q3.nat_predicate.reduction Imo1981Q3.NatPredicate.reduction
 
-theorem n_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < n := by exact_mod_cast h1.n_range.left
+theorem n_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < n := mod_cast h1.n_range.left
 #align imo1981_q3.nat_predicate.n_pos Imo1981Q3.NatPredicate.n_pos
 
-theorem m_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < m := by exact_mod_cast h1.m_range.left
+theorem m_pos {m n : ℕ} (h1 : NatPredicate N m n) : 0 < m := mod_cast h1.m_range.left
 #align imo1981_q3.nat_predicate.m_pos Imo1981Q3.NatPredicate.m_pos
 
-theorem n_le_N {m n : ℕ} (h1 : NatPredicate N m n) : n ≤ N := by exact_mod_cast h1.n_range.right
+theorem n_le_N {m n : ℕ} (h1 : NatPredicate N m n) : n ≤ N := mod_cast h1.n_range.right
 set_option linter.uppercaseLean3 false in
 #align imo1981_q3.nat_predicate.n_le_N Imo1981Q3.NatPredicate.n_le_N
 

Archive/Imo/Imo1987Q1.lean

@@ -25,6 +25,8 @@ holds true for `n = 0` as well, so we first prove it, then deduce the original v
 `n ≥ 1`. -/
 
 
+set_option autoImplicit true
+
 variable (α : Type*) [Fintype α] [DecidableEq α]
 
 open scoped BigOperators Nat

Archive/Imo/Imo1988Q6.lean

@@ -184,7 +184,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   · -- For the second condition, we note that it suffices to check that c ≠ m_x.
     suffices hc : c ≠ mx
     · refine' lt_of_le_of_ne _ hc
-      exact_mod_cast c_lt
+      exact mod_cast c_lt
     -- However, recall that B(m_x) ≠ m_x + m_y.
     -- If c = m_x, we can prove B(m_x) = m_x + m_y.
     contrapose! hm_B₂
@@ -237,14 +237,14 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
     · have hpos : z * z + x * x > 0 := by
         apply add_pos_of_nonneg_of_pos
         · apply mul_self_nonneg
-        · apply mul_pos <;> exact_mod_cast hx
+        · apply mul_pos <;> exact mod_cast hx
       have hzx : z * z + x * x = (z * x + 1) * k := by
         rw [← sub_eq_zero, ← h_root]
         ring
       rw [hzx] at hpos
       replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.ofNat_zero_le k)
       replace hpos : z * x ≥ 0 := Int.le_of_lt_add_one hpos
-      apply nonneg_of_mul_nonneg_left hpos (by exact_mod_cast hx)
+      apply nonneg_of_mul_nonneg_left hpos (mod_cast hx)
     · contrapose! hV₀ with x_lt_z
       apply ne_of_gt
       calc
@@ -284,7 +284,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
   · -- Show the descent step.
     intro x y _ hx h_base _ z _ _ hV₀
     constructor
-    · have zy_pos : z * y ≥ 0 := by rw [hV₀]; exact_mod_cast Nat.zero_le _
+    · have zy_pos : z * y ≥ 0 := by rw [hV₀]; exact mod_cast Nat.zero_le _
       apply nonneg_of_mul_nonneg_left zy_pos
       linarith
     · contrapose! hV₀ with x_lt_z

Archive/Imo/Imo1994Q1.lean

@@ -89,11 +89,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
     simp only [mem_map, mem_Icc, mem_Ioc, Fin.zero_le, true_and_iff, Equiv.subLeft_apply,
       Function.Embedding.coeFn_mk, exists_prop, RelEmbedding.coe_toEmbedding] at hx ⊢
     rcases hx with ⟨i, ⟨hi, rfl⟩⟩
-    have h1 : a i + a (Fin.last m - k) ≤ n := by
-      -- Porting note: Original proof was `by linarith only [h, a.monotone hi]`
-      have := a.monotone hi
-      simp only at this ⊢
-      linarith only [h, this]
+    have h1 : a i + a (Fin.last m - k) ≤ n := by linarith only [h, a.monotone hi]
     have h2 : a i + a (Fin.last m - k) ∈ A := hadd _ (ha _) _ (ha _) h1
     rw [← mem_coe, ← range_orderEmbOfFin A hm, Set.mem_range] at h2
     cases' h2 with j hj

Archive/Imo/Imo2013Q5.lean

@@ -54,7 +54,7 @@ theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
       _ = x ^ n - y ^ n := geom_sum₂_mul x y n
   -- Choose n larger than 1 / (x - y).
   obtain ⟨N, hN⟩ := exists_nat_gt (1 / (x - y))
-  have hNp : 0 < N := by exact_mod_cast (one_div_pos.mpr hxmy).trans hN
+  have hNp : 0 < N := mod_cast (one_div_pos.mpr hxmy).trans hN
   have :=
     calc
       1 = (x - y) * (1 / (x - y)) := by field_simp
@@ -113,7 +113,7 @@ theorem fx_gt_xm1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 ≤ x)
     (x - 1 : ℝ) < f x := by
   have hx0 :=
     calc
-      (x - 1 : ℝ) < ⌊x⌋₊ := by exact_mod_cast Nat.sub_one_lt_floor x
+      (x - 1 : ℝ) < ⌊x⌋₊ := mod_cast Nat.sub_one_lt_floor x
       _ ≤ f ⌊x⌋₊ := H4 _ (Nat.floor_pos.2 hx)
   obtain h_eq | h_lt := (Nat.floor_le <| zero_le_one.trans hx).eq_or_lt
   · rwa [h_eq] at hx0
@@ -143,12 +143,12 @@ theorem fixed_point_of_pos_nat_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n)
     (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y) (H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n)
     (H5 : ∀ x : ℚ, 1 < x → (x : ℝ) ≤ f x) {a : ℚ} (ha1 : 1 < a) (hae : f a = a) :
     f (a ^ n) = a ^ n := by
-  have hh0 : (a : ℝ) ^ n ≤ f (a ^ n) := by exact_mod_cast H5 (a ^ n) (one_lt_pow ha1 hn.ne')
+  have hh0 : (a : ℝ) ^ n ≤ f (a ^ n) := mod_cast H5 (a ^ n) (one_lt_pow ha1 hn.ne')
   have hh1 :=
     calc
       f (a ^ n) ≤ f a ^ n := pow_f_le_f_pow hn ha1 H1 H4
       _ = (a : ℝ) ^ n := by rw [← hae]
-  exact_mod_cast hh1.antisymm hh0
+  exact mod_cast hh1.antisymm hh0
 #align imo2013_q5.fixed_point_of_pos_nat_pow Imo2013Q5.fixed_point_of_pos_nat_pow
 
 theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
@@ -170,7 +170,7 @@ theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
       _ = f (a ^ N) := by ring_nf
       _ = a ^ N := (fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae)
       _ = x + (a ^ N - x) := by ring
-  have heq := h1.antisymm (by exact_mod_cast h2)
+  have heq := h1.antisymm (mod_cast h2)
   linarith [H5 x hx, H5 _ h_big_enough]
 #align imo2013_q5.fixed_point_of_gt_1 Imo2013Q5.fixed_point_of_gt_1
 
@@ -191,7 +191,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
     calc
       ↑(pn + 2) * f x = (↑pn + 1 + 1) * f x := by norm_cast
       _ = (↑pn + 1) * f x + f x := by ring
-      _ ≤ f (↑pn.succ * x) + f x := by exact_mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
+      _ ≤ f (↑pn.succ * x) + f x := mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
       _ ≤ f ((↑pn + 1) * x + x) := by exact_mod_cast H2 _ _ (mul_pos pn.cast_add_one_pos hx) hx
       _ = f ((↑pn + 1 + 1) * x) := by ring_nf
       _ = f (↑(pn + 2) * x) := by norm_cast
@@ -216,10 +216,10 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
     have hxnm1 : ∀ n : ℕ, 0 < n → (x : ℝ) ^ n - 1 < f x ^ n := by
       intro n hn
       calc
-        (x : ℝ) ^ n - 1 < f (x ^ n) := by
-          exact_mod_cast fx_gt_xm1 (one_le_pow_of_one_le hx.le n) H1 H2 H4
+        (x : ℝ) ^ n - 1 < f (x ^ n) :=
+            mod_cast fx_gt_xm1 (one_le_pow_of_one_le hx.le n) H1 H2 H4
         _ ≤ f x ^ n := pow_f_le_f_pow hn hx H1 H4
-    have hx' : 1 < (x : ℝ) := by exact_mod_cast hx
+    have hx' : 1 < (x : ℝ) := mod_cast hx
     have hxp : 0 < x := by positivity
     exact le_of_all_pow_lt_succ' hx' (f_pos_of_pos hxp H1 H4) hxnm1
   have h_f_commutes_with_pos_nat_mul : ∀ n : ℕ, 0 < n → ∀ x : ℚ, 0 < x → f (n * x) = n * f x := by

Archive/Imo/Imo2020Q2.lean

@@ -31,17 +31,15 @@ theorem imo2020_q2 (a b c d : ℝ) (hd0 : 0 < d) (hdc : d ≤ c) (hcb : c ≤ b)
     (a + 2 * b + 3 * c + 4 * d) * a ^ a * b ^ b * c ^ c * d ^ d =
         (a + 2 * b + 3 * c + 4 * d) * (a ^ a * b ^ b * c ^ c * d ^ d) := by ac_rfl
     _ ≤ (a + 2 * b + 3 * c + 4 * d) * (a * a + b * b + c * c + d * d) := by gcongr; linarith
-    _ = (a + 2 * b + 3 * c + 4 * d) * (a * a) + (a + 2 * b + 3 * c + 4 * d) * (b * b)
-        + (a + 2 * b + 3 * c + 4 * d) * (c * c) + (a + 2 * b + 3 * c + 4 * d) * (d * d) := by ring
-    _ ≤ (a + 3 * b + 3 * c + 3 * d) * (a * a) + (3 * a + b + 3 * c + 3 * d) * (b * b)
-        + (3 * a + 3 * b + c + 3 * d) * (c * c) + (3 * a + 3 * b + 3 * c + d) * (d * d) := by
-        -- Porting note: after #2220 is fixed we can change all `a * a` to `a ^ 2` and automation
-        -- will work better
-        gcongr ?_ * _ + ?_ * _ + ?_ * _ + ?_ * _ <;> (try linarith) <;> apply mul_self_nonneg
-    _ < (a + 3 * b + 3 * c + 3 * d) * (a * a) + (3 * a + b + 3 * c + 3 * d) * (b * b)
-        + (3 * a + 3 * b + c + 3 * d) * (c * c) + (3 * a + 3 * b + 3 * c + d) * (d * d)
+    _ = (a + 2 * b + 3 * c + 4 * d) * a ^ 2 + (a + 2 * b + 3 * c + 4 * d) * b ^ 2
+        + (a + 2 * b + 3 * c + 4 * d) * c ^ 2 + (a + 2 * b + 3 * c + 4 * d) * d ^ 2 := by ring
+    _ ≤ (a + 3 * b + 3 * c + 3 * d) * a ^ 2 + (3 * a + b + 3 * c + 3 * d) * b ^ 2
+        + (3 * a + 3 * b + c + 3 * d) * c ^ 2 + (3 * a + 3 * b + 3 * c + d) * d ^ 2 := by
+        gcongr ?_ * _ + ?_ * _ + ?_ * _ + ?_ * _ <;> linarith
+    _ < (a + 3 * b + 3 * c + 3 * d) * a ^ 2 + (3 * a + b + 3 * c + 3 * d) * b ^ 2
+        + (3 * a + 3 * b + c + 3 * d) * c ^ 2 + (3 * a + 3 * b + 3 * c + d) * d ^ 2
         + (6 * a * b * c + 6 * a * b * d + 6 * a * c * d + 6 * b * c * d) :=
         (lt_add_of_pos_right _ (by apply_rules [add_pos, mul_pos, zero_lt_one] <;> linarith))
-    _ = HPow.hPow (a + b + c + d) 3 := by ring -- Porting note: See issue #2220
+    _ = (a + b + c + d) ^ 3 := by ring
     _ = 1 := by simp [h1]
 #align imo2020_q2 imo2020_q2

Archive/Sensitivity.lean

@@ -353,7 +353,7 @@ theorem g_injective : Injective (g m) := by
 
 theorem f_image_g (w : V m.succ) (hv : ∃ v, g m v = w) : f m.succ w = √ (m + 1) • w := by
   rcases hv with ⟨v, rfl⟩
-  have : √ (m + 1) * √ (m + 1) = m + 1 := Real.mul_self_sqrt (by exact_mod_cast zero_le _)
+  have : √ (m + 1) * √ (m + 1) = m + 1 := Real.mul_self_sqrt (mod_cast zero_le _)
   rw [f_succ_apply, g_apply]
   simp [this, f_squared, smul_add, add_smul, smul_smul, V]
   abel
@@ -400,7 +400,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   let W := Span (e '' H)
   let img := range (g m)
   suffices 0 < dim (W ⊓ img) by
-    exact_mod_cast exists_mem_ne_zero_of_rank_pos this
+    exact mod_cast exists_mem_ne_zero_of_rank_pos this
   have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1 : Cardinal) := by
     convert ← rank_submodule_le (W ⊔ img)
     rw [← Nat.cast_succ]