Merge branch 'master' into rida/ENatTopology

.github/workflows/lean4checker.yml

@@ -69,7 +69,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.9.0
+          git checkout v4.11.0-rc1
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

.github/workflows/nightly_detect_failure.yml

@@ -22,7 +22,7 @@ jobs:
         type: 'stream'
         topic: 'Mathlib status updates'
         content: |
-          ❌ The latest CI for Mathlib's branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
+          ❌ The latest CI for Mathlib's branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
 
   handle_success:
     if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
@@ -50,6 +50,7 @@ jobs:
               git tag "nightly-testing-${version}"
               git push origin "nightly-testing-${version}"
               hash="$(git rev-parse "nightly-testing-${version}")"
+              printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"
               curl -X POST "http://speed.lean-fro.org/mathlib4/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"
           fi
         else
@@ -83,9 +84,15 @@ jobs:
       run: pip install zulip
 
     - name: Check last message and post if necessary
+      env:
+        ZULIP_EMAIL: '[email protected]'
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+        ZULIP_SITE: 'https://leanprover.zulipchat.com'
+        SHA: ${{ env.SHA }}
       run: |
+        import os
         import zulip
-        client = zulip.Client(email='[email protected]', api_key='${{ secrets.ZULIP_API_KEY }}', site='https://leanprover.zulipchat.com')
+        client = zulip.Client(email=os.getenv('ZULIP_EMAIL'), api_key=os.getenv('ZULIP_API_KEY'), site=os.getenv('ZULIP_SITE'))
 
         # Get the last message in the 'status updates' topic
         request = {
@@ -97,20 +104,19 @@ jobs:
         }
         response = client.get_messages(request)
         messages = response['messages']
-        if not messages or messages[0]['content'] != "✅ The latest CI for Mathlib's branch#nightly-testing has succeeded!":
+        if not messages or messages[0]['content'] != f"✅ The latest CI for Mathlib's branch#nightly-testing has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))":
             # Post the success message
             request = {
                 'type': 'stream',
                 'to': 'nightly-testing',
                 'topic': 'Mathlib status updates',
-                'content': "✅ The latest CI for Mathlib's branch#nightly-testing has succeeded!"
+                'content': f"✅ The latest CI for Mathlib's branch#nightly-testing has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
             }
             result = client.send_message(request)
             print(result)
       shell: python
 
     # Next, determine if we should remind the humans to create a new PR to the `bump/v4.X.0` branch.
-    # https://chat.openai.com/share/504882f9-9d98-4d8d-ad19-5161c4a24fe1
 
     - name: Check for matching bump/nightly-YYYY-MM-DD branch
       id: check_branch
@@ -176,16 +182,18 @@ jobs:
       env:
         BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
         BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
+        SHA: ${{ env.SHA }}
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
       shell: python
       run: |
         import os
         import zulip
-        client = zulip.Client(email='[email protected]', api_key='${{ secrets.ZULIP_API_KEY }}', site='https://leanprover.zulipchat.com')
+        client = zulip.Client(email='[email protected]', api_key=os.getenv('ZULIP_API_KEY'), site='https://leanprover.zulipchat.com')
         current_version = os.getenv('NIGHTLY')
         bump_version = os.getenv('BUMP_VERSION')
         bump_branch = os.getenv('BUMP_BRANCH')
-        print(f'Current version: {current_version}, Bump version: {bump_version}')
+        sha = os.getenv('SHA')
+        print(f'Current version: {current_version}, Bump version: {bump_version}, SHA: {sha}')
         if current_version > bump_version:
             print('Lean toolchain in `nightly-testing` is ahead of the bump branch.')
             # Get the last message in the 'Mathlib bump branch reminders' topic
@@ -199,7 +207,7 @@ jobs:
             response = client.get_messages(request)
             messages = response['messages']
             bump_branch_suffix = bump_branch.replace('bump/', '')
-            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing, and then PR that to {bump_branch}. "
+            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
             payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
             payload += f"```bash\n./scripts/create-adaptation-pr.sh {bump_branch_suffix} {current_version}\n```\n"
             # Only post if the message is different

.github/workflows/nolints.yml

@@ -57,7 +57,7 @@ jobs:
         shell: bash
         run: |
           env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --update Mathlib
-          ./scripts/update-style-exceptions.sh
+          lake exe lint-style --update
 
       - name: configure git setup
         run: |

Archive/Hairer.lean

