Trigger CI for leanprover/lean4#2722

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/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/Data/List/Basic.lean

@@ -4160,37 +4160,37 @@ end ZipRight
 #noalign list.to_chunks_join
 #noalign list.to_chunks_length_le
 
-/-! ### all₂ -/
+/-! ### Forall -/
 
-section All₂
+section Forall
 
 variable {p q : α → Prop} {l : List α}
 
 @[simp]
-theorem all₂_cons (p : α → Prop) (x : α) : ∀ l : List α, All₂ p (x :: l) ↔ p x ∧ All₂ p l
+theorem forall_cons (p : α → Prop) (x : α) : ∀ l : List α, Forall p (x :: l) ↔ p x ∧ Forall p l
   | [] => (and_true_iff _).symm
   | _ :: _ => Iff.rfl
-#align list.all₂_cons List.all₂_cons
+#align list.all₂_cons List.forall_cons
 
-theorem all₂_iff_forall : ∀ {l : List α}, All₂ p l ↔ ∀ x ∈ l, p x
+theorem forall_iff_forall_mem : ∀ {l : List α}, Forall p l ↔ ∀ x ∈ l, p x
   | [] => (iff_true_intro <| forall_mem_nil _).symm
-  | x :: l => by rw [forall_mem_cons, all₂_cons, all₂_iff_forall]
-#align list.all₂_iff_forall List.all₂_iff_forall
+  | x :: l => by rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]
+#align list.all₂_iff_forall List.forall_iff_forall_mem
 
-theorem All₂.imp (h : ∀ x, p x → q x) : ∀ {l : List α}, All₂ p l → All₂ q l
+theorem Forall.imp (h : ∀ x, p x → q x) : ∀ {l : List α}, Forall p l → Forall q l
   | [] => id
-  | x :: l => by simp; rw [←and_imp]; exact And.imp (h x) (All₂.imp h)
-#align list.all₂.imp List.All₂.imp
+  | x :: l => by simp; rw [←and_imp]; exact And.imp (h x) (Forall.imp h)
+#align list.all₂.imp List.Forall.imp
 
 @[simp]
-theorem all₂_map_iff {p : β → Prop} (f : α → β) : All₂ p (l.map f) ↔ All₂ (p ∘ f) l := by
+theorem forall_map_iff {p : β → Prop} (f : α → β) : Forall p (l.map f) ↔ Forall (p ∘ f) l := by
   induction l <;> simp [*]
-#align list.all₂_map_iff List.all₂_map_iff
+#align list.all₂_map_iff List.forall_map_iff
 
-instance (p : α → Prop) [DecidablePred p] : DecidablePred (All₂ p) := fun _ =>
-  decidable_of_iff' _ all₂_iff_forall
+instance (p : α → Prop) [DecidablePred p] : DecidablePred (Forall p) := fun _ =>
+  decidable_of_iff' _ forall_iff_forall_mem
 
-end All₂
+end Forall
 
 /-! ### Retroattributes
 

Mathlib/Data/List/Defs.lean

@@ -220,14 +220,14 @@ end mapIdxM
 #align list.sublists List.sublists
 #align list.forall₂ List.Forall₂
 
