Trigger CI for leanprover/lean4#2712

Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

@@ -31,34 +31,6 @@ set_option linter.uppercaseLean3 false
 
 namespace Counterexample
 
-namespace FromBhavik
-
-/-- Bhavik Mehta's example.  There are only the initial definitions, but no proofs.  The Type
-`K` is a canonically ordered commutative semiring with the property that `2 * (1/2) ≤ 2 * 1`, even
-though it is not true that `1/2 ≤ 1`, since `1/2` and `1` are not comparable. -/
-def K : Type :=
-  Subsemiring.closure ({1.5} : Set ℚ)
-deriving CommSemiring
-#align counterexample.from_Bhavik.K Counterexample.FromBhavik.K
-
-instance : Coe K ℚ :=
-  ⟨fun x => x.1⟩
-
-instance inhabitedK : Inhabited K :=
-  ⟨0⟩
-#align counterexample.from_Bhavik.inhabited_K Counterexample.FromBhavik.inhabitedK
-
-instance : Preorder K where
-  le x y := x = y ∨ (x : ℚ) + 1 ≤ (y : ℚ)
-  le_refl x := Or.inl rfl
-  le_trans x y z xy yz := by
-    rcases xy with (rfl | xy); · apply yz
-    rcases yz with (rfl | yz); · right; apply xy
-    right
-    exact xy.trans (le_trans ((le_add_iff_nonneg_right _).mpr zero_le_one) yz)
-
-end FromBhavik
-
 theorem mem_zmod_2 (a : ZMod 2) : a = 0 ∨ a = 1 := by
   rcases a with ⟨_ | _, _ | _ | _ | _⟩
   · exact Or.inl rfl

Mathlib.lean

@@ -391,6 +391,7 @@ import Mathlib.Algebra.Order.Ring.Cone
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Order.Ring.InjSurj
 import Mathlib.Algebra.Order.Ring.Lemmas
+import Mathlib.Algebra.Order.Ring.Star
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.SMul
 import Mathlib.Algebra.Order.Sub.Basic
@@ -1203,8 +1204,10 @@ import Mathlib.CategoryTheory.Sites.CoverPreserving
 import Mathlib.CategoryTheory.Sites.Coverage
 import Mathlib.CategoryTheory.Sites.DenseSubsite
 import Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
+import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
 import Mathlib.CategoryTheory.Sites.Grothendieck
 import Mathlib.CategoryTheory.Sites.InducedTopology
+import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.LeftExact
 import Mathlib.CategoryTheory.Sites.Limits
 import Mathlib.CategoryTheory.Sites.Plus
@@ -1263,6 +1266,7 @@ import Mathlib.Combinatorics.HalesJewett
 import Mathlib.Combinatorics.Hall.Basic
 import Mathlib.Combinatorics.Hall.Finite
 import Mathlib.Combinatorics.Hindman
+import Mathlib.Combinatorics.Optimization.ValuedCSP
 import Mathlib.Combinatorics.Partition
 import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Combinatorics.Quiver.Arborescence
@@ -1410,6 +1414,7 @@ import Mathlib.Data.Fin.Interval
 import Mathlib.Data.Fin.SuccPred
 import Mathlib.Data.Fin.Tuple.Basic
 import Mathlib.Data.Fin.Tuple.BubbleSortInduction
+import Mathlib.Data.Fin.Tuple.Curry
 import Mathlib.Data.Fin.Tuple.Monotone
 import Mathlib.Data.Fin.Tuple.NatAntidiagonal
 import Mathlib.Data.Fin.Tuple.Reflection
@@ -1921,6 +1926,7 @@ import Mathlib.Data.ZMod.Algebra
 import Mathlib.Data.ZMod.Basic
 import Mathlib.Data.ZMod.Coprime
 import Mathlib.Data.ZMod.Defs
+import Mathlib.Data.ZMod.IntUnitsPower
 import Mathlib.Data.ZMod.Parity
 import Mathlib.Data.ZMod.Quotient
 import Mathlib.Data.ZMod.Units
@@ -2025,6 +2031,7 @@ import Mathlib.Geometry.Manifold.MFDeriv
 import Mathlib.Geometry.Manifold.Metrizable
 import Mathlib.Geometry.Manifold.PartitionOfUnity
 import Mathlib.Geometry.Manifold.Sheaf.Basic
