Rat isInt

Stream: lean4

[Matthew Pocock]

[sorry - posted to wrong stream- I have reposted in mathlib4 but can't move or delete from here]

I was reading through the Rat source, and noticed that it defines isInt but then seems to not use it much of anywhere. Is this to avoid needing to constantly unfold the definition? Could this be "fixed" by marking it as simp? While playing about, I also proved the following trivial things that I couldn't see in the library but which I may have overlooked. Are they worth adding, potentially as simp rules? Not sure if I've followed the naming convention or style guide.

/--!
Some theorems describing cases where ℚ corresponds to ℤ.
-/

theorem isInt_ofInt (i : ℤ) : (Rat.ofInt i).isInt = true := by
    simp only [Rat.isInt, Rat.ofInt]

theorem floor_eq_self_if_isInt (a : ℚ) : a.isInt → a.floor = a := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.floor, Int.cast_ite]
    intro ha1
    simp [ha1, ← den_eq_one_iff a]

theorem ceil_eq_self_if_isInt (a : ℚ) : a.isInt → a.ceil = a := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.ceil, Int.cast_ite, Int.cast_add, Int.cast_one]
    intro ha1
    simp [ha1, ← den_eq_one_iff a]

theorem sum_isInt (a b : ℚ) : a.isInt → b.isInt → (a + b).isInt := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.add_def]
    intro ha hb
    simp only [hb, Nat.cast_one, mul_one, ha]
    simp [Rat.normalize]

theorem sub_isInt (a b : ℚ) : a.isInt → b.isInt → (a - b).isInt := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.sub_def]
    intro ha hb
    simp only [hb, Nat.cast_one, mul_one, ha]
    simp [Rat.normalize]

theorem mul_isInt (a b : ℚ) : a.isInt → b.isInt → (a * b).isInt := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.mul_def]
    intro ha hb
    simp only [ha, hb, mul_one]
    simp [Rat.normalize]