-/-- `l.All₂ p` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e.
-`List.All₂ p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
+/-- `l.Forall p` is equivalent to `∀ a ∈ l, p a`, but unfolds directly to a conjunction, i.e.
+`List.Forall p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`. -/
 @[simp]
-def All₂ (p : α → Prop) : List α → Prop
+def Forall (p : α → Prop) : List α → Prop
   | [] => True
   | x :: [] => p x
-  | x :: l => p x ∧ All₂ p l
-#align list.all₂ List.All₂
+  | x :: l => p x ∧ Forall p l
+#align list.all₂ List.Forall
 
 #align list.transpose List.transpose
 #align list.sections List.sections

Mathlib/Data/List/Zip.lean

@@ -55,14 +55,14 @@ theorem zip_swap : ∀ (l₁ : List α) (l₂ : List β), (zip l₁ l₂).map Pr
 
 #align list.length_zip List.length_zip
 
-theorem all₂_zipWith {f : α → β → γ} {p : γ → Prop} :
+theorem forall_zipWith {f : α → β → γ} {p : γ → Prop} :
     ∀ {l₁ : List α} {l₂ : List β} (_h : length l₁ = length l₂),
-      All₂ p (zipWith f l₁ l₂) ↔ Forall₂ (fun x y => p (f x y)) l₁ l₂
+      Forall p (zipWith f l₁ l₂) ↔ Forall₂ (fun x y => p (f x y)) l₁ l₂
   | [], [], _ => by simp
   | a :: l₁, b :: l₂, h => by
     simp only [length_cons, succ_inj'] at h
-    simp [all₂_zipWith h]
-#align list.all₂_zip_with List.all₂_zipWith
+    simp [forall_zipWith h]
+#align list.all₂_zip_with List.forall_zipWith
 
 theorem lt_length_left_of_zipWith {f : α → β → γ} {i : ℕ} {l : List α} {l' : List β}
     (h : i < (zipWith f l l').length) : i < l.length := by

Mathlib/NumberTheory/Dioph.lean

@@ -264,10 +264,10 @@ theorem sumsq_nonneg (x : α → ℕ) : ∀ l, 0 ≤ sumsq l x
     exact add_nonneg (mul_self_nonneg _) (sumsq_nonneg _ ps)
 #align poly.sumsq_nonneg Poly.sumsq_nonneg
 
-theorem sumsq_eq_zero (x) : ∀ l, sumsq l x = 0 ↔ l.All₂ fun a : Poly α => a x = 0
+theorem sumsq_eq_zero (x) : ∀ l, sumsq l x = 0 ↔ l.Forall fun a : Poly α => a x = 0
   | [] => eq_self_iff_true _
   | p::ps => by
-    rw [List.all₂_cons, ← sumsq_eq_zero _ ps]; rw [sumsq]
+    rw [List.forall_cons, ← sumsq_eq_zero _ ps]; rw [sumsq]
     exact
       ⟨fun h : p x * p x + sumsq ps x = 0 =>
         have : p x = 0 :=
@@ -351,10 +351,10 @@ theorem reindex_dioph (f : α → β) : ∀ _ : Dioph S, Dioph {v | v ∘ f ∈
 
 variable {β}
 
-theorem DiophList.all₂ (l : List (Set <| α → ℕ)) (d : l.All₂ Dioph) :
-    Dioph {v | l.All₂ fun S : Set (α → ℕ) => v ∈ S} := by
-  suffices ∃ (β : _) (pl : List (Poly (Sum α β))), ∀ v, List.All₂ (fun S : Set _ => S v) l ↔
-          ∃ t, List.All₂ (fun p : Poly (Sum α β) => p (v ⊗ t) = 0) pl
+theorem DiophList.forall (l : List (Set <| α → ℕ)) (d : l.Forall Dioph) :
+    Dioph {v | l.Forall fun S : Set (α → ℕ) => v ∈ S} := by
+  suffices ∃ (β : _) (pl : List (Poly (Sum α β))), ∀ v, List.Forall (fun S : Set _ => S v) l ↔
+          ∃ t, List.Forall (fun p : Poly (Sum α β) => p (v ⊗ t) = 0) pl
     from
     let ⟨β, pl, h⟩ := this
     ⟨β, Poly.sumsq pl, fun v => (h v).trans <| exists_congr fun t => (Poly.sumsq_eq_zero _ _).symm⟩
@@ -372,7 +372,7 @@ theorem DiophList.all₂ (l : List (Set <| α → ℕ)) (d : l.All₂ Dioph) :
             ⟨m ⊗ n, by
               rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from
                     funext fun s => by cases' s with a b <;> rfl]; exact hm, by
-              refine List.All₂.imp (fun q hq => ?_) hn; dsimp [(· ∘ ·)]
+              refine List.Forall.imp (fun q hq => ?_) hn; dsimp [(· ∘ ·)]
               rw [show
                     (fun x : Sum α γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n
                     from funext fun s => by cases' s with a b <;> rfl]; exact hq⟩,
@@ -381,14 +381,14 @@ theorem DiophList.all₂ (l : List (Set <| α → ℕ)) (d : l.All₂ Dioph) :
                 rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
                     funext fun s => by cases' s with a b <;> rfl] at hl⟩,
               ⟨t ∘ inr, by
-                refine List.All₂.imp (fun q hq => ?_) hr; dsimp [(· ∘ ·)] at hq
+                refine List.Forall.imp (fun q hq => ?_) hr; dsimp [(· ∘ ·)] at hq
                 rwa [show
                     (fun x : Sum α γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) =
                       v ⊗ t ∘ inr
                     from funext fun s => by cases' s with a b <;> rfl] at hq ⟩⟩⟩⟩
-#align dioph.dioph_list.all₂ Dioph.DiophList.all₂
+#align dioph.dioph_list.all₂ Dioph.DiophList.forall
 
-theorem inter (d : Dioph S) (d' : Dioph S') : Dioph (S ∩ S') := DiophList.all₂ [S, S'] ⟨d, d'⟩
+theorem inter (d : Dioph S) (d' : Dioph S') : Dioph (S ∩ S') := DiophList.forall [S, S'] ⟨d, d'⟩
 #align dioph.inter Dioph.inter
 
 theorem union : ∀ (_ : Dioph S) (_ : Dioph S'), Dioph (S ∪ S')

Mathlib/Tactic/Linarith/Lemmas.lean

@@ -10,6 +10,7 @@ import Mathlib.Algebra.Order.Monoid.Lemmas
 import Mathlib.Init.Data.Int.Order
 import Mathlib.Algebra.Order.ZeroLEOne
 import Mathlib.Algebra.GroupPower.Order
+import Mathlib.Data.Nat.Cast.Order
 
 /-!
 # Lemmas for `linarith`.
@@ -68,6 +69,7 @@ lemma zero_mul_eq {α} {R : α → α → Prop} [Semiring α] {a b : α} (h : a
     a * b = 0 := by
   simp [h]
 
+lemma nat_cast_nonneg (α : Type u) [OrderedSemiring α] (n : ℕ) : (0 : α) ≤ n := Nat.cast_nonneg n
 
 end Linarith
 

Mathlib/Tactic/Linarith/Preprocessing.lean

@@ -32,7 +32,8 @@ namespace Linarith
 
 /-! ### Preprocessing -/
 
-open Lean Elab Tactic Meta
+open Lean hiding Rat
+open Elab Tactic Meta
 open Qq
 
 /-- Processor that recursively replaces `P ∧ Q` hypotheses with the pair `P` and `Q`. -/
@@ -114,33 +115,43 @@ partial def isNatProp (e : Expr) : Bool :=
   | (``Not, #[e]) => isNatProp e
   | _ => false
 
-/-- If `e` is of the form `((n : ℕ) : ℤ)`, `isNatIntCoe e` returns `n : ℕ`. -/
-def isNatIntCoe (e : Expr) : Option Expr :=
+
+/-- If `e` is of the form `((n : ℕ) : C)`, `isNatCoe e` returns `⟨n, C⟩`. -/
+def isNatCoe (e: Expr) : Option (Expr × Expr) :=
   match e.getAppFnArgs with
-  | (``Nat.cast, #[.const ``Int [], _, n]) => some n
+  | (``Nat.cast, #[target, _, n]) => some ⟨n, target⟩
   | _ => none
 
 /--
-`getNatComparisons e` returns a list of all subexpressions of `e` of the form `((t : ℕ) : ℤ)`.
+`getNatComparisons e` returns a list of all subexpressions of `e` of the form `((t : ℕ) : C)`.
 -/
-partial def getNatComparisons (e : Expr) : List Expr :=
-  match isNatIntCoe e with
-  | some n => [n]
+partial def getNatComparisons (e : Expr) : List (Expr × Expr) :=
+  match isNatCoe e with
+  | some x => [x]
   | none => match e.getAppFnArgs with
     | (``HAdd.hAdd, #[_, _, _, _, a, b]) => getNatComparisons a ++ getNatComparisons b
     | (``HMul.hMul, #[_, _, _, _, a, b]) => getNatComparisons a ++ getNatComparisons b
+    | (``HSub.hSub, #[_, _, _, _, a, b]) => getNatComparisons a ++ getNatComparisons b
+    | (``Neg.neg, #[_, _, a]) => getNatComparisons a
     | _ => []
 
-/-- If `e : ℕ`, returns a proof of `0 ≤ (e : ℤ)`. -/
-def mk_coe_nat_nonneg_prf (e : Expr) : MetaM Expr :=
-  mkAppM ``Int.coe_nat_nonneg #[e]
+/-- If `e : ℕ`, returns a proof of `0 ≤ (e : C)`. -/
+def mk_coe_nat_nonneg_prf (p : Expr × Expr) : MetaM (Option Expr) :=
+  match p with
+  | ⟨e, target⟩ => try commitIfNoEx (mkAppM ``nat_cast_nonneg #[target, e])
+    catch e => do
+      trace[linarith] "Got exception when using cast {e.toMessageData}"
+      return none
+
 
 open Std
 
 /-- Ordering on `Expr`. -/
--- We only define this so we can use `RBSet Expr`. Perhaps `HashSet` would be more appropriate?
-def Expr.compare (a b : Expr) : Ordering :=
-  if Expr.lt a b then .lt else if a.equal b then .eq else .gt
+def Expr.Ord : Ord Expr :=
+⟨fun a b => if Expr.lt a b then .lt else if a.equal b then .eq else .gt⟩
+
+attribute [local instance] Expr.Ord
+
 
 /--
 If `h` is an equality or inequality between natural numbers,
@@ -166,12 +177,12 @@ def natToInt : GlobalBranchingPreprocessor where
           pure h
       else
         pure h
-    let nonnegs ← l.foldlM (init := ∅) fun (es : RBSet Expr Expr.compare) h => do
+    let nonnegs ← l.foldlM (init := ∅) fun (es : RBSet (Expr × Expr) lexOrd.compare) h => do
       try
         let (a, b) ← getRelSides (← inferType h)
         pure <| (es.insertList (getNatComparisons a)).insertList (getNatComparisons b)
       catch _ => pure es
-    pure [(g, ((← nonnegs.toList.mapM mk_coe_nat_nonneg_prf) ++ l : List Expr))]
+    pure [(g, ((← nonnegs.toList.filterMapM mk_coe_nat_nonneg_prf) ++ l : List Expr))]
 
 end natToInt
 

Mathlib/Tactic/Says.lean

@@ -19,6 +19,9 @@ The typical usage case is:
 ```
 simp? [X] says simp only [X, Y, Z]
 ```
+
+If you use `set_option says.verify true` (set automatically during CI) then `X says Y`
+runs `X` and verifies that it still prints "Try this: Y".
 -/
 
 open Lean Elab Tactic
@@ -92,6 +95,20 @@ def evalTacticCapturingTryThis (tac : TSyntax `tactic) : TacticM (TSyntax ``tact
   | .ok stx => return stx
   | .error err => throwError m!"Failed to parse tactic output: {tryThis}\n{err}"
 
+/--
+If you write `X says`, where `X` is a tactic that produces a "Try this: Y" message,
+then you will get a message "Try this: X says Y".
+Once you've clicked to replace `X says` with `X says Y`,
+afterwards `X says Y` will only run `Y`.
+
+The typical usage case is:
+```
+simp? [X] says simp only [X, Y, Z]
+```
+
+If you use `set_option says.verify true` (set automatically during CI) then `X says Y`
+runs `X` and verifies that it still prints "Try this: Y".
+-/
 syntax (name := says) tactic " says" (colGt tacticSeq)? : tactic
 
 elab_rules : tactic

Mathlib/Topology/MetricSpace/MetrizableUniformity.lean

@@ -140,7 +140,8 @@ theorem le_two_mul_dist_ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x
       rw [← not_lt, Nat.lt_iff_add_one_le, ← hL_len]
       intro hLm
       rw [mem_setOf_eq, take_all_of_le hLm, two_mul, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
-          sum_eq_zero_iff, ← all₂_iff_forall, all₂_zipWith, ← chain_append_singleton_iff_forall₂]
+          sum_eq_zero_iff, ← forall_iff_forall_mem, forall_zipWith,
+          ← chain_append_singleton_iff_forall₂]
           at hm <;>
         [skip; simp]
       exact hd₀ (hm.rel (mem_append.2 <| Or.inr <| mem_singleton_self _))

test/linarith.lean

@@ -525,4 +525,14 @@ noncomputable instance : LinearOrderedField (P c d) := test_sorry
 example (p : P PUnit.{u+1} PUnit.{v+1}) (h : 0 < p) : 0 < 2 * p := by
   linarith
 
+example (n : Nat) : n + 1 ≥ (1 / 2 : ℚ) := by linarith
+
+example {α : Type} [LinearOrderedCommRing α] (n : Nat) : (5 : α) - (n : α) ≤ (6 : α) := by
+  linarith
+
+example {α : Type} [LinearOrderedCommRing α] (n : Nat) : -(n : α) ≤ 0 := by
+  linarith
+
+example {α : Type} [LinearOrderedCommRing α] (n : Nat) (a : α) (h : a ≥ 2): a * (n : α) + 5 ≥ 4 := by
+  nlinarith
 example (x : ℚ) (h : x * (2⁻¹ + 2 / 3) = 1) : x = 6 / 7 := by linarith