case zero
R : Type u_1
inst✝¹⁵ : Ring R
R₂ : Type ?u.888280
inst✝¹⁴ : Ring R₂
R₃ : Type ?u.888286
inst✝¹³ : Ring R₃
M : Type ?u.888292
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommGroup M
M₂ : Type ?u.888301
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommGroup M₂
M₃ : Type ?u.888310
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommGroup M₃
M₄ : Type ?u.888319
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
c : R
⊢ smulRight 1 c ^ Nat.zero = smulRight 1 (c ^ Nat.zero)

case succ
R : Type u_1
inst✝¹⁵ : Ring R
R₂ : Type ?u.888280
inst✝¹⁴ : Ring R₂
R₃ : Type ?u.888286
inst✝¹³ : Ring R₃
M : Type ?u.888292
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommGroup M
M₂ : Type ?u.888301
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommGroup M₂
M₃ : Type ?u.888310
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommGroup M₃
M₄ : Type ?u.888319
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
c : R
n : ℕ
ihn : smulRight 1 c ^ n = smulRight 1 (c ^ n)
⊢ smulRight 1 c ^ Nat.succ n = smulRight 1 (c ^ Nat.succ n)
R : Type u_1
inst✝¹⁵ : Ring R
R₂ : Type ?u.888280
inst✝¹⁴ : Ring R₂
R₃ : Type ?u.888286
inst✝¹³ : Ring R₃
M : Type ?u.888292
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommGroup M
M₂ : Type ?u.888301
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommGroup M₂
M₃ : Type ?u.888310
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommGroup M₃
M₄ : Type ?u.888319
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
c : R
n : ℕ
⊢ smulRight 1 c ^ n = smulRight 1 (c ^ n)
induction' n with n ihn
case zero.h
R : Type u_1
inst✝¹⁵ : Ring R
R₂ : Type ?u.888280
inst✝¹⁴ : Ring R₂
R₃ : Type ?u.888286
inst✝¹³ : Ring R₃
M : Type ?u.888292
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommGroup M
M₂ : Type ?u.888301
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommGroup M₂
M₃ : Type ?u.888310
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommGroup M₃
M₄ : Type ?u.888319
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
c : R
⊢ ↑(smulRight 1 c ^ Nat.zero) 1 = ↑(smulRight 1 (c ^ Nat.zero)) 1
case zero
R : Type u_1
inst✝¹⁵ : Ring R
R₂ : Type ?u.888280
inst✝¹⁴ : Ring R₂
R₃ : Type ?u.888286
inst✝¹³ : Ring R₃
M : Type ?u.888292
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommGroup M
M₂ : Type ?u.888301
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommGroup M₂
M₃ : Type ?u.888310
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommGroup M₃
M₄ : Type ?u.888319
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
c : R
⊢ smulRight 1 c ^ Nat.zero = smulRight 1 (c ^ Nat.zero)
ext
no goals
case zero.h
R : Type u_1
inst✝¹⁵ : Ring R
R₂ : Type ?u.888280
inst✝¹⁴ : Ring R₂
R₃ : Type ?u.888286
inst✝¹³ : Ring R₃
M : Type ?u.888292
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommGroup M
M₂ : Type ?u.888301
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommGroup M₂
M₃ : Type ?u.888310
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommGroup M₃
M₄ : Type ?u.888319
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
c : R
⊢ ↑(smulRight 1 c ^ Nat.zero) 1 = ↑(smulRight 1 (c ^ Nat.zero)) 1
simp
no goals
case succ
R : Type u_1
inst✝¹⁵ : Ring R
R₂ : Type ?u.888280
inst✝¹⁴ : Ring R₂
R₃ : Type ?u.888286
inst✝¹³ : Ring R₃
M : Type ?u.888292
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommGroup M
M₂ : Type ?u.888301
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommGroup M₂
M₃ : Type ?u.888310
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommGroup M₃
M₄ : Type ?u.888319
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
c : R
n : ℕ
ihn : smulRight 1 c ^ n = smulRight 1 (c ^ n)
⊢ smulRight 1 c ^ Nat.succ n = smulRight 1 (c ^ Nat.succ n)
rw [pow_succ, ihn, mul_def, smulRight_comp, smul_eq_mul, pow_succ']