@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2023 Floris Van Doorn. All rights reserved.
+Copyright (c) 2023 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Sébastien Gouëzel, Patrick Massot, Ruben Van de Velde, Floris Van Doorn,
+Authors: Johan Commelin, Sébastien Gouëzel, Patrick Massot, Ruben Van de Velde, Floris van Doorn,
 Junyan Xu
 -/
 import Mathlib.Algebra.MvPolynomial.Funext

Archive/Imo/Imo1975Q1.lean

@@ -25,11 +25,10 @@ by the Rearrangement Inequality
 
 /- Let `n` be a natural number, `x` and `y` be as in the problem statement and `σ` be the
 permutation of natural numbers such that `z = y ∘ σ` -/
-variable (n : ℕ) (σ : Equiv.Perm ℕ) (hσ : {x | σ x ≠ x} ⊆ Finset.Icc 1 n) (x y : ℕ → ℝ)
-variable (hx : AntitoneOn x (Finset.Icc 1 n))
-variable (hy : AntitoneOn y (Finset.Icc 1 n))
+variable (n : ℕ) (σ : Equiv.Perm ℕ) (x y : ℕ → ℝ)
 
-theorem imo1975_q1 :
+theorem imo1975_q1 (hσ : {x | σ x ≠ x} ⊆ Finset.Icc 1 n)
+    (hx : AntitoneOn x (Finset.Icc 1 n)) (hy : AntitoneOn y (Finset.Icc 1 n)) :
     ∑ i ∈ Finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i ∈ Finset.Icc 1 n, (x i - y (σ i)) ^ 2 := by
   simp only [sub_sq, Finset.sum_add_distrib, Finset.sum_sub_distrib]
   -- a finite sum is invariant if we permute the order of summation

Archive/Imo/Imo1981Q3.lean

@@ -130,6 +130,7 @@ satisfying `NatPredicate m n N` are `fib K` and `fib (K+1)`, respectively.
 -/
 variable {K : ℕ} (HK : N < fib K + fib (K + 1)) {N}
 
+include HK in
 theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤ fib (K + 1) := by
   obtain ⟨k : ℕ, hm : m = fib k, hn : n = fib (k + 1)⟩ := h1.imp_fib m
   by_cases h2 : k < K + 1
@@ -156,6 +157,7 @@ theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤
 We spell out the consequences of this result for `specifiedSet N` here.
 -/
 variable {M : ℕ} (HM : M = fib K ^ 2 + fib (K + 1) ^ 2)
+include HK HM
 
 theorem k_bound {m n : ℤ} (h1 : ProblemPredicate N m n) : m ^ 2 + n ^ 2 ≤ M := by
   have h2 : 0 ≤ m := h1.m_range.left.le

Archive/Imo/Imo1986Q5.lean

@@ -38,6 +38,7 @@ structure IsGood (f : ℝ≥0 → ℝ≥0) : Prop where
 namespace IsGood
 
 variable {f : ℝ≥0 → ℝ≥0} (hf : IsGood f) {x y : ℝ≥0}
+include hf
 
 theorem map_add (x y : ℝ≥0) : f (x + y) = f (x * f y) * f y :=
   (hf.map_add_rev x y).symm

Archive/Imo/Imo2008Q3.lean

