Nat -> ZMod n -> ZMod m

Stream: Is there code for X?

[Michael Stoll]

This should be in mathlib, but I can't find it:

lemma foo {m n : ℕ} (h : m ∣ n) (a : ℕ) : ((a : ZMod n) : ZMod m) = (a : ZMod m)

or equivalently,

lemma bar {m n : ℕ} (h : m ∣ n) : (ZMod.cast : ZMod n → ZMod m) ∘ (Nat.cast : ℕ → ZMod n) = Nat.cast

Any ideas where it is hiding?

[Ruben Van de Velde]

ZMod.cast_nat_cast h

[Michael Stoll]

Found it:

lemma foo {m n : ℕ} (h : m ∣ n) (a : ℕ) : ((a : ZMod n) : ZMod m) = (a : ZMod m) :=
  ZMod.cast_nat_cast h a

(by apply? returned, among others, refine ZMod.cast_nat_cast ?h a, which, however, does not work when pasted in. Replacing ?h by h does it. Why does apply? not do that, too?)

[Michael Stoll]

BTW, ZMod.cast_nat_cast h does not work as a proof of bar.

[Ruben Van de Velde]

lemma bar {m n : ℕ} (h : m ∣ n) : (ZMod.cast : ZMod n → ZMod m) ∘ (Nat.cast : ℕ → ZMod n) = Nat.cast :=
  funext <| ZMod.cast_nat_cast h