feat: add lemmas about floor/ceil/fract/round and `OfNat.ofNa…

…t` (#6037)

Motivated by `fract_add_one` from the Sphere Eversion Project.

Mathlib/Algebra/Order/Floor.lean

@@ -450,6 +450,11 @@ theorem floor_add_one (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1 := by
   rw [←cast_one, floor_add_nat ha 1]
 #align nat.floor_add_one Nat.floor_add_one
 
+theorem floor_add_ofNat (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
+    ⌊a + OfNat.ofNat n⌋₊ = ⌊a⌋₊ + OfNat.ofNat n :=
+  floor_add_nat ha n
+
+@[simp]
 theorem floor_sub_nat [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ℕ) :
     ⌊a - n⌋₊ = ⌊a⌋₊ - n := by
   obtain ha | ha := le_total a 0
@@ -461,6 +466,15 @@ theorem floor_sub_nat [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n :
     exact le_tsub_of_add_le_left ((add_zero _).trans_le h)
 #align nat.floor_sub_nat Nat.floor_sub_nat
 
+@[simp]
+theorem floor_sub_one [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) : ⌊a - 1⌋₊ = ⌊a⌋₊ - 1 := by
+  exact_mod_cast floor_sub_nat a 1
+
+@[simp]
+theorem floor_sub_ofNat [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ℕ) [n.AtLeastTwo] :
+    ⌊a - OfNat.ofNat n⌋₊ = ⌊a⌋₊ - OfNat.ofNat n :=
+  floor_sub_nat a n
+
 theorem ceil_add_nat (ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
   eq_of_forall_ge_iff fun b => by
     rw [← not_lt, ← not_lt, not_iff_not, lt_ceil]
@@ -476,6 +490,10 @@ theorem ceil_add_one (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1 := by
   rw [cast_one.symm, ceil_add_nat ha 1]
 #align nat.ceil_add_one Nat.ceil_add_one
 
+theorem ceil_add_ofNat (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] :
+    ⌈a + OfNat.ofNat n⌉₊ = ⌈a⌉₊ + OfNat.ofNat n :=
+  ceil_add_nat ha n
+
 theorem ceil_lt_add_one (ha : 0 ≤ a) : (⌈a⌉₊ : α) < a + 1 :=
   lt_ceil.1 <| (Nat.lt_succ_self _).trans_le (ceil_add_one ha).ge
 #align nat.ceil_lt_add_one Nat.ceil_lt_add_one
@@ -501,6 +519,8 @@ section LinearOrderedSemifield
 
 variable [LinearOrderedSemifield α] [FloorSemiring α]
 
+-- TODO: should these lemmas be `simp`? `norm_cast`?
+
 theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
   cases' le_total a 0 with ha ha
   · rw [floor_of_nonpos, floor_of_nonpos ha]
@@ -517,6 +537,10 @@ theorem floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n := by
   · exact cast_pos.2 hn
 #align nat.floor_div_nat Nat.floor_div_nat
 
+theorem floor_div_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
+    ⌊a / OfNat.ofNat n⌋₊ = ⌊a⌋₊ / OfNat.ofNat n :=
+  floor_div_nat a n
+
 /-- Natural division is the floor of field division. -/
 theorem floor_div_eq_div (m n : ℕ) : ⌊(m : α) / n⌋₊ = m / n := by
   convert floor_div_nat (m : α) n
@@ -707,6 +731,8 @@ theorem floor_zero : ⌊(0 : α)⌋ = 0 := by rw [← cast_zero, floor_intCast]
 theorem floor_one : ⌊(1 : α)⌋ = 1 := by rw [← cast_one, floor_intCast]
 #align int.floor_one Int.floor_one
 
+@[simp] theorem floor_ofNat (n : ℕ) [n.AtLeastTwo] : ⌊(OfNat.ofNat n : α)⌋ = n := floor_natCast n
+
 @[mono]
 theorem floor_mono : Monotone (floor : α → ℤ) :=
   gc_coe_floor.monotone_u
@@ -723,6 +749,7 @@ theorem floor_add_int (a : α) (z : ℤ) : ⌊a + z⌋ = ⌊a⌋ + z :=
     rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]
 #align int.floor_add_int Int.floor_add_int
 
+@[simp]
 theorem floor_add_one (a : α) : ⌊a + 1⌋ = ⌊a⌋ + 1 := by
   -- Porting note: broken `convert floor_add_int a 1`
   rw [← cast_one, floor_add_int]
@@ -749,11 +776,21 @@ theorem floor_int_add (z : ℤ) (a : α) : ⌊↑z + a⌋ = z + ⌊a⌋ := by
 theorem floor_add_nat (a : α) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n := by rw [← Int.cast_ofNat, floor_add_int]
 #align int.floor_add_nat Int.floor_add_nat
 
+@[simp]
+theorem floor_add_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
+    ⌊a + OfNat.ofNat n⌋ = ⌊a⌋ + OfNat.ofNat n :=
+  floor_add_nat a n
+
 @[simp]
 theorem floor_nat_add (n : ℕ) (a : α) : ⌊↑n + a⌋ = n + ⌊a⌋ := by
   rw [← Int.cast_ofNat, floor_int_add]
 #align int.floor_nat_add Int.floor_nat_add
 
+@[simp]
+theorem floor_ofNat_add (n : ℕ) [n.AtLeastTwo] (a : α) :
+    ⌊OfNat.ofNat n + a⌋ = OfNat.ofNat n + ⌊a⌋ :=
+  floor_nat_add n a
+
 @[simp]
 theorem floor_sub_int (a : α) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z :=
   Eq.trans (by rw [Int.cast_neg, sub_eq_add_neg]) (floor_add_int _ _)
@@ -763,6 +800,13 @@ theorem floor_sub_int (a : α) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z :=
 theorem floor_sub_nat (a : α) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n := by rw [← Int.cast_ofNat, floor_sub_int]
 #align int.floor_sub_nat Int.floor_sub_nat
 
+@[simp] theorem floor_sub_one (a : α) : ⌊a - 1⌋ = ⌊a⌋ - 1 := by exact_mod_cast floor_sub_nat a 1
+
+@[simp]
+theorem floor_sub_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] :
+    ⌊a - OfNat.ofNat n⌋ = ⌊a⌋ - OfNat.ofNat n :=
+  floor_sub_nat a n
+
 theorem abs_sub_lt_one_of_floor_eq_floor {α : Type _} [LinearOrderedCommRing α] [FloorRing α]
     {a b : α} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1 := by
   have : a < ⌊a⌋ + 1 := lt_floor_add_one a
@@ -827,24 +871,47 @@ theorem fract_add_nat (a : α) (m : ℕ) : fract (a + m) = fract a := by
 #align int.fract_add_nat Int.fract_add_nat
 
 @[simp]
-theorem fract_sub_int (a : α) (m : ℤ) : fract (a - m) = fract a := by
-  rw [fract]
-  simp
-#align int.fract_sub_int Int.fract_sub_int
+theorem fract_add_one (a : α) : fract (a + 1) = fract a := by exact_mod_cast fract_add_nat a 1
+
+@[simp]
+theorem fract_add_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] : fract (a + OfNat.ofNat n) = fract a :=
+  fract_add_nat a n
 
 @[simp]
 theorem fract_int_add (m : ℤ) (a : α) : fract (↑m + a) = fract a := by rw [add_comm, fract_add_int]
 #align int.fract_int_add Int.fract_int_add
 
+@[simp]
+theorem fract_nat_add (n : ℕ) (a : α) : fract (↑n + a) = fract a := by rw [add_comm, fract_add_nat]
+
+@[simp]
+theorem fract_one_add (a : α) : fract (1 + a) = fract a := by exact_mod_cast fract_nat_add 1 a
+
+@[simp]
+theorem fract_ofNat_add (n : ℕ) [n.AtLeastTwo] (a : α) : fract (OfNat.ofNat n + a) = fract a :=
+  fract_nat_add n a
+
+@[simp]
+theorem fract_sub_int (a : α) (m : ℤ) : fract (a - m) = fract a := by
+  rw [fract]
+  simp
+#align int.fract_sub_int Int.fract_sub_int
+
 @[simp]
 theorem fract_sub_nat (a : α) (n : ℕ) : fract (a - n) = fract a := by
   rw [fract]
   simp
 #align int.fract_sub_nat Int.fract_sub_nat
 
 @[simp]
-theorem fract_int_nat (n : ℕ) (a : α) : fract (↑n + a) = fract a := by rw [add_comm, fract_add_nat]
-#align int.fract_int_nat Int.fract_int_nat
+theorem fract_sub_one (a : α) : fract (a - 1) = fract a := by exact_mod_cast fract_sub_nat a 1
+
+@[simp]
+theorem fract_sub_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] : fract (a - OfNat.ofNat n) = fract a :=
+  fract_sub_nat a n
+
+-- Was a duplicate lemma under a bad name
+#align int.fract_int_nat Int.fract_int_add
 
 theorem fract_add_le (a b : α) : fract (a + b) ≤ fract a + fract b := by
   rw [fract, fract, fract, sub_add_sub_comm, sub_le_sub_iff_left, ← Int.cast_add, Int.cast_le]
@@ -888,7 +955,7 @@ theorem fract_zero : fract (0 : α) = 0 := by rw [fract, floor_zero, cast_zero,
 theorem fract_one : fract (1 : α) = 0 := by simp [fract]
 #align int.fract_one Int.fract_one
 
-theorem abs_fract : |Int.fract a| = Int.fract a :=
+theorem abs_fract : |fract a| = fract a :=
   abs_eq_self.mpr <| fract_nonneg a
 #align int.abs_fract Int.abs_fract
 
@@ -908,6 +975,9 @@ theorem fract_intCast (z : ℤ) : fract (z : α) = 0 := by
 theorem fract_natCast (n : ℕ) : fract (n : α) = 0 := by simp [fract]
 #align int.fract_nat_cast Int.fract_natCast
 
+@[simp]
+theorem fract_ofNat (n : ℕ) [n.AtLeastTwo] : fract (OfNat.ofNat n : α) = 0 := fract_natCast n
+
 -- porting note: simp can prove this
 -- @[simp]
 theorem fract_floor (a : α) : fract (⌊a⌋ : α) = 0 :=
@@ -1133,6 +1203,9 @@ theorem ceil_natCast (n : ℕ) : ⌈(n : α)⌉ = n :=
   eq_of_forall_ge_iff fun a => by rw [ceil_le, ← cast_ofNat, cast_le]
 #align int.ceil_nat_cast Int.ceil_natCast
 
+@[simp]
+theorem ceil_ofNat (n : ℕ) [n.AtLeastTwo] : ⌈(OfNat.ofNat n : α)⌉ = n := ceil_natCast n
+
 theorem ceil_mono : Monotone (ceil : α → ℤ) :=
   gc_ceil_coe.monotone_l
 #align int.ceil_mono Int.ceil_mono
@@ -1152,6 +1225,10 @@ theorem ceil_add_one (a : α) : ⌈a + 1⌉ = ⌈a⌉ + 1 := by
   rw [←ceil_add_int a (1 : ℤ), cast_one]
 #align int.ceil_add_one Int.ceil_add_one
 
+@[simp]
+theorem ceil_add_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] : ⌈a + OfNat.ofNat n⌉ = ⌈a⌉ + OfNat.ofNat n :=
+  ceil_add_nat a n
+
 @[simp]
 theorem ceil_sub_int (a : α) (z : ℤ) : ⌈a - z⌉ = ⌈a⌉ - z :=
   Eq.trans (by rw [Int.cast_neg, sub_eq_add_neg]) (ceil_add_int _ _)
@@ -1168,6 +1245,10 @@ theorem ceil_sub_one (a : α) : ⌈a - 1⌉ = ⌈a⌉ - 1 := by
   rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]
 #align int.ceil_sub_one Int.ceil_sub_one
 
+@[simp]
+theorem ceil_sub_ofNat (a : α) (n : ℕ) [n.AtLeastTwo] : ⌈a - OfNat.ofNat n⌉ = ⌈a⌉ - OfNat.ofNat n :=
+  ceil_sub_nat a n
+
 theorem ceil_lt_add_one (a : α) : (⌈a⌉ : α) < a + 1 := by
   rw [← lt_ceil, ← Int.cast_one, ceil_add_int]
   apply lt_add_one
@@ -1344,6 +1425,9 @@ theorem round_one : round (1 : α) = 1 := by simp [round]
 theorem round_natCast (n : ℕ) : round (n : α) = n := by simp [round]
 #align round_nat_cast round_natCast
 
+@[simp]
+theorem round_ofNat (n : ℕ) [n.AtLeastTwo] : round (OfNat.ofNat n : α) = n := round_natCast n
+
 @[simp]
 theorem round_intCast (n : ℤ) : round (n : α) = n := by simp [round]
 #align round_int_cast round_intCast
@@ -1374,16 +1458,24 @@ theorem round_sub_one (a : α) : round (a - 1) = round a - 1 := by
 
 @[simp]
 theorem round_add_nat (x : α) (y : ℕ) : round (x + y) = round x + y := by
-  rw [round, round, fract_add_nat, Int.floor_add_nat, Int.ceil_add_nat, ← apply_ite₂, ite_self]
+  exact_mod_cast round_add_int x y
 #align round_add_nat round_add_nat
 
+@[simp]
+theorem round_add_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
+    round (x + OfNat.ofNat n) = round x + OfNat.ofNat n :=
+  round_add_nat x n
+
 @[simp]
 theorem round_sub_nat (x : α) (y : ℕ) : round (x - y) = round x - y := by
-  rw [sub_eq_add_neg, ← Int.cast_ofNat]
-  norm_cast
-  rw [round_add_int, sub_eq_add_neg]
+  exact_mod_cast round_sub_int x y
 #align round_sub_nat round_sub_nat
 
+@[simp]
+theorem round_sub_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
+    round (x - OfNat.ofNat n) = round x - OfNat.ofNat n :=
+  round_sub_nat x n
+
 @[simp]
 theorem round_int_add (x : α) (y : ℤ) : round ((y : α) + x) = y + round x := by
   rw [add_comm, round_add_int, add_comm]
@@ -1394,6 +1486,11 @@ theorem round_nat_add (x : α) (y : ℕ) : round ((y : α) + x) = y + round x :=
   rw [add_comm, round_add_nat, add_comm]
 #align round_nat_add round_nat_add
 
+@[simp]
+theorem round_ofNat_add (n : ℕ) [n.AtLeastTwo] (x : α) :
+    round (OfNat.ofNat n + x) = OfNat.ofNat n + round x :=
+  round_nat_add x n
+
 theorem abs_sub_round_eq_min (x : α) : |x - round x| = min (fract x) (1 - fract x) := by
   simp_rw [round, min_def_lt, two_mul, ← lt_tsub_iff_left]
   cases' lt_or_ge (fract x) (1 - fract x) with hx hx