case zero
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
⊢ ↑(x ^ Nat.zero) = ↑x ^ Nat.zero

case succ
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
n : ℕ
ih : ↑(x ^ n) = ↑x ^ n
⊢ ↑(x ^ Nat.succ n) = ↑x ^ Nat.succ n
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
n : ℕ
⊢ ↑(x ^ n) = ↑x ^ n
induction' n with n ih
no goals
case zero
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
⊢ ↑(x ^ Nat.zero) = ↑x ^ Nat.zero
simp
no goals
case succ
R✝ : Type u
S : Type v
T : Type w
inst✝⁴ : NonAssocSemiring R✝
M : Submonoid R✝
inst✝³ : SetLike S R✝
hSR : SubsemiringClass S R✝
s : S
R : Type u_1
inst✝² : Semiring R
inst✝¹ : SetLike S R
inst✝ : SubsemiringClass S R
x : { x // x ∈ s }
n : ℕ
ih : ↑(x ^ n) = ↑x ^ n
⊢ ↑(x ^ Nat.succ n) = ↑x ^ Nat.succ n
simp [pow_succ, ih]