bump to nightly-2023-08-04-09

mathlib commit leanprover-community/mathlib@48a058d

Mathbin/Data/Bitvec/Core.lean

@@ -83,7 +83,6 @@ def shl (x : Bitvec n) (i : ℕ) : Bitvec n :=
 #align bitvec.shl Bitvec.shl
 -/
 
-#print Bitvec.fillShr /-
 /-- `fill_shr x i fill` is the bitvector obtained by right-shifting `x` `i` times and then
 padding with `fill : bool`. If `x.length < i` then this will return the constant `fill`
 bitvector. -/
@@ -98,7 +97,6 @@ def fillShr (x : Bitvec n) (i : ℕ) (fill : Bool) : Bitvec n :=
           rw [min_eq_left h₁, tsub_eq_zero_iff_le.mpr h₁, zero_min, Nat.add_zero]) <|
     replicate (min n i) fill++ₜtake (n - i) x
 #align bitvec.fill_shr Bitvec.fillShr
--/
 
 #print Bitvec.ushr /-
 /-- unsigned shift right -/

Mathbin/LinearAlgebra/Dimension.lean

@@ -380,15 +380,14 @@ theorem LinearIndependent.set_finite_of_isNoetherian [IsNoetherian R M] {s : Set
 #align linear_independent.set_finite_of_is_noetherian LinearIndependent.set_finite_of_isNoetherian
 -/
 
-#print basisFintypeOfFiniteSpans /-
 -- One might hope that a finite spanning set implies that any linearly independent set is finite.
 -- While this is true over a division ring
 -- (simply because any linearly independent set can be extended to a basis),
 -- I'm not certain what more general statements are possible.
 /--
 Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
 -/
-def basisFintypeOfFiniteSpans (w : Set M) [Fintype w] (s : span R w = ⊤) {ι : Type w}
+def basis_finite_of_finite_spans (w : Set M) [Fintype w] (s : span R w = ⊤) {ι : Type w}
     (b : Basis ι R M) : Fintype ι :=
   by
   -- We'll work by contradiction, assuming `ι` is infinite.
@@ -415,8 +414,7 @@ def basisFintypeOfFiniteSpans (w : Set M) [Fintype w] (s : span R w = ⊤) {ι :
   -- giving the desire contradiction.
   refine' b.linear_independent.not_mem_span_image _ k'
   exact nm
-#align basis_fintype_of_finite_spans basisFintypeOfFiniteSpans
--/
+#align basis_fintype_of_finite_spans basis_finite_of_finite_spansₓ
 
 #print union_support_maximal_linearIndependent_eq_range_basis /-
 -- From [Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973]
@@ -633,7 +631,7 @@ theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) :
   cases fintypeOrInfinite ι
   · -- `v` is a finite basis, so by `basis_fintype_of_finite_spans` so is `v'`.
     haveI : Fintype (range v) := Set.fintypeRange v
-    haveI := basisFintypeOfFiniteSpans _ v.span_eq v'
+    haveI := basis_finite_of_finite_spans _ v.span_eq v'
     -- We clean up a little:
     rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
     simp only [Cardinal.lift_natCast, Cardinal.natCast_inj]
@@ -707,7 +705,7 @@ theorem basis_le_span' {ι : Type _} (b : Basis ι R M) {w : Set M} [Fintype w]
     (#ι) ≤ Fintype.card w :=
   by
   haveI := nontrivial_of_invariantBasisNumber R
-  haveI := basisFintypeOfFiniteSpans w s b
+  haveI := basis_finite_of_finite_spans w s b
   rw [Cardinal.mk_fintype ι]
   simp only [Cardinal.natCast_le]
   exact Basis.le_span'' b s

Mathbin/LinearAlgebra/Dual.lean

@@ -1733,7 +1733,7 @@ theorem dualMap_injective_iff {f : V₁ →ₗ[K] V₂} :
   refine' ⟨_, fun h => dual_map_injective_of_surjective h⟩
   rw [← range_eq_top, ← ker_eq_bot]
   intro h
-  apply FiniteDimensional.eq_top_of_finrank_eq
+  apply Submodule.eq_top_of_finrank_eq
   rw [← finrank_eq_zero] at h 
   rw [← add_zero (FiniteDimensional.finrank K f.range), ← h, ←
     LinearMap.finrank_range_dualMap_eq_finrank_range, LinearMap.finrank_range_add_finrank_ker,

Mathbin/LinearAlgebra/FiniteDimensional.lean

@@ -402,7 +402,7 @@ theorem finrank_zero_iff [FiniteDimensional K V] : finrank K V = 0 ↔ Subsingle
 #align finite_dimensional.finrank_zero_iff FiniteDimensional.finrank_zero_iff
 -/
 
-#print FiniteDimensional.eq_top_of_finrank_eq /-
+#print Submodule.eq_top_of_finrank_eq /-
 /-- If a submodule has maximal dimension in a finite dimensional space, then it is equal to the
 whole space. -/
 theorem eq_top_of_finrank_eq [FiniteDimensional K V] {S : Submodule K V}
@@ -430,7 +430,7 @@ theorem eq_top_of_finrank_eq [FiniteDimensional K V] {S : Submodule K V}
   have := bS.span_eq
   rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this 
   rw [this, map_top (Submodule.subtype S), range_subtype]
-#align finite_dimensional.eq_top_of_finrank_eq FiniteDimensional.eq_top_of_finrank_eq
+#align finite_dimensional.eq_top_of_finrank_eq Submodule.eq_top_of_finrank_eq
 -/
 
 variable (K)
@@ -1305,6 +1305,8 @@ section DivisionRing
 variable [DivisionRing K] [AddCommGroup V] [Module K V] {V₂ : Type v'} [AddCommGroup V₂]
   [Module K V₂]
 
+/- warning: submodule.eq_top_of_finrank_eq clashes with finite_dimensional.eq_top_of_finrank_eq -> Submodule.eq_top_of_finrank_eq
+Case conversion may be inaccurate. Consider using '#align submodule.eq_top_of_finrank_eq Submodule.eq_top_of_finrank_eqₓ'. -/
 #print Submodule.eq_top_of_finrank_eq /-
 theorem eq_top_of_finrank_eq [FiniteDimensional K V] {S : Submodule K V}
     (h : finrank K S = finrank K V) : S = ⊤ :=

Mathbin/LinearAlgebra/FreeModule/Finite/Basic.lean

@@ -43,7 +43,7 @@ noncomputable instance [Nontrivial R] [Module.Finite R M] :
   by
   obtain ⟨h⟩ := id ‹Module.Finite R M›
   choose s hs using h
-  exact basisFintypeOfFiniteSpans (↑s) hs (choose_basis _ _)
+  exact basis_finite_of_finite_spans (↑s) hs (choose_basis _ _)
 
 end Ring
 

Mathbin/NumberTheory/NumberField/Embeddings.lean

@@ -237,12 +237,10 @@ theorem IsReal.coe_embedding_apply {φ : K →+* ℂ} (hφ : IsReal φ) (x : K)
 #align number_field.complex_embedding.is_real.coe_embedding_apply NumberField.ComplexEmbedding.IsReal.coe_embedding_apply
 -/
 
-#print NumberField.ComplexEmbedding.IsReal.place_embedding /-
 theorem IsReal.place_embedding {φ : K →+* ℂ} (hφ : IsReal φ) : place hφ.Embedding = place φ := by
   ext x;
   simp only [place_apply, Real.norm_eq_abs, ← abs_of_real, norm_eq_abs, hφ.coe_embedding_apply x]
 #align number_field.complex_embedding.is_real.place_embedding NumberField.ComplexEmbedding.IsReal.place_embedding
--/
 
 #print NumberField.ComplexEmbedding.isReal_conjugate_iff /-
 theorem isReal_conjugate_iff {φ : K →+* ℂ} : IsReal (conjugate φ) ↔ IsReal φ :=
@@ -297,11 +295,9 @@ instance : NonnegHomClass (InfinitePlace K) K ℝ
   coe_injective' _ _ h := Subtype.eq (AbsoluteValue.ext fun x => congr_fun h x)
   map_nonneg w x := w.1.NonNeg _
 
-#print NumberField.InfinitePlace.coe_mk /-
 theorem coe_mk (φ : K →+* ℂ) : ⇑(mk φ) = place φ :=
   rfl
 #align number_field.infinite_place.coe_mk NumberField.InfinitePlace.coe_mk
--/
 
 #print NumberField.InfinitePlace.apply /-
 theorem apply (φ : K →+* ℂ) (x : K) : (mk φ) x = Complex.abs (φ x) :=
@@ -323,12 +319,10 @@ theorem mk_embedding (w : InfinitePlace K) : mk (embedding w) = w :=
 #align number_field.infinite_place.mk_embedding NumberField.InfinitePlace.mk_embedding
 -/
 
-#print NumberField.InfinitePlace.abs_embedding /-
 @[simp]
 theorem abs_embedding (w : InfinitePlace K) (x : K) : Complex.abs (embedding w x) = w x :=
   congr_fun (congr_arg coeFn w.2.choose_spec) x
 #align number_field.infinite_place.abs_embedding NumberField.InfinitePlace.abs_embedding
--/
 
 #print NumberField.InfinitePlace.eq_iff_eq /-
 theorem eq_iff_eq (x : K) (r : ℝ) : (∀ w : InfinitePlace K, w x = r) ↔ ∀ φ : K →+* ℂ, ‖φ x‖ = r :=
@@ -407,14 +401,14 @@ def IsComplex (w : InfinitePlace K) : Prop :=
 #align number_field.infinite_place.is_complex NumberField.InfinitePlace.IsComplex
 -/
 
-#print NumberField.ComplexEmbeddings.IsReal.embedding_mk /-
+#print NumberField.InfinitePlace.embedding_mk_eq_of_isReal /-
 @[simp]
-theorem NumberField.ComplexEmbeddings.IsReal.embedding_mk {φ : K →+* ℂ}
+theorem NumberField.InfinitePlace.embedding_mk_eq_of_isReal {φ : K →+* ℂ}
     (h : ComplexEmbedding.IsReal φ) : embedding (mk φ) = φ :=
   by
   have := mk_eq_iff.mp (mk_embedding (mk φ)).symm
   rwa [complex_embedding.is_real_iff.mp h, or_self_iff, eq_comm] at this 
-#align number_field.complex_embeddings.is_real.embedding_mk NumberField.ComplexEmbeddings.IsReal.embedding_mk
+#align number_field.complex_embeddings.is_real.embedding_mk NumberField.InfinitePlace.embedding_mk_eq_of_isReal
 -/
 
 #print NumberField.InfinitePlace.isReal_iff /-
@@ -449,42 +443,38 @@ theorem not_isReal_iff_isComplex {w : InfinitePlace K} : ¬IsReal w ↔ IsComple
 #align number_field.infinite_place.not_is_real_iff_is_complex NumberField.InfinitePlace.not_isReal_iff_isComplex
 -/
 
-#print NumberField.InfinitePlace.not_isComplex_iff_isReal /-
 @[simp]
 theorem not_isComplex_iff_isReal {w : InfinitePlace K} : ¬IsComplex w ↔ IsReal w := by
   rw [← not_is_real_iff_is_complex, Classical.not_not]
 #align number_field.infinite_place.not_is_complex_iff_is_real NumberField.InfinitePlace.not_isComplex_iff_isReal
--/
 
 #print NumberField.InfinitePlace.isReal_or_isComplex /-
 theorem isReal_or_isComplex (w : InfinitePlace K) : IsReal w ∨ IsComplex w := by
   rw [← not_is_real_iff_is_complex]; exact em _
 #align number_field.infinite_place.is_real_or_is_complex NumberField.InfinitePlace.isReal_or_isComplex
 -/
 
-#print NumberField.InfinitePlace.IsReal.embedding /-
+#print NumberField.InfinitePlace.embedding_of_isReal /-
 /-- For `w` a real infinite place, return the corresponding embedding as a morphism `K →+* ℝ`. -/
-noncomputable def IsReal.embedding {w : InfinitePlace K} (hw : IsReal w) : K →+* ℝ :=
+noncomputable def NumberField.InfinitePlace.embedding_of_isReal {w : InfinitePlace K}
+    (hw : IsReal w) : K →+* ℝ :=
   (isReal_iff.mp hw).Embedding
-#align number_field.infinite_place.is_real.embedding NumberField.InfinitePlace.IsReal.embedding
+#align number_field.infinite_place.is_real.embedding NumberField.InfinitePlace.embedding_of_isReal
 -/
 
-#print NumberField.InfinitePlace.IsReal.place_embedding_apply /-
 @[simp]
-theorem IsReal.place_embedding_apply {w : InfinitePlace K} (hw : IsReal w) (x : K) :
-    place (IsReal.embedding hw) x = w x :=
+theorem IsReal.place_embedding_of_isReal_apply {w : InfinitePlace K} (hw : IsReal w) (x : K) :
+    place (NumberField.InfinitePlace.embedding_of_isReal hw) x = w x :=
   by
   rw [is_real.embedding, complex_embedding.is_real.place_embedding, ← coe_mk]
   exact congr_fun (congr_arg coeFn (mk_embedding w)) x
-#align number_field.infinite_place.is_real.place_embedding_apply NumberField.InfinitePlace.IsReal.place_embedding_apply
--/
+#align number_field.infinite_place.is_real.place_embedding_apply NumberField.InfinitePlace.IsReal.place_embedding_of_isReal_apply
 
-#print NumberField.InfinitePlace.IsReal.abs_embedding_apply /-
 @[simp]
-theorem IsReal.abs_embedding_apply {w : InfinitePlace K} (hw : IsReal w) (x : K) :
-    |IsReal.embedding hw x| = w x := by rw [← is_real.place_embedding_apply hw x]; congr
-#align number_field.infinite_place.is_real.abs_embedding_apply NumberField.InfinitePlace.IsReal.abs_embedding_apply
--/
+theorem IsReal.abs_embedding_of_isReal_apply {w : InfinitePlace K} (hw : IsReal w) (x : K) :
+    |NumberField.InfinitePlace.embedding_of_isReal hw x| = w x := by
+  rw [← is_real.place_embedding_apply hw x]; congr
+#align number_field.infinite_place.is_real.abs_embedding_apply NumberField.InfinitePlace.IsReal.abs_embedding_of_isReal_apply
 
 variable (K)
 
@@ -495,7 +485,7 @@ noncomputable def mkReal :
     where
   toFun := Subtype.map mk fun φ hφ => ⟨φ, hφ, rfl⟩
   invFun w := ⟨w.1.Embedding, isReal_iff.1 w.2⟩
-  left_inv φ := Subtype.ext_iff.2 (NumberField.ComplexEmbeddings.IsReal.embedding_mk φ.2)
+  left_inv φ := Subtype.ext_iff.2 (NumberField.InfinitePlace.embedding_mk_eq_of_isReal φ.2)
   right_inv w := Subtype.ext_iff.2 (mk_embedding w.1)
 #align number_field.infinite_place.mk_real NumberField.InfinitePlace.mkReal
 -/
@@ -508,15 +498,13 @@ noncomputable def mkComplex :
 #align number_field.infinite_place.mk_complex NumberField.InfinitePlace.mkComplex
 -/
 
-#print NumberField.InfinitePlace.mkComplex_embedding /-
 theorem mkComplex_embedding (φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }) :
     (mkComplex K φ : InfinitePlace K).Embedding = φ ∨
       (mkComplex K φ : InfinitePlace K).Embedding = ComplexEmbedding.conjugate φ :=
   by
   rw [@eq_comm _ _ ↑φ, @eq_comm _ _ (complex_embedding.conjugate ↑φ), ← mk_eq_iff, mk_embedding]
   rfl
 #align number_field.infinite_place.mk_complex_embedding NumberField.InfinitePlace.mkComplex_embedding
--/
 
 #print NumberField.InfinitePlace.mkReal_coe /-
 @[simp]
@@ -534,25 +522,20 @@ theorem mkComplex_coe (φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }
 #align number_field.infinite_place.mk_complex_coe NumberField.InfinitePlace.mkComplex_coe
 -/
 
-#print NumberField.InfinitePlace.mkReal.apply /-
 @[simp]
 theorem mkReal.apply (φ : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ }) (x : K) :
     mkReal K φ x = Complex.abs (φ x) :=
   apply φ x
 #align number_field.infinite_place.mk_real.apply NumberField.InfinitePlace.mkReal.apply
--/
 
-#print NumberField.InfinitePlace.mkComplex.apply /-
 @[simp]
 theorem mkComplex.apply (φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }) (x : K) :
     mkComplex K φ x = Complex.abs (φ x) :=
   apply φ x
 #align number_field.infinite_place.mk_complex.apply NumberField.InfinitePlace.mkComplex.apply
--/
 
 variable [NumberField K]
 
-#print NumberField.InfinitePlace.mkComplex.filter /-
 theorem mkComplex.filter (w : { w : InfinitePlace K // w.IsComplex }) :
     (Finset.univ.filterₓ fun φ => mkComplex K φ = w) =
       {⟨w.1.Embedding, isComplex_iff.1 w.2⟩,
@@ -565,9 +548,7 @@ theorem mkComplex.filter (w : { w : InfinitePlace K // w.IsComplex }) :
     mk_eq_iff, mk_embedding, @eq_comm _ _ w.val]
   simpa only [Finset.mem_univ, true_and_iff]
 #align number_field.infinite_place.mk_complex.filter NumberField.InfinitePlace.mkComplex.filter
--/
 
-#print NumberField.InfinitePlace.mkComplex.filter_card /-
 theorem mkComplex.filter_card (w : { w : InfinitePlace K // w.IsComplex }) :
     (Finset.univ.filterₓ fun φ => mkComplex K φ = w).card = 2 :=
   by
@@ -577,7 +558,6 @@ theorem mkComplex.filter_card (w : { w : InfinitePlace K // w.IsComplex }) :
       (subtype.mk_eq_mk.not.2 <|
         ne_comm.1 <| complex_embedding.is_real_iff.not.1 <| is_complex_iff.1 w.2)
 #align number_field.infinite_place.mk_complex.filter_card NumberField.InfinitePlace.mkComplex.filter_card
--/
 
 #print NumberField.InfinitePlace.NumberField.InfinitePlace.fintype /-
 noncomputable instance NumberField.InfinitePlace.fintype : Fintype (InfinitePlace K) :=

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "b958934cb632da1dc92417773d96e0ae3eec8956",
+    "rev": "8d126006f6703f2e6d8fd67c610d6122abd332af",
     "name": "lean3port",
-    "inputRev?": "b958934cb632da1dc92417773d96e0ae3eec8956"}},
+    "inputRev?": "8d126006f6703f2e6d8fd67c610d6122abd332af"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
@@ -22,9 +22,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "4412853e2b44449d06f0461dd97599fe7913392b",
+    "rev": "72ea277bd5a9687917fae7bccc45ab6b2586ac3f",
     "name": "mathlib",
-    "inputRev?": "4412853e2b44449d06f0461dd97599fe7913392b"}},
+    "inputRev?": "72ea277bd5a9687917fae7bccc45ab6b2586ac3f"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-08-04-07"
+def tag : String := "nightly-2023-08-04-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"b958934cb632da1dc92417773d96e0ae3eec8956"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"8d126006f6703f2e6d8fd67c610d6122abd332af"
 
 @[default_target]
 lean_lib Mathbin where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-30
+leanprover/lean4:nightly-2023-08-03