bump to nightly-2023-06-20-03

mathlib commit leanprover-community/mathlib@0723536

Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.terminates_iff_rat
-! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
+! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Data.Rat.Floor
 /-!
 # Termination of Continued Fraction Computations (`gcf.of`)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Summary
 We show that the continued fraction for a value `v`, as defined in
 `algebra.continued_fractions.computation.basic`, terminates if and only if `v` corresponds to a

Mathbin/CategoryTheory/Enriched/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.enriched.basic
-! leanprover-community/mathlib commit 95a87616d63b3cb49d3fe678d416fbe9c4217bf4
+! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Tactic.ApplyFun
 /-!
 # Enriched categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We set up the basic theory of `V`-enriched categories,
 for `V` an arbitrary monoidal category.
 

Mathbin/CategoryTheory/Monoidal/Internal/Limits.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.monoidal.internal.limits
-! leanprover-community/mathlib commit 12921e9eaa574d0087ae4856860e6dda8690a438
+! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Limits.Preserves.Basic
 /-!
 # Limits of monoid objects.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `C` has limits, so does `Mon_ C`, and the forgetful functor preserves these limits.
 
 (This could potentially replace many individual constructions for concrete categories,

Mathbin/Data/Finset/Pairwise.lean

@@ -62,10 +62,12 @@ theorem PairwiseDisjoint.image_finset_of_le [DecidableEq ι] {s : Finset ι} {f
 #align set.pairwise_disjoint.image_finset_of_le Set.PairwiseDisjoint.image_finset_of_le
 -/
 
+#print Set.PairwiseDisjoint.attach /-
 theorem PairwiseDisjoint.attach (hs : (s : Set ι).PairwiseDisjoint f) :
     (s.attach : Set { x // x ∈ s }).PairwiseDisjoint (f ∘ Subtype.val) := fun i _ j _ hij =>
   hs i.2 j.2 <| mt Subtype.ext_val hij
 #align set.pairwise_disjoint.attach Set.PairwiseDisjoint.attach
+-/
 
 end SemilatticeInf
 

Mathbin/Data/Set/Pairwise/Basic.lean

@@ -480,14 +480,17 @@ theorem PairwiseDisjoint.elim_set {s : Set ι} {f : ι → Set α} (hs : s.Pairw
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print Set.PairwiseDisjoint.prod /-
 theorem PairwiseDisjoint.prod {f : ι → Set α} {g : ι' → Set β} (hs : s.PairwiseDisjoint f)
     (ht : t.PairwiseDisjoint g) :
     (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2 :=
   fun ⟨i, i'⟩ ⟨hi, hi'⟩ ⟨j, j'⟩ ⟨hj, hj'⟩ hij =>
   disjoint_left.2 fun ⟨a, b⟩ ⟨hai, hbi⟩ ⟨haj, hbj⟩ =>
     hij <| Prod.ext (hs.elim_set hi hj _ hai haj) <| ht.elim_set hi' hj' _ hbi hbj
 #align set.pairwise_disjoint.prod Set.PairwiseDisjoint.prod
+-/
 
+#print Set.pairwiseDisjoint_pi /-
 theorem pairwiseDisjoint_pi {ι' α : ι → Type _} {s : ∀ i, Set (ι' i)} {f : ∀ i, ι' i → Set (α i)}
     (hs : ∀ i, (s i).PairwiseDisjoint (f i)) :
     ((univ : Set ι).pi s).PairwiseDisjoint fun I => (univ : Set ι).pi fun i => f _ (I i) :=
@@ -497,6 +500,7 @@ theorem pairwiseDisjoint_pi {ι' α : ι → Type _} {s : ∀ i, Set (ι' i)} {f
       funext fun i =>
         (hs i).elim_set (hI i trivial) (hJ i trivial) (a i) (haI i trivial) (haJ i trivial)
 #align set.pairwise_disjoint_pi Set.pairwiseDisjoint_pi
+-/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 #print Set.pairwiseDisjoint_image_right_iff /-

Mathbin/Data/Set/Pairwise/Lattice.lean

@@ -101,6 +101,7 @@ theorem PairwiseDisjoint.biUnion {s : Set ι'} {g : ι' → Set ι} {f : ι →
 -/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print Set.PairwiseDisjoint.prod_left /-
 /-- If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is
 pairwise disjoint. Not to be confused with `set.pairwise_disjoint.prod`. -/
 theorem PairwiseDisjoint.prod_left {f : ι × ι' → α}
@@ -118,6 +119,7 @@ theorem PairwiseDisjoint.prod_left {f : ι × ι' → α}
     · convert le_iSup₂ i' hi.2; rfl
     · convert le_iSup₂ j' hj.2; rfl
 #align set.pairwise_disjoint.prod_left Set.PairwiseDisjoint.prod_left
+-/
 
 end CompleteLattice
 
@@ -126,6 +128,7 @@ section Frame
 variable [Frame α]
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print Set.pairwiseDisjoint_prod_left /-
 theorem pairwiseDisjoint_prod_left {s : Set ι} {t : Set ι'} {f : ι × ι' → α} :
     (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f ↔
       (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧
@@ -138,6 +141,7 @@ theorem pairwiseDisjoint_prod_left {s : Set ι} {t : Set ι'} {f : ι × ι' →
   · exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)
   · exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)
 #align set.pairwise_disjoint_prod_left Set.pairwiseDisjoint_prod_left
+-/
 
 end Frame
 

Mathbin/Data/Set/Prod.lean

@@ -1049,13 +1049,17 @@ section Nonempty
 
 variable [∀ i, Nonempty (α i)]
 
+#print Set.pi_eq_empty_iff' /-
 theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [pi_eq_empty_iff]
 #align set.pi_eq_empty_iff' Set.pi_eq_empty_iff'
+-/
 
+#print Set.disjoint_pi /-
 @[simp]
 theorem disjoint_pi : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i) := by
   simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']
 #align set.disjoint_pi Set.disjoint_pi
+-/
 
 end Nonempty
 

Mathbin/Data/Zmod/Algebra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 
 ! This file was ported from Lean 3 source module data.zmod.algebra
-! leanprover-community/mathlib commit 290a7ba01fbcab1b64757bdaa270d28f4dcede35
+! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -31,7 +31,9 @@ section
 variable {n : ℕ} (m : ℕ) [CharP R m]
 
 #print ZMod.algebra' /-
-/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/
+/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n`.
+See note [reducible non-instances]. -/
+@[reducible]
 def algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
   { ZMod.castHom h R with
     smul := fun a r => a * r
@@ -48,8 +50,13 @@ def algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
 
 end
 
-instance (p : ℕ) [CharP R p] : Algebra (ZMod p) R :=
+/-- The `zmod p`-algebra structure on a ring of characteristic `p`. This is not an
+instance since it creates a diamond with `algebra.id`.
+See note [reducible non-instances]. -/
+@[reducible]
+def algebra (p : ℕ) [CharP R p] : Algebra (ZMod p) R :=
   algebra' R p dvd_rfl
+#align zmod.algebra ZMod.algebra
 
 end ZMod
 

Mathbin/FieldTheory/Cardinality.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 
 ! This file was ported from Lean 3 source module field_theory.cardinality
-! leanprover-community/mathlib commit 13e18cfa070ea337ea960176414f5ae3a1534aae
+! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -42,8 +42,10 @@ universe u
 /-- A finite field has prime power cardinality. -/
 theorem Fintype.isPrimePow_card_of_field {α} [Fintype α] [Field α] : IsPrimePow ‖α‖ :=
   by
+  -- TODO: `algebra` version of `char_p.exists`, of type `Σ p, algebra (zmod p) α`
   cases' CharP.exists α with p _
   haveI hp := Fact.mk (CharP.char_is_prime α p)
+  letI : Algebra (ZMod p) α := ZMod.algebra _ _
   let b := IsNoetherian.finsetBasis (ZMod p) α
   rw [Module.card_fintype b, ZMod.card, isPrimePow_pow_iff]
   · exact hp.1.IsPrimePow

Mathbin/FieldTheory/Finite/GaloisField.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Alex J. Best, Johan Commelin, Eric Rodriguez, Ruben Van de Velde
 
 ! This file was ported from Lean 3 source module field_theory.finite.galois_field
-! leanprover-community/mathlib commit 4b05d3f4f0601dca8abf99c4ec99187682ed0bba
+! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -165,8 +165,6 @@ theorem splits_zMod_x_pow_sub_x : Splits (RingHom.id (ZMod p)) (X ^ p - X) :=
   rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]
 #align galois_field.splits_zmod_X_pow_sub_X GaloisField.splits_zMod_x_pow_sub_x
 
-attribute [-instance] ZMod.algebra
-
 /-- A Galois field with exponent 1 is equivalent to `zmod` -/
 def equivZmodP : GaloisField p 1 ≃ₐ[ZMod p] ZMod p :=
   let h : (X ^ p ^ 1 : (ZMod p)[X]) = X ^ Fintype.card (ZMod p) := by rw [pow_one, ZMod.card p]
@@ -244,6 +242,8 @@ def ringEquivOfCardEq (hKK' : Fintype.card K = Fintype.card K') : K ≃+* K' :=
     all_goals infer_instance
   rw [← hpp'] at *
   haveI := fact_iff.2 hp
+  letI : Algebra (ZMod p) K := ZMod.algebra _ _
+  letI : Algebra (ZMod p) K' := ZMod.algebra _ _
   exact alg_equiv_of_card_eq p hKK'
 #align finite_field.ring_equiv_of_card_eq FiniteField.ringEquivOfCardEq
 

Mathbin/FieldTheory/Finite/Trace.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Stoll
 
 ! This file was ported from Lean 3 source module field_theory.finite.trace
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,7 +25,8 @@ finite field, trace
 namespace FiniteField
 
 /-- The trace map from a finite field to its prime field is nongedenerate. -/
-theorem trace_to_zMod_nondegenerate (F : Type _) [Field F] [Finite F] {a : F} (ha : a ≠ 0) :
+theorem trace_to_zMod_nondegenerate (F : Type _) [Field F] [Finite F]
+    [Algebra (ZMod (ringChar F)) F] {a : F} (ha : a ≠ 0) :
     ∃ b : F, Algebra.trace (ZMod (ringChar F)) F (a * b) ≠ 0 :=
   by
   haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩

Mathbin/FieldTheory/IsAlgClosed/Classification.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module field_theory.is_alg_closed.classification
-! leanprover-community/mathlib commit 660b3a2db3522fa0db036e569dc995a615c4c848
+! leanprover-community/mathlib commit 0723536a0522d24fc2f159a096fb3304bef77472
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -196,10 +196,9 @@ variable {K L : Type} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L]
 #print IsAlgClosed.ringEquivOfCardinalEqOfCharZero /-
 /-- Two uncountable algebraically closed fields of characteristic zero are isomorphic
 if they have the same cardinality. -/
-@[nolint def_lemma]
 theorem ringEquivOfCardinalEqOfCharZero [CharZero K] [CharZero L] (hK : ℵ₀ < (#K))
-    (hKL : (#K) = (#L)) : K ≃+* L := by
-  apply Classical.choice
+    (hKL : (#K) = (#L)) : Nonempty (K ≃+* L) :=
+  by
   cases'
     exists_isTranscendenceBasis ℤ
       (show Function.Injective (algebraMap ℤ K) from Int.cast_injective) with
@@ -219,9 +218,10 @@ theorem ringEquivOfCardinalEqOfCharZero [CharZero K] [CharZero L] (hK : ℵ₀ <
 -/
 
 private theorem ring_equiv_of_cardinal_eq_of_char_p (p : ℕ) [Fact p.Prime] [CharP K p] [CharP L p]
-    (hK : ℵ₀ < (#K)) (hKL : (#K) = (#L)) : K ≃+* L :=
+    (hK : ℵ₀ < (#K)) (hKL : (#K) = (#L)) : Nonempty (K ≃+* L) :=
   by
-  apply Classical.choice
+  letI : Algebra (ZMod p) K := ZMod.algebra _ _
+  letI : Algebra (ZMod p) L := ZMod.algebra _ _
   cases'
     exists_isTranscendenceBasis (ZMod p)
       (show Function.Injective (algebraMap (ZMod p) K) from RingHom.injective _) with
@@ -246,18 +246,19 @@ private theorem ring_equiv_of_cardinal_eq_of_char_p (p : ℕ) [Fact p.Prime] [Ch
 #print IsAlgClosed.ringEquivOfCardinalEqOfCharEq /-
 /-- Two uncountable algebraically closed fields are isomorphic
 if they have the same cardinality and the same characteristic. -/
-@[nolint def_lemma]
 theorem ringEquivOfCardinalEqOfCharEq (p : ℕ) [CharP K p] [CharP L p] (hK : ℵ₀ < (#K))
-    (hKL : (#K) = (#L)) : K ≃+* L := by
-  apply Classical.choice
+    (hKL : (#K) = (#L)) : Nonempty (K ≃+* L) :=
+  by
   rcases CharP.char_is_prime_or_zero K p with (hp | hp)
   · haveI : Fact p.prime := ⟨hp⟩
-    exact ⟨ring_equiv_of_cardinal_eq_of_char_p p hK hKL⟩
+    letI : Algebra (ZMod p) K := ZMod.algebra _ _
+    letI : Algebra (ZMod p) L := ZMod.algebra _ _
+    exact ring_equiv_of_cardinal_eq_of_char_p p hK hKL
   · rw [hp] at *
     skip
     letI : CharZero K := CharP.charP_to_charZero K
     letI : CharZero L := CharP.charP_to_charZero L
-    exact ⟨ring_equiv_of_cardinal_eq_of_char_zero hK hKL⟩
+    exact ring_equiv_of_cardinal_eq_of_char_zero hK hKL
 #align is_alg_closed.ring_equiv_of_cardinal_eq_of_char_eq IsAlgClosed.ringEquivOfCardinalEqOfCharEq
 -/
 

Mathbin/FieldTheory/KrullTopology.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Monnet
 
 ! This file was ported from Lean 3 source module field_theory.krull_topology
-! leanprover-community/mathlib commit 039a089d2a4b93c761b234f3e5f5aeb752bac60f
+! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Tactic.ByContra
 /-!
 # Krull topology
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the Krull topology on `L ≃ₐ[K] L` for an arbitrary field extension `L/K`. In order to do
 this, we first define a `group_filter_basis` on `L ≃ₐ[K] L`, whose sets are `E.fixing_subgroup` for
 all intermediate fields `E` with `E/K` finite dimensional.

Mathbin/MeasureTheory/Function/ConditionalExpectation/Basic.lean

@@ -4,14 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 
 ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.basic
-! leanprover-community/mathlib commit d8bbb04e2d2a44596798a9207ceefc0fb236e41e
+! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.MeasureTheory.Function.ConditionalExpectation.CondexpL1
 
 /-! # Conditional expectation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We build the conditional expectation of an integrable function `f` with value in a Banach space
 with respect to a measure `μ` (defined on a measurable space structure `m0`) and a measurable space
 structure `m` with `hm : m ≤ m0` (a sub-sigma-algebra). This is an `m`-strongly measurable

Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -4,14 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 
 ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.condexp_L1
-! leanprover-community/mathlib commit d8bbb04e2d2a44596798a9207ceefc0fb236e41e
+! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.MeasureTheory.Function.ConditionalExpectation.CondexpL2
 
 /-! # Conditional expectation in L1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains two more steps of the construction of the conditional expectation, which is
 completed in `measure_theory.function.conditional_expectation.basic`. See that file for a
 description of the full process.

Mathbin/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 
 ! This file was ported from Lean 3 source module measure_theory.function.conditional_expectation.condexp_L2
-! leanprover-community/mathlib commit d8bbb04e2d2a44596798a9207ceefc0fb236e41e
+! leanprover-community/mathlib commit e160cefedc932ce41c7049bf0c4b0f061d06216e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.MeasureTheory.Function.ConditionalExpectation.Unique
 
 /-! # Conditional expectation in L2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains one step of the construction of the conditional expectation, which is completed
 in `measure_theory.function.conditional_expectation.basic`. See that file for a description of the
 full process.