From bc2aae380ce8e75d40f8bb40d8670b11dbff467f Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 14 Nov 2025 14:35:47 +0100
Subject: [PATCH] feat: add lemmas about Int range sizes (#11159)

This PR adds lemmas about the sizes of ranges of Ints, analogous to the
Nat lemmas in `Init.Data.Range.Polymorphic.NatLemmas`. See also
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Reasonning.20about.20PRange.20sizes.20.28with.20.60Int.60.29/with/546466339.

Closes #11158

---------

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
---
 src/Init/Data/Range/Polymorphic.lean          |  1 +
 .../Data/Range/Polymorphic/IntLemmas.lean     | 39 +++++++++++++++++++
 2 files changed, 40 insertions(+)
 create mode 100644 src/Init/Data/Range/Polymorphic/IntLemmas.lean

diff --git a/src/Init/Data/Range/Polymorphic.lean b/src/Init/Data/Range/Polymorphic.lean
index f6bfd45170..4893f752d9 100644
--- a/src/Init/Data/Range/Polymorphic.lean
+++ b/src/Init/Data/Range/Polymorphic.lean
@@ -18,6 +18,7 @@ public import Init.Data.Range.Polymorphic.UInt
 public import Init.Data.Range.Polymorphic.SInt
 
 public import Init.Data.Range.Polymorphic.NatLemmas
+public import Init.Data.Range.Polymorphic.IntLemmas
 public import Init.Data.Range.Polymorphic.GetElemTactic
 
 public section
diff --git a/src/Init/Data/Range/Polymorphic/IntLemmas.lean b/src/Init/Data/Range/Polymorphic/IntLemmas.lean
new file mode 100644
index 0000000000..047982cbb9
--- /dev/null
+++ b/src/Init/Data/Range/Polymorphic/IntLemmas.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Bentkamp
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Int
+public import Init.Data.Range.Polymorphic.Lemmas
+
+public section
+
+namespace Std.PRange.Int
+
+@[simp]
+theorem size_rco {a b : Int} :
+    (a...b).size = (b - a).toNat := by
+  simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size]
+  omega
+
+@[simp]
+theorem size_rcc {a b : Int} :
+    (a...=b).size = (b + 1 - a).toNat := by
+  simp [Rcc.size, Rxc.HasSize.size]
+
+@[simp]
+theorem size_roc {a b : Int} :
+    (a<...=b).size = (b - a).toNat := by
+  simp only [Roc.size, Rxc.HasSize.size]
+  omega
+
+@[simp]
+theorem size_roo {a b : Int} :
+    (a<...b).size = (b - a - 1).toNat := by
+  simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size]
+  omega
+
+end Std.PRange.Int