@@ -43,7 +43,7 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
     simp only [n, Int.natAbs_sq, Int.natCast_pow, Int.ofNat_succ, Int.natCast_dvd_natCast.mp]
     refine (ZMod.intCast_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp ?_
     simp only [m, Int.cast_pow, Int.cast_add, Int.cast_one, ZMod.coe_valMinAbs]
-    rw [pow_two, ← hy]; exact add_left_neg 1
+    rw [pow_two, ← hy]; exact neg_add_cancel 1
   have hnat₂ : n ≤ p / 2 := ZMod.natAbs_valMinAbs_le y
   have hnat₃ : p ≥ 2 * n := by linarith [Nat.div_mul_le_self p 2]
   set k : ℕ := p - 2 * n with hnat₄

Archive/Imo/Imo2019Q2.lean

@@ -66,7 +66,7 @@ attribute [local instance] FiniteDimensional.of_fact_finrank_eq_two
 
 variable (V : Type*) (Pt : Type*)
 variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
-variable [NormedAddTorsor V Pt] [hd2 : Fact (finrank ℝ V = 2)]
+variable [NormedAddTorsor V Pt]
 
 namespace Imo2019Q2
 
@@ -96,7 +96,7 @@ structure Imo2019q2Cfg where
   C_ne_Q₁ : C ≠ Q₁
 
 /-- A default choice of orientation, for lemmas that need to pick one. -/
-def someOrientation : Module.Oriented ℝ V (Fin 2) :=
+def someOrientation [hd2 : Fact (finrank ℝ V = 2)] : Module.Oriented ℝ V (Fin 2) :=
   ⟨Basis.orientation (finBasisOfFinrankEq _ _ hd2.out)⟩
 
 variable {V Pt}
@@ -249,7 +249,7 @@ section Oriented
 
 variable [Module.Oriented ℝ V (Fin 2)]
 
-theorem oangle_CQ₁Q_sign_eq_oangle_CBA_sign :
+theorem oangle_CQ₁Q_sign_eq_oangle_CBA_sign [Fact (finrank ℝ V = 2)] :
     (∡ cfg.C cfg.Q₁ cfg.Q).sign = (∡ cfg.C cfg.B cfg.A).sign := by
   rw [← cfg.sbtw_Q_A₁_Q₁.symm.oangle_eq_right,
     cfg.sOppSide_CB_Q_Q₁.oangle_sign_eq_neg (left_mem_affineSpan_pair ℝ cfg.C cfg.B)
@@ -259,14 +259,18 @@ theorem oangle_CQ₁Q_sign_eq_oangle_CBA_sign :
     cfg.wbtw_B_Q_B₁.oangle_eq_right cfg.Q_ne_B,
     cfg.wbtw_A_B₁_C.symm.oangle_sign_eq_of_ne_left cfg.B cfg.B₁_ne_C.symm]
 
-theorem oangle_CQ₁Q_eq_oangle_CBA : ∡ cfg.C cfg.Q₁ cfg.Q = ∡ cfg.C cfg.B cfg.A :=
+theorem oangle_CQ₁Q_eq_oangle_CBA [Fact (finrank ℝ V = 2)] :
+    ∡ cfg.C cfg.Q₁ cfg.Q = ∡ cfg.C cfg.B cfg.A :=
   oangle_eq_of_angle_eq_of_sign_eq cfg.angle_CQ₁Q_eq_angle_CBA
     cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign
 
 end Oriented
 
 /-! ### More obvious configuration properties -/
 
+section
+
+variable [hd2 : Fact (finrank ℝ V = 2)]
 
 theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by
   intro h
@@ -568,6 +572,8 @@ theorem result : Concyclic ({cfg.P, cfg.Q, cfg.P₁, cfg.Q₁} : Set Pt) := by
   simp only [Set.insert_subset_iff, Set.singleton_subset_iff]
   exact ⟨cfg.P_mem_ω, cfg.Q_mem_ω, cfg.P₁_mem_ω, cfg.Q₁_mem_ω⟩
 
+end
+
 end Imo2019q2Cfg
 
 end
@@ -576,7 +582,7 @@ end Imo2019Q2
 
 open Imo2019Q2
 
-theorem imo2019_q2 (A B C A₁ B₁ P Q P₁ Q₁ : Pt)
+theorem imo2019_q2 [Fact (finrank ℝ V = 2)] (A B C A₁ B₁ P Q P₁ Q₁ : Pt)
     (affine_independent_ABC : AffineIndependent ℝ ![A, B, C]) (wbtw_B_A₁_C : Wbtw ℝ B A₁ C)
     (wbtw_A_B₁_C : Wbtw ℝ A B₁ C) (wbtw_A_P_A₁ : Wbtw ℝ A P A₁) (wbtw_B_Q_B₁ : Wbtw ℝ B Q B₁)
     (PQ_parallel_AB : line[ℝ, P, Q] ∥ line[ℝ, A, B]) (P_ne_Q : P ≠ Q)

Archive/Imo/Imo2024Q1.lean

@@ -60,6 +60,7 @@ lemma condition_toIcoMod_iff {α : ℝ} :
 namespace Condition
 
 variable {α : ℝ} (hc : Condition α)
+include hc
 
 lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
   rcases h with ⟨h0, h2⟩

Archive/Imo/Imo2024Q2.lean

@@ -47,6 +47,9 @@ namespace Condition
 
 variable {a b : ℕ} (h : Condition a b)
 
+section
+include h
+
 lemma a_pos : 0 < a := h.1
 
 lemma b_pos : 0 < b := h.2.1
@@ -79,6 +82,8 @@ lemma dvd_g_of_le_N_of_dvd {n : ℕ} (hn : h.N ≤ n) {d : ℕ} (hab : d ∣ a ^
   rw [← h.gcd_eq_g hn, Nat.dvd_gcd_iff]
   exact ⟨hab, hba⟩
 
+end
+
 lemma a_coprime_ab_add_one : a.Coprime (a * b + 1) := by
   simp
 
@@ -132,7 +137,7 @@ lemma ab_add_one_dvd_a_pow_large_n_add_b : a * b + 1 ∣ a ^ h.large_n + b := by
       (IsUnit.mul_right_eq_zero (ZMod.unitOfCoprime _ a_coprime_ab_add_one).isUnit).1 this
   rw [mul_add]
   norm_cast
-  simp only [mul_right_inv, Units.val_one, ZMod.coe_unitOfCoprime]
+  simp only [mul_inv_cancel, Units.val_one, ZMod.coe_unitOfCoprime]
   norm_cast
   convert ZMod.natCast_self (a * b + 1) using 2
   exact add_comm _ _
@@ -151,6 +156,8 @@ lemma ab_add_one_dvd_a_pow_large_n_0_add_b : a * b + 1 ∣ a ^ h.large_n_0 + b :
   rw [← h.gcd_eq_g h.N_le_large_n_0]
   exact Nat.gcd_dvd_left _ _
 
+include h
+
 lemma ab_add_one_dvd_b_add_one : a * b + 1 ∣ b + 1 := by
   rw [add_comm b]
   suffices a * b + 1 ∣ a ^ h.large_n_0 + b by

Archive/Imo/Imo2024Q6.lean

@@ -39,6 +39,7 @@ symmetric form). -/
 def Aquaesulian (f : G → G) : Prop := ∀ x y, f (f y + x) = f x + y ∨ f (f x + y) = f y + x
 
 variable {f : G → G} (h : Aquaesulian f)
+include h
 
 lemma Aquaesulian.apply_apply_add (x : G) : f (f x + x) = f x + x := by
   rcases h x x with hx | hx <;> exact hx
@@ -62,9 +63,9 @@ lemma Aquaesulian.apply_zero : f 0 = 0 := by
 @[simp]
 lemma Aquaesulian.apply_neg_apply_add (x : G) : f (-(f x)) + x = 0 := by
   rcases h x (-(f x)) with hc | hc
-  · rw [add_right_neg, ← h.apply_zero] at hc
+  · rw [add_neg_cancel, ← h.apply_zero] at hc
     exact h.injective hc
-  · rw [add_right_neg, h.apply_zero] at hc
+  · rw [add_neg_cancel, h.apply_zero] at hc
     exact hc.symm
 
 @[simp]

Archive/MiuLanguage/DecisionNec.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gihan Marasingha
 -/
 import Archive.MiuLanguage.Basic
+import Mathlib.Data.List.Basic
 import Mathlib.Data.List.Count
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Tactic.Ring
@@ -71,9 +72,10 @@ theorem count_equiv_one_or_two_mod3_of_derivable (en : Miustr) :
   any_goals apply mod3_eq_1_or_mod3_eq_2 h_ih
   -- Porting note: `simp_rw [count_append]` usually doesn't work
   · left; rw [count_append, count_append]; rfl
-  · right; simp_rw [count_append, count_cons, if_false, two_mul]; simp
+  · right; simp_rw [count_append, count_cons, beq_iff_eq, ite_false, add_zero, two_mul]
   · left; rw [count_append, count_append, count_append]
-    simp_rw [count_cons_self, count_nil, count_cons, ite_false, add_right_comm, add_mod_right]
+    simp_rw [count_cons_self, count_nil, count_cons, beq_iff_eq, ite_false, add_right_comm,
+      add_mod_right]
     simp
   · left; rw [count_append, count_append, count_append]
     simp only [ne_eq, not_false_eq_true, count_cons_of_ne, count_nil, add_zero]
@@ -127,7 +129,7 @@ theorem goodm_of_rule1 (xs : Miustr) (h₁ : Derivable (xs ++ ↑[I])) (h₂ : G
   · change ¬M ∈ tail (xs ++ ↑([I] ++ [U]))
     rw [← append_assoc, tail_append_singleton_of_ne_nil]
     · simp_rw [mem_append, mem_singleton, or_false]; exact nmtail
-    · exact append_ne_nil_of_ne_nil_left _ _ this
+    · exact append_ne_nil_of_left_ne_nil this _
 
 theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M :: xs)) :
     Goodm (↑(M :: xs) ++ xs) := by

