no goals
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ mk i a ^ n = mk (n • i) (GMonoid.gnpow n a)
match n with
| 0 =>
  rw [pow_zero]
  exact (GMonoid.gnpow_zero' ⟨_, a⟩).symm
| n+1 =>
  rw [pow_succ, mk_pow a n, mk_mul_mk]
  exact (GMonoid.gnpow_succ' n ⟨_, a⟩).symm
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ 1 = mk (0 • i) (GMonoid.gnpow 0 a)
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ mk i a ^ 0 = mk (0 • i) (GMonoid.gnpow 0 a)
rw [pow_zero]
no goals
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ 1 = mk (0 • i) (GMonoid.gnpow 0 a)
exact (GMonoid.gnpow_zero' ⟨_, a⟩).symm
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n✝ n : ℕ
⊢ mk (i + n • i) (GMul.mul a (GMonoid.gnpow n a)) = mk ((n + 1) • i) (GMonoid.gnpow (n + 1) a)
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n✝ n : ℕ
⊢ mk i a ^ (n + 1) = mk ((n + 1) • i) (GMonoid.gnpow (n + 1) a)
rw [pow_succ, mk_pow a n, mk_mul_mk]
no goals
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n✝ n : ℕ
⊢ mk (i + n • i) (GMul.mul a (GMonoid.gnpow n a)) = mk ((n + 1) • i) (GMonoid.gnpow (n + 1) a)
exact (GMonoid.gnpow_succ' n ⟨_, a⟩).symm