Homomorphism rules for Fin used by the grind tactic. The injection function is Fin.val.

theorem Lean.Grind.Fin.eq_iff_val_eq {n : Nat} (a b : Fin n) : a = b ↔ ↑a = ↑b

theorem Lean.Grind.Fin.val_ite {n : Nat} (c : Prop) [Decidable c] (x y : Fin n) : ↑(if c then x else y) = if c then ↑x else ↑y

theorem Lean.Grind.Fin.val_OfNat_ofNat (n : Nat) [NeZero n] (a : Nat) : ↑(OfNat.ofNat a) = a % n

Homomorphism predicate: the range fact for Fin.val, instantiated by grind for the terms it internalizes.