chore: bump to v4.20.1 (#302)

Author: pitmonticone

MIL/C06_Discrete_Mathematics/S02_Counting_Arguments.lean

@@ -117,7 +117,7 @@ example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
     intro x _ y _ xney
     simp [disjoint_iff_ne, xney]
   -- continue the calculation
-  transitivity (∑ i in range (n+1), i)
+  transitivity (∑ i ∈ range (n + 1), i)
   · congr; ext i
     rw [card_image_of_injective, card_range]
     intros i1 i2; simp

MIL/C08_Hierarchies/S03_Subobjects.lean

@@ -132,8 +132,8 @@ instance [Group G] (H : Subgroup₁ G) : Group H :=
   inv := fun x ↦ ⟨x⁻¹, H.inv_mem x.property⟩
   inv_mul_cancel := fun x ↦ SetCoe.ext (inv_mul_cancel (x : G)) }
 
-class SubgroupClass₁ (S : Type) (G : Type) [Group G] [SetLike S G]
-    extends SubmonoidClass₁ S G  : Prop where
+class SubgroupClass₁ (S : Type) (G : Type) [Group G] [SetLike S G] : Prop
+    extends SubmonoidClass₁ S G where
   inv_mem : ∀ (s : S) {a : G}, a ∈ s → a⁻¹ ∈ s
 
 instance [Group G] : SubmonoidClass₁ (Subgroup₁ G) G where

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
+   "rev": "5c0c94b3f563ed756b48b9439788c53b0d56a897",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0",
+   "inputRev": "v4.20.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",

lakefile.toml

@@ -9,7 +9,7 @@ relaxedAutoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.20.0"
+rev = "v4.20.1"
 
 [[lean_lib]]
 name = "MIL"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.0
+leanprover/lean4:v4.20.1