Cannot use `Nat.ModEq.pow_totient` (Euler's theorem)

Stream: mathlib4

[ElCondor]

I'm trying to use Euler's theorem, as implemented in https://github.com/leanprover-community/mathlib4/blob/7766bcc46ae69e55b32297edb59448f2e1fe1dde/Mathlib/FieldTheory/Finite/Basic.lean#L474

However, even using it in the most basic form doesn't seem to work: see here.

It looks like rw is looking for an expression like x ^ φ n % n and won't accept something like x ^ φ n ≡ 1 [MOD n].

What am I doing wrong?

[Kevin Buzzard]

The rw tactic will only eat theorems of the form A = B or A ↔ B. And when it eats one of these, it will change all As to Bs. You don't have this set-up, because you have a congruence, not an equality. You could turn it into an equality in $\Z/n\Z$, but Lean is picky about these things.

example {x n : ℕ} (h0 : Coprime x n) : x ^ φ n ≡ 1 [MOD n] := by
  apply Nat.ModEq.pow_totient h0

[ElCondor]

Kevin Buzzard said:

The rw tactic will only eat theorems of the form A = B or A ↔ B. And when it eats one of these, it will change all As to Bs. You don't have this set-up, because you have a congruence, not an equality. You could turn it into an equality in $\Z/n\Z$, but Lean is picky about these things.

example {x n : ℕ} (h0 : Coprime x n) : x ^ φ n ≡ 1 [MOD n] := by
  apply Nat.ModEq.pow_totient h0

OK I understand.

I switched to using ZMod instead, and I was able to prove a part of what I want (proving a result related to RSA) using these: see live.

Now using eq0 : (M ^ e) ^ d = M (in terms of (ZMod (p * q))ˣ objects) I'd like to switch back to m = ((m ^ e) ^ d) % (p * q) (in terms of integers).

I guess that involves coercions at some point but honestly I have no idea how to proceed. Would someone be able to help me? (regarding the first case of by_cases only, I'll try to implement the other one on my own)

[Kevin Buzzard]

    {
      let M : Units (ZMod (p * q)) := ZMod.unitOfCoprime _ h
      have eq0 : (M ^ e) ^ d = M := by calc
        (M ^ e) ^ d = M ^ (e * d)               := by rw [<-pow_mul]
            _       = M ^ (1 + φ (p * q) * k)   := by rw [hde]
            _       = M * (M ^ φ (p * q)) ^ k   := by rw [pow_add, pow_one, pow_mul]
            _       = M                         := by rw [ZMod.pow_totient M]; simp
      -- eq0 is an equality in (Z/pqZ)^*. Change it to an equality in Z/pqZ
      replace eq0 := congrArg Units.val eq0
      -- now move the "invisible to mathematicians" map from (Z/pqZ)^* to Z/pqZ so that
      -- it applies directly to M, not (M^e)^d
      push_cast at eq0
      -- Now turn M back into m
      simp only [unitOfCoprime] at eq0
      -- now move the "invisible to mathematicians" map from Z to Z/pqZ so it applies
      -- to (m^e)^d not m
      norm_cast at eq0
      -- now use the lemma saying (↑a : ZMod n) = (↑b : ZMod n) ↔ a % n = b % n
      rw [nat_cast_eq_nat_cast_iff'] at eq0
      -- and now we can rewrite it in the goal
      rw [eq0]
      -- and finally apply the lemma saying a % b = a if a < b
      exact (mod_eq_of_lt hm).symm
    }

This really is harder than it should be, but there's my effort.