Theorem: mod_cast_eq_cast_mod (FormalSnarksProject/ToMathlib/ForTransformations.lean)

State before:
F : Type
inst✝ : Field F
a b : ℕ
⊢ ↑a % ↑b = ↑(a % b)
Tactic:
exact rfl
State after:
no goals