Merge remote-tracking branch 'upstream/master' into bump/v4.31.0

Author: mathlib4-bot

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -17,11 +17,9 @@ in terms of injective functions. The general result about `Fintype.card (α ↪
 uses is `Fintype.card_embedding_eq`.
 -/
 
-
 namespace Theorems100
 
 local notation "|" x "|" => Finset.card x
-
 local notation "‖" x "‖" => Fintype.card x
 
 /-- **Birthday Problem**: set cardinality interpretation. -/
@@ -30,38 +28,23 @@ theorem birthday :
   simp only [Fintype.card_fin, Fintype.card_embedding_eq, Fintype.card_fun]
   decide
 
-section MeasureTheory
-
 open MeasureTheory ProbabilityTheory
 
-open scoped ProbabilityTheory ENNReal
-
 variable {n m : ℕ}
 
-/- In order for Lean to understand that we can take probabilities in `Fin 23 → Fin 365`, we must
-tell Lean that there is a `MeasurableSpace` structure on the space. Note that this instance
-is only for `Fin m` - Lean automatically figures out that the function space `Fin n → Fin m`
-is _also_ measurable, by using `MeasurableSpace.pi`, and furthermore that all sets are measurable,
-from `MeasurableSingletonClass.pi`. -/
-instance : MeasurableSpace (Fin m) :=
-  ⊤
-
-instance : MeasurableSingletonClass (Fin m) :=
-  ⟨fun _ => trivial⟩
-
 /- We then endow the space with a canonical measure, which is called ℙ.
 We define this to be the conditional counting measure. -/
 noncomputable instance measureSpace : MeasureSpace (Fin n → Fin m) :=
   ⟨uniformOn Set.univ⟩
 
-theorem FinFin.measure_apply {s : Set <| Fin n → Fin m} :
+theorem Fin.measure_apply {s : Set <| Fin n → Fin m} :
     ℙ s = |s.toFinite.toFinset| / ‖Fin n → Fin m‖ := by
   rw [volume, measureSpace, uniformOn_univ, Measure.count_apply_finite]
 
 /-- **Birthday Problem**: first probabilistic interpretation. -/
 theorem birthday_measure :
-    ℙ ({f | (Function.Injective f)} : Set ((Fin 23) → (Fin 365))) < 1 / 2 := by
-  rw [FinFin.measure_apply]
+    ℙ ({f | f.Injective} : Set (Fin 23 → Fin 365)) < 1 / 2 := by
+  rw [Fin.measure_apply]
   generalize_proofs hfin
   have : |hfin.toFinset| = 42200819302092359872395663074908957253749760700776448000000 := by
     trans ‖Fin 23 ↪ Fin 365‖
@@ -76,6 +59,4 @@ theorem birthday_measure :
     simp only [Fintype.card_pi, Fintype.card_fin, Finset.prod_const, Finset.card_univ]
     norm_num
 
-end MeasureTheory
-
 end Theorems100

Mathlib/Algebra/Algebra/Operations.lean

@@ -570,10 +570,8 @@ theorem mul_smul_mul_eq_smul_mul_smul (x y : R) : (x * y) • (M * N) = (x • M
 
 /-- Sub-R-modules of an R-algebra form an idempotent semiring. -/
 instance idemSemiring : IdemSemiring (Submodule R A) where
-  __ := instNonUnitalSemiring
   one_mul := Submodule.one_mul
   mul_one := Submodule.mul_one
-  bot_le _ := bot_le
 
 instance : IsOrderedRing (Submodule R A) where
 
@@ -797,7 +795,6 @@ theorem prod_span_singleton {ι : Type*} (s : Finset ι) (x : ι → A) :
 
 variable (R A)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- R-submodules of the R-algebra A are a module over `Set A`. -/
 noncomputable instance moduleSet : Module (SetSemiring A) (Submodule R A) where
   smul s P := span R (SetSemiring.down s) * P

Mathlib/Algebra/Order/Floor/Defs.lean

@@ -170,7 +170,7 @@ instance : FloorRing ℤ where
 
 /-- A `FloorRing` constructor from the `floor` function alone. -/
 @[implicit_reducible]
-def FloorRing.ofFloor (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (floor : α → ℤ)
+def FloorRing.ofFloor (α) [Ring α] [LinearOrder α] [IsOrderedRing α] (floor : α → ℤ)
     (gc_coe_floor : GaloisConnection (↑) floor) : FloorRing α :=
   { floor
     ceil := fun a => -floor (-a)
@@ -179,7 +179,7 @@ def FloorRing.ofFloor (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (
 
 /-- A `FloorRing` constructor from the `ceil` function alone. -/
 @[implicit_reducible]
-def FloorRing.ofCeil (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (ceil : α → ℤ)
+def FloorRing.ofCeil (α) [Ring α] [LinearOrder α] [IsOrderedRing α] (ceil : α → ℤ)
     (gc_ceil_coe : GaloisConnection ceil (↑)) : FloorRing α :=
   { floor := fun a => -ceil (-a)
     ceil
@@ -286,7 +286,7 @@ theorem floor_le (a : α) : (⌊a⌋ : α) ≤ a :=
 theorem floor_nonneg : 0 ≤ ⌊a⌋ ↔ 0 ≤ a := by rw [le_floor, Int.cast_zero]
 
 @[bound]
-theorem floor_nonpos [IsStrictOrderedRing α] (ha : a ≤ 0) : ⌊a⌋ ≤ 0 := by
+theorem floor_nonpos [IsOrderedRing α] (ha : a ≤ 0) : ⌊a⌋ ≤ 0 := by
   rw [← @cast_le α, Int.cast_zero]
   exact (floor_le a).trans ha
 
@@ -306,7 +306,7 @@ theorem le_ceil (a : α) : a ≤ ⌈a⌉ :=
   gc_ceil_coe.le_u_l a
 
 @[bound]
-theorem ceil_nonneg [IsStrictOrderedRing α] (ha : 0 ≤ a) : 0 ≤ ⌈a⌉ := mod_cast ha.trans (le_ceil a)
+theorem ceil_nonneg [IsOrderedRing α] (ha : 0 ≤ a) : 0 ≤ ⌈a⌉ := mod_cast ha.trans (le_ceil a)
 
 @[simp]
 theorem ceil_pos : 0 < ⌈a⌉ ↔ 0 < a := by rw [lt_ceil, cast_zero]
@@ -315,7 +315,7 @@ end Int
 
 section FloorRingToSemiring
 
-variable [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α]
+variable [Ring α] [LinearOrder α] [IsOrderedRing α] [FloorRing α]
 
 /-! #### A floor ring as a floor semiring -/
 

Mathlib/Algebra/Order/Floor/Ring.lean

@@ -158,7 +158,7 @@ theorem floor_eq_on_Ico' (n : ℤ) : ∀ a ∈ Set.Ico (n : R) (n + 1), (⌊a⌋
 theorem preimage_floor_singleton (m : ℤ) : (floor : R → ℤ) ⁻¹' {m} = Ico (m : R) (m + 1) :=
   ext fun _ => floor_eq_iff
 
-variable [IsStrictOrderedRing R]
+variable [IsOrderedRing R]
 
 @[simp, bound]
 theorem sub_one_lt_floor (a : R) : a - 1 < ⌊a⌋ :=
@@ -276,21 +276,16 @@ theorem mul_fract_eq_one_iff_exists_int {x : R} {k : R} (hk : 1 < k) :
   rw [floor_eq_iff, ← mul_le_mul_iff_right₀ hk0, ← mul_lt_mul_iff_right₀ hk0, hn]
   simp [mul_add, hk]
 
-end LinearOrderedRing
-
-section LinearOrderedCommRing
-variable {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] {a : R}
-
 theorem cast_mul_floor_div_cancel_of_pos {n : ℤ} (hn : 0 < n) (a : R) : ⌊n * a⌋ / n = ⌊a⌋ := by
-  rw [mul_comm, mul_cast_floor_div_cancel_of_pos hn]
+  rw [Commute.intCast_left, mul_cast_floor_div_cancel_of_pos hn]
 
 theorem natCast_mul_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : R) : ⌊n * a⌋ / n = ⌊a⌋ := by
-  rw [mul_comm, mul_natCast_floor_div_cancel hn]
+  rw [Nat.cast_comm, mul_natCast_floor_div_cancel hn]
 
-end LinearOrderedCommRing
+end LinearOrderedRing
 
 section LinearOrderedField
-variable {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a b : k}
+variable {k : Type*} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k}
 
 theorem floor_div_cast_of_nonneg {n : ℤ} (hn : 0 ≤ n) (a : k) : ⌊a / n⌋ = ⌊a⌋ / n := by
   obtain rfl | hn := hn.eq_or_lt
@@ -332,7 +327,7 @@ theorem fract_sub_self (a : R) : fract a - a = -⌊a⌋ :=
 theorem fract_add (a b : R) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
   ⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by unfold fract; grind⟩
 
-variable [IsStrictOrderedRing R]
+variable [IsOrderedRing R]
 
 @[simp]
 theorem fract_add_intCast (a : R) (m : ℤ) : fract (a + m) = fract a := by
@@ -441,8 +436,9 @@ theorem fract_eq_iff {a b : R} : fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z : 
     exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩,
    by
     rintro ⟨h₀, h₁, z, hz⟩
-    rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz,
-      Int.cast_inj, floor_eq_iff, ← hz]
+    rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz]
+    refine congrArg Int.cast ?_
+    rw [floor_eq_iff, ← hz]
     constructor <;> simpa [sub_eq_add_neg, add_assoc] ⟩
 
 theorem fract_eq_fract {a b : R} : fract a = fract b ↔ ∃ z : ℤ, a - b = z :=
@@ -513,13 +509,13 @@ theorem image_fract (s : Set R) : fract '' s = ⋃ m : ℤ, (fun x : R => x - m)
 
 section LinearOrderedField
 
-variable {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {b : k}
+variable {k : Type*} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {b : k}
 
 theorem fract_div_mul_self_mem_Ico (a b : k) (ha : 0 < a) : fract (b / a) * a ∈ Ico 0 a :=
   ⟨(mul_nonneg_iff_of_pos_right ha).2 (fract_nonneg (b / a)),
     (mul_lt_iff_lt_one_left ha).2 (fract_lt_one (b / a))⟩
 
-omit [IsStrictOrderedRing k] in
+omit [IsOrderedRing k] in
 theorem fract_div_mul_self_add_zsmul_eq (a b : k) (ha : a ≠ 0) :
     fract (b / a) * a + ⌊b / a⌋ • a = b := by
   rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]
@@ -619,7 +615,7 @@ theorem ceil_eq_on_Ioc (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, ⌈a⌉ = z
 theorem preimage_ceil_singleton (m : ℤ) : (ceil : R → ℤ) ⁻¹' {m} = Ioc ((m : R) - 1) m :=
   ext fun _ => ceil_eq_iff
 
-variable [IsStrictOrderedRing R]
+variable [IsOrderedRing R]
 
 theorem floor_neg : ⌊-a⌋ = -⌈a⌉ :=
   eq_of_forall_le_iff fun z => by rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]
@@ -713,8 +709,9 @@ theorem ceil_zero : ⌈(0 : R)⌉ = 0 := by rw [← cast_zero, ceil_intCast]
 @[simp]
 theorem ceil_one : ⌈(1 : R)⌉ = 1 := by rw [← cast_one, ceil_intCast]
 
-theorem ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, (⌈a⌉ : R) = z := fun a ha =>
-  mod_cast ceil_eq_on_Ioc z a ha
+omit [IsOrderedRing R] in
+theorem ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, (⌈a⌉ : R) = z :=
+  fun a ha => congrArg Int.cast (ceil_eq_on_Ioc z a ha)
 
 lemma ceil_eq_self_iff_mem (a : R) : ⌈a⌉ = a ↔ a ∈ Set.range Int.cast := by
   aesop
@@ -729,8 +726,9 @@ theorem floor_lt_ceil_of_lt {a b : R} (h : a < b) : ⌊a⌋ < ⌈b⌉ :=
 
 lemma ceil_eq_floor_add_one_iff_notMem (a : R) : ⌈a⌉ = ⌊a⌋ + 1 ↔ a ∉ Set.range Int.cast := by
   refine ⟨fun h ht => ?_, fun h => ?_⟩
-  · have := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
-    linarith [Int.cast_inj.mp this]
+  · have h0 := ((floor_eq_self_iff_mem _).mpr ht).trans ((ceil_eq_self_iff_mem _).mpr ht).symm
+    rw [h, cast_add, cast_one, left_eq_add] at h0
+    exact one_ne_zero h0
   · apply le_antisymm (Int.ceil_le_floor_add_one _)
     rw [add_one_le_iff, lt_ceil]
     exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))
@@ -742,9 +740,8 @@ theorem fract_eq_zero_or_add_one_sub_ceil (a : R) : fract a = 0 ∨ fract a = a
   suffices (⌈a⌉ : R) = ⌊a⌋ + 1 by
     rw [this, ← self_sub_fract]
     abel
-  norm_cast
-  rw [ceil_eq_iff]
-  refine ⟨?_, _root_.le_of_lt <| by simp⟩
+  rw [← Int.cast_one, ← Int.cast_add]
+  refine congrArg Int.cast (ceil_eq_iff.mpr ⟨?_, _root_.le_of_lt <| by simp⟩)
   rw [cast_add, cast_one, add_tsub_cancel_right, ← self_sub_fract a, sub_lt_self_iff]
   exact ha.symm.lt_of_le (fract_nonneg a)
 
@@ -759,7 +756,7 @@ theorem ceil_sub_self_eq (ha : fract a ≠ 0) : (⌈a⌉ : R) - a = 1 - fract a
 end ceil
 
 section LinearOrderedField
-variable {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] [FloorRing k] {a b : k}
+variable {k : Type*} [Field k] [LinearOrder k] [IsOrderedRing k] [FloorRing k] {a b : k}
 
 lemma mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉ ≤ a) : b * a < ⌊a⌋ := by
   calc
@@ -889,7 +886,7 @@ end Nat
 
 section FloorRingToSemiring
 
-variable [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
+variable [Ring R] [LinearOrder R] [IsOrderedRing R] [FloorRing R]
 
 /-! #### A floor ring as a floor semiring -/
 

Mathlib/Algebra/Order/Floor/Semifield.lean

@@ -51,7 +51,7 @@ theorem floor_div_eq_div (m n : ℕ) : ⌊(m : K) / n⌋₊ = m / n := by
 end LinearOrderedSemifield
 
 section LinearOrderedField
-variable [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K}
+variable [Field K] [LinearOrder K] [IsOrderedRing K] [FloorSemiring K] {a b : K}
 
 lemma mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉₊ ≤ a) : b * a < ⌊a⌋₊ := by
   calc

Mathlib/Algebra/Order/Floor/Semiring.lean

@@ -157,10 +157,9 @@ theorem mul_cast_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : R) : ⌊a * n⌋
   rw [le_div_iff_mul_le (zero_lt_of_ne_zero hn), le_floor_iff (mul_nonneg ha (cast_nonneg' n)),
     le_floor_iff ha, cast_mul, mul_le_mul_iff_of_pos_right (cast_pos'.mpr (zero_lt_of_ne_zero hn))]
 
-theorem cast_mul_floor_div_cancel {R : Type*} [CommSemiring R] [LinearOrder R]
-    [IsStrictOrderedRing R] [FloorSemiring R] {n : ℕ} (hn : n ≠ 0) (a : R) :
+theorem cast_mul_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : R) :
     ⌊n * a⌋₊ / n = ⌊a⌋₊ := by
-  rw [mul_comm, mul_cast_floor_div_cancel hn]
+  rw [Nat.cast_comm, mul_cast_floor_div_cancel hn]
 
 end floor
 
@@ -207,7 +206,7 @@ theorem ceil_le_floor_add_one (a : R) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1 := by
   exact (lt_floor_add_one a).le
 
 @[simp]
-theorem ceil_intCast {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R]
+theorem ceil_intCast {R : Type*} [Ring R] [LinearOrder R] [IsOrderedRing R]
     [FloorSemiring R] (z : ℤ) :
     ⌈(z : R)⌉₊ = z.toNat :=
   eq_of_forall_ge_iff fun a => by