Archive/MiuLanguage/DecisionSuf.lean

@@ -251,7 +251,7 @@ theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count
     · -- case `x = M` gives a contradiction.
       exfalso; exact hm (mem_cons_self M xs)
     · -- case `x = I`
-      rw [count_cons, if_pos rfl, length, succ_inj']
+      rw [count_cons, beq_self_eq_true, if_pos rfl, length, succ_inj']
       apply hxs
       · simpa only [count]
       · rw [mem_cons, not_or] at hm; exact hm.2
@@ -307,7 +307,9 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D
   use as, bs
   refine ⟨rfl, ?_, ?_, ?_⟩
   · -- Porting note: `simp_rw [count_append]` didn't work
-    rw [count_append] at hu; simp_rw [count_cons, if_true, add_succ, succ_inj'] at hu
+    rw [count_append] at hu
+    simp_rw [count_cons, beq_self_eq_true, if_true, add_succ, beq_iff_eq, reduceIte, add_zero,
+      succ_inj'] at hu
     rwa [count_append, count_append]
   · apply And.intro rfl
     rw [cons_append, cons_append]

Archive/Sensitivity.lean

@@ -1,8 +1,9 @@
 /-
-Copyright (c) 2019 Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis,
+Copyright (c) 2019 Reid Barton, Johan Commelin, Jesse Michael Han, Chris Hughes, Robert Y. Lewis,
 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, Patrick Massot
+Authors: Reid Barton, Johan Commelin, Jesse Michael Han, Chris Hughes, Robert Y. Lewis,
+  Patrick Massot
 -/
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.ApplyFun
@@ -19,7 +20,7 @@ dimension n ≥ 1, if one colors more than half the vertices then at least one
 vertex has at least √n colored neighbors.
 
 A fun summer collaboration by
-Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, and Patrick Massot,
+Reid Barton, Johan Commelin, Jesse Michael Han, Chris Hughes, Robert Y. Lewis, and Patrick Massot,
 based on Don Knuth's account of the story
 (https://www.cs.stanford.edu/~knuth/papers/huang.pdf),
 using the Lean theorem prover (https://leanprover.github.io/),

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -92,6 +92,7 @@ theorem irreducible_Phi (p : ℕ) (hp : p.Prime) (hpa : p ∣ a) (hpb : p ∣ b)
       exact mt Int.natCast_dvd_natCast.mp hp2b
   all_goals exact Monic.isPrimitive (monic_Phi a b)
 
+attribute [local simp] map_ofNat in -- use `ofNat` simp theorem with bad keys
 theorem real_roots_Phi_le : Fintype.card ((Φ ℚ a b).rootSet ℝ) ≤ 3 := by
   rw [← map_Phi a b (algebraMap ℤ ℚ), Φ, ← one_mul (X ^ 5), ← C_1]
   apply (card_rootSet_le_derivative _).trans

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -113,19 +113,19 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
       ring
     · suffices -(1 : ℝ) < (r : ℝ)⁻¹ * x by exact this.ne'
       calc
-        -(1 : ℝ) = (r : ℝ)⁻¹ * -r := by simp [inv_mul_cancel hlt.ne']
+        -(1 : ℝ) = (r : ℝ)⁻¹ * -r := by simp [inv_mul_cancel₀ hlt.ne']
         _ < (r : ℝ)⁻¹ * x := by nlinarith [inv_pos.mpr hlt]
     · suffices (r : ℝ)⁻¹ * x < 1 by exact this.ne
       calc
         (r : ℝ)⁻¹ * x < (r : ℝ)⁻¹ * r := by nlinarith [inv_pos.mpr hlt]
-        _ = 1 := inv_mul_cancel hlt.ne'
+        _ = 1 := inv_mul_cancel₀ hlt.ne'
     · nlinarith
   have hcont : ContinuousOn F (Icc (-r) r) := (by continuity : Continuous F).continuousOn
   calc
     ∫ x in -r..r, 2 * f x = F r - F (-r) :=
       integral_eq_sub_of_hasDerivAt_of_le (neg_le_self r.2) hcont hderiv
         (continuous_const.mul hf).continuousOn.intervalIntegrable
     _ = NNReal.pi * (r : ℝ) ^ 2 := by
-      norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π]
+      norm_num [F, inv_mul_cancel₀ hlt.ne', ← mul_div_assoc, mul_comm π]
 
 end Theorems100