case zero
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
⊢ ↑(of A i) a ^ Nat.zero = ↑(of A (Nat.zero • i)) (GradedMonoid.GMonoid.gnpow Nat.zero a)

case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ ↑(of A i) a ^ Nat.succ n = ↑(of A (Nat.succ n • i)) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a)
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
⊢ ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
induction' n with n n_ih
no goals
case zero
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
⊢ ↑(of A i) a ^ Nat.zero = ↑(of A (Nat.zero • i)) (GradedMonoid.GMonoid.gnpow Nat.zero a)
exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ ↑(of A (i + n • i)) (GradedMonoid.GMul.mul a (GradedMonoid.GMonoid.gnpow n a)) =
    ↑(of A (Nat.succ n • i)) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a)
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ ↑(of A i) a ^ Nat.succ n = ↑(of A (Nat.succ n • i)) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a)
rw [pow_succ, n_ih, of_mul_of a]
no goals
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ ↑(of A (i + n • i)) (GradedMonoid.GMul.mul a (GradedMonoid.GMonoid.gnpow n a)) =
    ↑(of A (Nat.succ n • i)) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a)
exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm