permu

Stream: mathlib4

[vxctyxeha]

Why can't it be called natCast_modEq_iff at the end of the line

import Mathlib
open List
open Nat
open Int

theorem rearrange_digits_diff_divisible_by_9
    (m m' : ℕ)(h_digits_perm : (Nat.digits 10 m').Perm (Nat.digits 10 m)) :
    (9 : ℤ) ∣ (m : ℤ) - (m' : ℤ) := by
  simp [@Int.modEq_comm,← @Int.modEq_iff_dvd]
  have h_m_mod_sum : m ≡ (Nat.digits 10 m).sum [MOD 9] := by
     exact modEq_nine_digits_sum m
  have h_m'_mod_sum : m' ≡ (Nat.digits 10 m').sum [MOD 9] := by
     exact modEq_nine_digits_sum m'
  have h_sum_eq : (Nat.digits 10 m').sum = (Nat.digits 10 m).sum :=
      List.Perm.sum_eq h_digits_perm
  rw [h_sum_eq] at h_m'_mod_sum
  have h_nat_modEq : m ≡ m' [MOD 9] := by
    apply Nat.ModEq.trans h_m_mod_sum
    exact id (ModEq.symm h_m'_mod_sum)
  rw [natCast_modEq_iff]

[Yury G. Kudryashov]

Please minimize your example by calling extract_goal so that we can see the proof state at the exact point of interest.

[Aaron Liu]

The problem is that (9 : ℤ) isn't unifying with (Nat.cast _ : ℤ), it works if you change it to (Nat.cast 9 : ℤ).

[Aaron Liu]

Specifically, change m ≡ m' [ZMOD Nat.cast 9]