From 49b7459e781c2cea928235d669585fb02ff89efe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Dupuis?= Date: Mon, 23 Oct 2023 02:56:48 +0000 Subject: [PATCH] feat: add gcongr lemmas for `Nat.floor`, `Nat.ceil`, `Int.floor`, `Int.ceil` (#7811) The lemmas are just restatements of lemmas of the form `Monotone Nat.floor` etc, but these cannot be tagged directly with the gcongr attribute. Co-authored-by: Mario Carneiro --- Mathlib/Algebra/Order/Floor.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Mathlib/Algebra/Order/Floor.lean b/Mathlib/Algebra/Order/Floor.lean index 4ec4f037133ca..a47e675ea4234 100644 --- a/Mathlib/Algebra/Order/Floor.lean +++ b/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]