From 58e967b79828f5b4cf91157f9a88577bf3baaff2 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 18 Jul 2023 13:58:38 +0000 Subject: [PATCH] fix: coercions in ZMod.coe_add_eq_ite (#5981) The change in behaviour of coercions in mathlib4 meant that this lemma was translated incorrectly (into a much simpler statement). --- Mathlib/Data/ZMod/Basic.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index 9ecfbe90b8a03..007bbcfa5a644 100644 --- a/Mathlib/Data/ZMod/Basic.lean +++ b/Mathlib/Data/ZMod/Basic.lean @@ -266,14 +266,16 @@ theorem int_cast_cast (i : ZMod n) : ((i : ℤ) : R) = i := #align zmod.int_cast_cast ZMod.int_cast_cast theorem coe_add_eq_ite {n : ℕ} (a b : ZMod n) : - (↑(a + b) : ℤ) = if (n : ℤ) ≤ a + b then a + b - n else a + b := by - cases n - · simp - simp only [Fin.val_add_eq_ite, ← Int.ofNat_add, ← Int.ofNat_succ, Int.ofNat_le] + (↑(a + b) : ℤ) = if (n : ℤ) ≤ a + b then (a : ℤ) + b - n else a + b := by + cases' n with n + · simp; rfl + change Fin (n + 1) at a b + change ((((a + b) : Fin (n + 1)) : ℕ) : ℤ) = if ((n + 1 : ℕ) : ℤ) ≤ (a : ℕ) + b then _ else _ + simp only [Fin.val_add_eq_ite, Int.ofNat_succ, Int.ofNat_le] + norm_cast split_ifs with h - · norm_cast + · rw [Nat.cast_sub h] congr - simp · rfl #align zmod.coe_add_eq_ite ZMod.coe_add_eq_ite