chore: bump toolchain to v4.22.0-rc2 (leanprover-community#26564)

This merged the reviewed changes from `bump/v4.22.0`, and updates Mathlib to use the `v4.22.0-rc2` toolchain.

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

Author: 3 people

Archive/Imo/Imo1987Q1.lean

@@ -46,7 +46,7 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x :
 theorem card_fixed_points :
     card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! := by
   simp only [card_congr (fixedPointsEquiv α), card_sigma, card_perm]
-  have (x) : ({x}ᶜ : Set α) = Finset.filter (· ≠ x) Finset.univ := by
+  have (x : _) : ({x}ᶜ : Set α) = Finset.filter (· ≠ x) Finset.univ := by
     ext; simp
   simp [this]
 

Cache/Lean.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster, Arthur Paulino
 -/
 
-import Lean.Util.Paths
+import Lean.Data.Json
+import Lean.Util.Path
 
 /-!
 # Helper Functions

Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

@@ -268,7 +268,7 @@ instance counterUniformity : UniformSpace ℕ := UniformSpace.ofCore counterCore
 
 lemma HasBasis_counterUniformity :
     (uniformity ℕ).HasBasis (fun _ ↦ True) fundamentalEntourage := by
-  show counterCoreUniformity.uniformity.HasBasis (fun _ ↦ True) fundamentalEntourage
+  change counterCoreUniformity.uniformity.HasBasis (fun _ ↦ True) fundamentalEntourage
   simp only [Filter.hasBasis_iff, true_and]
   intro T
   refine ⟨fun ⟨s, ⟨⟨r, hr⟩, hs⟩⟩ ↦ ⟨r, subset_of_eq_of_subset hr hs⟩ , fun ⟨n, hn⟩ ↦ ?_⟩
@@ -291,7 +291,7 @@ theorem TopIsDiscrete' : DiscreteTopology ℕ := by
     rw [mem_fundamentalEntourage]
     aesop
   · refine ⟨fundamentalEntourage (n + 1), ?_, ?_⟩
-    · show fundamentalEntourage (n + 1) ∈ counterCoreUniformity.uniformity
+    · change fundamentalEntourage (n + 1) ∈ counterCoreUniformity.uniformity
       exact @Filter.HasBasis.mem_of_mem (ℕ × ℕ) ℕ counterCoreUniformity.uniformity (fun _ ↦ True)
         fundamentalEntourage (n + 1) HasBasis_counterUniformity trivial
     · simp only [preimage_subset_iff, mem_fundamentalEntourage, add_le_iff_nonpos_right,

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -154,7 +154,7 @@ protected def copy (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) :
     NonUnitalSubalgebra R A :=
   { S.toNonUnitalSubsemiring.copy s hs with
     smul_mem' := fun r a (ha : a ∈ s) => by
-      show r • a ∈ s
+      change r • a ∈ s
       rw [hs] at ha ⊢
       exact S.smul_mem' r ha }
 
@@ -676,7 +676,7 @@ lemma adjoin_eq_span (s : Set A) : (adjoin R s).toSubmodule = span R (Subsemigro
       case Hsmul_r => exact fun r x y _ _ hxy ↦ by simpa [mul_smul_comm] using smul_mem _ _ hxy
     | smul r x _ hpx => exact smul_mem _ _ hpx
   · apply span_le.2 _
-    show Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup
+    change Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup
     exact Subsemigroup.closure_le.2 (subset_adjoin R)
 
 variable (R A)

Mathlib/Algebra/Algebra/Operations.lean

@@ -437,7 +437,7 @@ theorem map_op_mul :
   · simp_rw [map_le_iff_le_comap]
     refine mul_le.2 fun m hm n hn => ?_
     rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
-    show op n * op m ∈ _
+    change op n * op m ∈ _
     exact mul_mem_mul hn hm
   · refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
     rw [Submodule.mem_map_equiv] at hm hn ⊢

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -49,7 +49,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem
   let l' : ι → S' := fun x => ⟨l x, hl x⟩
   have e' : ∑ i ∈ ι', l' i * s' i = 1 := by
     ext
-    show S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
+    change S'.subtype (∑ i ∈ ι', l' i * s' i) = 1
     simpa only [map_sum, map_mul] using e
   have : Ideal.span (s' '' ι') = ⊤ := by
     rw [Ideal.eq_top_iff_one, ← e']

Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

@@ -24,7 +24,7 @@ theorem mul_toSubmodule_le (S T : Subalgebra R A) :
     (Subalgebra.toSubmodule S)* (Subalgebra.toSubmodule T) ≤ Subalgebra.toSubmodule (S ⊔ T) := by
   rw [Submodule.mul_le]
   intro y hy z hz
-  show y * z ∈ S ⊔ T
+  change y * z ∈ S ⊔ T
   exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)
 
 /-- As submodules, subalgebras are idempotent. -/

Mathlib/Algebra/Algebra/Unitization.lean

@@ -562,12 +562,12 @@ instance instAlgebra : Algebra S (Unitization R A) where
   commutes' := fun s x => by
     induction x with
     | inl_add_inr =>
-      show inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
+      change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
       rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
   smul_def' := fun s x => by
     induction x with
     | inl_add_inr =>
-      show _ = inl (algebraMap S R s) * _
+      change _ = inl (algebraMap S R s) * _
       rw [mul_add, smul_add,Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
         smul_one_mul, inl_smul, inr_smul, smul_one_smul]
 

Mathlib/Algebra/Algebra/ZMod.lean

@@ -31,7 +31,7 @@ abbrev algebra' (h : m ∣ n) : Algebra (ZMod n) R where
   commutes' := fun a r =>
     show (cast a * r : R) = r * cast a by
       rcases ZMod.intCast_surjective a with ⟨k, rfl⟩
-      show ZMod.castHom h R k * r = r * ZMod.castHom h R k
+      change ZMod.castHom h R k * r = r * ZMod.castHom h R k
       rw [map_intCast, Int.cast_comm]
   smul_def' := fun _ _ => rfl
 

Mathlib/Algebra/BigOperators/Fin.lean

@@ -712,7 +712,7 @@ theorem alternatingProd_eq_finset_prod {G : Type*} [DivisionCommMonoid G] :
     rw [alternatingProd, Finset.prod_eq_one]
     rintro ⟨i, ⟨⟩⟩
   | g::[] => by
-    show g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
+    change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
     rw [Fin.prod_univ_succ]; simp
   | g::h::L =>
     calc g * h⁻¹ * L.alternatingProd