no goals
ι : Type u_2
R : Type u_3
A : Type u_1
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : Submonoid A
n : ℕ
⊢ val (Nat.unaryCast n) = ↑n
induction n <;> simp [Nat.unaryCast, zero_val, one_val, *]