+import Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
 import Mathlib.Geometry.Manifold.Sheaf.Smooth
 import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
 import Mathlib.Geometry.Manifold.VectorBundle.Basic
@@ -3079,6 +3086,7 @@ import Mathlib.SetTheory.ZFC.Basic
 import Mathlib.SetTheory.ZFC.Ordinal
 import Mathlib.Tactic
 import Mathlib.Tactic.Abel
+import Mathlib.Tactic.ApplyAt
 import Mathlib.Tactic.ApplyCongr
 import Mathlib.Tactic.ApplyFun
 import Mathlib.Tactic.ApplyWith

Mathlib/Algebra/Algebra/Operations.lean

@@ -463,10 +463,7 @@ protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n 
     obtain ⟨r, rfl⟩ := hx
     exact hr r
   revert hx
-  -- porting note: workaround for lean4#1926, was `simp_rw [pow_succ']`
-  suffices h_lean4_1926 : ∀ (hx' : x ∈ M ^ n * M), C (Nat.succ n) x (by rwa [pow_succ']) from
-    fun hx => h_lean4_1926 (by rwa [← pow_succ'])
-  -- porting note: end workaround
+  simp_rw [pow_succ']
   intro hx
   exact
     Submodule.mul_induction_on' (fun m hm x ih => hmul _ _ hm (n_ih _) _ ih)

Mathlib/Algebra/BigOperators/Ring.lean

@@ -147,7 +147,7 @@ theorem prod_add [DecidableEq α] (f g : α → β) (s : Finset α) :
           rw [prod_ite]
           congr 1
           exact prod_bij'
-            (fun a _ => a.1) (by simp; tauto) (by simp)
+            (fun a _ => a.1) (by simp) (by simp)
             (fun a ha => ⟨a, (mem_filter.1 ha).1⟩) (fun a ha => by simp at ha; simp; tauto)
             (by simp) (by simp)
           exact prod_bij'

Mathlib/Algebra/CharP/Quotient.lean

@@ -42,6 +42,18 @@ theorem quotient' {R : Type*} [CommRing R] (p : ℕ) [CharP R p] (I : Ideal R)
     exact ⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩⟩
 #align char_p.quotient' CharP.quotient'
 
+/-- `CharP.quotient'` as an `Iff`. -/
+theorem quotient_iff {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
+    CharP (R ⧸ I) n ↔ ∀ x : ℕ, ↑x ∈ I → (x : R) = 0 := by
+  refine ⟨fun _ x hx => ?_, CharP.quotient' n I⟩
+  rw [CharP.cast_eq_zero_iff R n, ←CharP.cast_eq_zero_iff (R ⧸ I) n _]
+  exact (Submodule.Quotient.mk_eq_zero I).mpr hx
+
+/-- `CharP.quotient_iff`, but stated in terms of inclusions of ideals. -/
+theorem quotient_iff_le_ker_natCast {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
+    CharP (R ⧸ I) n ↔ I.comap (Nat.castRingHom R) ≤ RingHom.ker (Nat.castRingHom R) := by
+  rw [CharP.quotient_iff, RingHom.ker_eq_comap_bot]; rfl
+
 end CharP
 
 theorem Ideal.Quotient.index_eq_zero {R : Type*} [CommRing R] (I : Ideal R) :

Mathlib/Algebra/DirectLimit.lean

@@ -732,17 +732,14 @@ protected theorem inv_mul_cancel {p : Ring.DirectLimit G f} (hp : p ≠ 0) : inv
   rw [_root_.mul_comm, DirectLimit.mul_inv_cancel G f hp]
 #align field.direct_limit.inv_mul_cancel Field.DirectLimit.inv_mul_cancel
 
--- porting note: this takes some time, had to increase heartbeats
-set_option maxHeartbeats 500000 in
 /-- Noncomputable field structure on the direct limit of fields.
 See note [reducible non-instances]. -/
 @[reducible]
 protected noncomputable def field [DirectedSystem G fun i j h => f' i j h] :
     Field (Ring.DirectLimit G fun i j h => f' i j h) :=
-  { Ring.DirectLimit.commRing G fun i j h => f' i j h,
-    DirectLimit.nontrivial G fun i j h =>
-      f' i j h with
-    inv := inv G fun i j h => f' i j h
+  -- This used to include the parent CommRing and Nontrivial instances,
+  -- but leaving them implicit avoids a very expensive (2-3 minutes!) eta expansion.
+  { inv := inv G fun i j h => f' i j h
     mul_inv_cancel := fun p => DirectLimit.mul_inv_cancel G fun i j h => f' i j h
     inv_zero := dif_pos rfl }
 #align field.direct_limit.field Field.DirectLimit.field

Mathlib/Algebra/Group/Basic.lean

@@ -280,7 +280,7 @@ theorem leftInverse_inv : LeftInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
 #align left_inverse_neg leftInverse_neg
 
 @[to_additive]
-theorem rightInverse_inv : LeftInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
+theorem rightInverse_inv : RightInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
   inv_inv
 #align right_inverse_inv rightInverse_inv
 #align right_inverse_neg rightInverse_neg

Mathlib/Algebra/Group/TypeTags.lean

@@ -267,6 +267,24 @@ instance Multiplicative.monoid [h : AddMonoid α] : Monoid (Multiplicative α) :
     npow_zero := @AddMonoid.nsmul_zero α h
     npow_succ := @AddMonoid.nsmul_succ α h }
 
+@[simp]
+theorem ofMul_pow [Monoid α] (n : ℕ) (a : α) : ofMul (a ^ n) = n • ofMul a :=
+  rfl
+#align of_mul_pow ofMul_pow
+
+@[simp]
+theorem toMul_nsmul [Monoid α] (n : ℕ) (a : Additive α) : toMul (n • a) = toMul a ^ n :=
+  rfl
+
+@[simp]
+theorem ofAdd_nsmul [AddMonoid α] (n : ℕ) (a : α) : ofAdd (n • a) = ofAdd a ^ n :=
+  rfl
+#align of_add_nsmul ofAdd_nsmul
+
+@[simp]
+theorem toAdd_pow [AddMonoid α] (a : Multiplicative α) (n : ℕ) : toAdd (a ^ n) = n • toAdd a :=
+  rfl
+
 instance Additive.addLeftCancelMonoid [LeftCancelMonoid α] : AddLeftCancelMonoid (Additive α) :=
   { Additive.addMonoid, Additive.addLeftCancelSemigroup with }
 
@@ -363,6 +381,24 @@ instance Multiplicative.divInvMonoid [SubNegMonoid α] : DivInvMonoid (Multiplic
     zpow_succ' := @SubNegMonoid.zsmul_succ' α _
     zpow_neg' := @SubNegMonoid.zsmul_neg' α _ }
 
+@[simp]
+theorem ofMul_zpow [DivInvMonoid α] (z : ℤ) (a : α) : ofMul (a ^ z) = z • ofMul a :=
+  rfl
+#align of_mul_zpow ofMul_zpow
+
+@[simp]
+theorem toMul_zsmul [DivInvMonoid α] (z : ℤ) (a : Additive α) : toMul (z • a) = toMul a ^ z :=
+  rfl
+
+@[simp]
+theorem ofAdd_zsmul [SubNegMonoid α] (z : ℤ) (a : α) : ofAdd (z • a) = ofAdd a ^ z :=
+  rfl
+#align of_add_zsmul ofAdd_zsmul
+
+@[simp]
+theorem toAdd_zpow [SubNegMonoid α] (a : Multiplicative α) (z : ℤ) : toAdd (a ^ z) = z • toAdd a :=
+  rfl
+
 instance Additive.subtractionMonoid [DivisionMonoid α] : SubtractionMonoid (Additive α) :=
   { Additive.subNegMonoid, Additive.involutiveNeg with
     neg_add_rev := @mul_inv_rev α _

Mathlib/Algebra/GroupPower/Basic.lean

@@ -443,25 +443,6 @@ theorem pow_dvd_pow [Monoid R] (a : R) {m n : ℕ} (h : m ≤ n) : a ^ m ∣ a ^
   ⟨a ^ (n - m), by rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]⟩
 #align pow_dvd_pow pow_dvd_pow
 
-theorem ofAdd_nsmul [AddMonoid A] (x : A) (n : ℕ) :
-    Multiplicative.ofAdd (n • x) = Multiplicative.ofAdd x ^ n :=
-  rfl
-#align of_add_nsmul ofAdd_nsmul
-
-theorem ofAdd_zsmul [SubNegMonoid A] (x : A) (n : ℤ) :
-    Multiplicative.ofAdd (n • x) = Multiplicative.ofAdd x ^ n :=
-  rfl
-#align of_add_zsmul ofAdd_zsmul
-
-theorem ofMul_pow [Monoid A] (x : A) (n : ℕ) : Additive.ofMul (x ^ n) = n • Additive.ofMul x :=
-  rfl
-#align of_mul_pow ofMul_pow
-
-theorem ofMul_zpow [DivInvMonoid G] (x : G) (n : ℤ) :
-    Additive.ofMul (x ^ n) = n • Additive.ofMul x :=
-  rfl
-#align of_mul_zpow ofMul_zpow
-
 @[to_additive (attr := simp)]
 theorem SemiconjBy.zpow_right [Group G] {a x y : G} (h : SemiconjBy a x y) :
     ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -1177,7 +1177,6 @@ section Multiplicative
 
 open Multiplicative
 
-@[simp]
 theorem Nat.toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b :=
   mul_comm _ _
 #align nat.to_add_pow Nat.toAdd_pow
@@ -1187,12 +1186,10 @@ theorem Nat.ofAdd_mul (a b : ℕ) : ofAdd (a * b) = ofAdd a ^ b :=
   (Nat.toAdd_pow _ _).symm
 #align nat.of_add_mul Nat.ofAdd_mul
 
-@[simp]
 theorem Int.toAdd_pow (a : Multiplicative ℤ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b :=
   mul_comm _ _
 #align int.to_add_pow Int.toAdd_pow
 
-@[simp]
 theorem Int.toAdd_zpow (a : Multiplicative ℤ) (b : ℤ) : toAdd (a ^ b) = toAdd a * b :=
   mul_comm _ _
 #align int.to_add_zpow Int.toAdd_zpow

Mathlib/Algebra/Order/Floor.lean

@@ -189,6 +189,9 @@ theorem floor_mono : Monotone (floor : α → ℕ) := fun a b h => by
   · exact le_floor ((floor_le ha).trans h)
 #align nat.floor_mono Nat.floor_mono
 
+@[gcongr]
+theorem floor_le_floor : ∀ x y : α, x ≤ y → ⌊x⌋₊ ≤ ⌊y⌋₊ := floor_mono
+
 theorem le_floor_iff' (hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ (n : α) ≤ a := by
   obtain ha | ha := le_total a 0
   · rw [floor_of_nonpos ha]
@@ -317,6 +320,9 @@ theorem ceil_mono : Monotone (ceil : α → ℕ) :=
   gc_ceil_coe.monotone_l
 #align nat.ceil_mono Nat.ceil_mono
 
+@[gcongr]
+theorem ceil_le_ceil : ∀ x y : α, x ≤ y → ⌈x⌉₊ ≤ ⌈y⌉₊ := ceil_mono
+
 @[simp]
 theorem ceil_zero : ⌈(0 : α)⌉₊ = 0 := by rw [← Nat.cast_zero, ceil_natCast]
 #align nat.ceil_zero Nat.ceil_zero
@@ -738,6 +744,9 @@ theorem floor_mono : Monotone (floor : α → ℤ) :=
   gc_coe_floor.monotone_u
 #align int.floor_mono Int.floor_mono
 
+@[gcongr]
+theorem floor_le_floor : ∀ x y : α, x ≤ y → ⌊x⌋ ≤ ⌊y⌋ := floor_mono
+
 theorem floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a := by
   -- Porting note: broken `convert le_floor`
   rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]
@@ -1210,6 +1219,9 @@ theorem ceil_mono : Monotone (ceil : α → ℤ) :=
   gc_ceil_coe.monotone_l
 #align int.ceil_mono Int.ceil_mono
 
+@[gcongr]
+theorem ceil_le_ceil : ∀ x y : α, x ≤ y → ⌈x⌉ ≤ ⌈y⌉ := ceil_mono
+
 @[simp]
 theorem ceil_add_int (a : α) (z : ℤ) : ⌈a + z⌉ = ⌈a⌉ + z := by
   rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_int]

Mathlib/Algebra/Order/Ring/Star.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2023 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import Mathlib.Algebra.Order.Ring.Defs
+import Mathlib.Algebra.Star.Order
+
+/-!
+# Commutative star-ordered rings are ordered rings
+
+A noncommutative star-ordered ring is generally not an ordered ring. Indeed, in a star-ordered
+ring, nonnegative elements are self-adjoint, but the product of self-adjoint elements is
+self-adjoint if and only if they commute. Therefore, a necessary condition for a star-ordered ring
+to be an ordered ring is that all nonnegative elements commute.  Consequently, if a star-ordered
+ring is spanned by it nonnegative elements (as is the case for C⋆-algebras) and it is also an
+ordered ring, then it is commutative.
+
+In this file we prove the converse: a *commutative* star-ordered ring is an ordered ring.
+-/
+
+namespace StarOrderedRing
+
+/- This example shows that nonnegative elements in a ordered semiring which is also star-ordered
+must commute. We provide this only as an example as opposed to a lemma because we never expect the
+type class assumptions to be satisfied without a `CommSemiring` intance already in scope; not that
+it is impossible, only that it shouldn't occur in practice. -/
+example {R : Type*} [OrderedSemiring R] [StarOrderedRing R] {x y : R} (hx : 0 ≤ x) (hy : 0 ≤ y) :
+    x * y = y * x := by
+  -- nonnegative elements are self-adjoint; we prove it by hand to avoid adding imports
+  have : ∀ z : R, 0 ≤ z → star z = z := by
+    intros z hz
+    rw [nonneg_iff] at hz
+    induction hz using AddSubmonoid.closure_induction' with
+    | Hs _ h => obtain ⟨x, rfl⟩ := h; simp
+    | H1 => simp
+    | Hmul x hx y hy => simp only [←nonneg_iff] at hx hy; aesop
+  -- `0 ≤ y * x`, and hence `y * x` is self-adjoint
+  have := this _ <| mul_nonneg hy hx
+  aesop
+
+/- This will be implied by the instance below, we only prove it to avoid duplicating the
+argument in the instance below for `mul_le_mul_of_nonneg_right`. -/
+private lemma mul_le_mul_of_nonneg_left {R : Type*} [CommSemiring R] [PartialOrder R]
+    [StarOrderedRing R] {a b c : R} (hab : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b := by
+  rw [StarOrderedRing.nonneg_iff] at hc
+  induction hc using AddSubmonoid.closure_induction' with
+  | Hs _ h =>
+    obtain ⟨x, rfl⟩ := h
+    simp_rw [mul_assoc, mul_comm x, ←mul_assoc]
+    exact conjugate_le_conjugate hab x
+  | H1 => simp
+  | Hmul x hx y hy =>
+    simp only [←nonneg_iff, add_mul] at hx hy ⊢
+    apply add_le_add <;> aesop
+
+/-- A commutative star-ordered semiring is an ordered semiring.
+
+This is not registered as an instance because it introduces a type class loop between `CommSemiring`
+and `OrderedCommSemiring`, and it seem loops still cause issues sometimes.
+
+See note [reducible non-instances]. -/
+@[reducible]
+def toOrderedCommSemiring (R : Type*) [CommSemiring R] [PartialOrder R]
+    [StarOrderedRing R] : OrderedCommSemiring R where
+  add_le_add_left _ _ := add_le_add_left
+  zero_le_one := by simpa using star_mul_self_nonneg (1 : R)
+  mul_comm := mul_comm
+  mul_le_mul_of_nonneg_left _ _ _ := mul_le_mul_of_nonneg_left
+  mul_le_mul_of_nonneg_right a b c := by simpa only [mul_comm _ c] using mul_le_mul_of_nonneg_left
+
+/-- A commutative star-ordered ring is an ordered ring.
+
+This is not registered as an instance because it introduces a type class loop between `CommSemiring`
+and `OrderedCommSemiring`, and it seem loops still cause issues sometimes.
+
+See note [reducible non-instances]. -/
+@[reducible]
+def toOrderedCommRing (R : Type*) [CommRing R] [PartialOrder R]
+    [StarOrderedRing R] : OrderedCommRing R where
+  add_le_add_left _ _ := add_le_add_left
+  zero_le_one := by simpa using star_mul_self_nonneg (1 : R)
+  mul_comm := mul_comm
+  mul_nonneg _ _ := let _ := toOrderedCommSemiring R; mul_nonneg