Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(ofPowerSeries Γ R) PowerSeries.X ^ n = ↑(single ↑n) 1
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(ofPowerSeries Γ R) (PowerSeries.X ^ n) = ↑(single ↑n) 1
rw [RingHom.map_pow]
case zero
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
⊢ ↑(ofPowerSeries Γ R) PowerSeries.X ^ Nat.zero = ↑(single ↑Nat.zero) 1

case succ
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
ih : ↑(ofPowerSeries Γ R) PowerSeries.X ^ n = ↑(single ↑n) 1
⊢ ↑(ofPowerSeries Γ R) PowerSeries.X ^ Nat.succ n = ↑(single ↑(Nat.succ n)) 1
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(ofPowerSeries Γ R) PowerSeries.X ^ n = ↑(single ↑n) 1
induction' n with n ih
no goals
case succ
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
ih : ↑(ofPowerSeries Γ R) PowerSeries.X ^ n = ↑(single ↑n) 1
⊢ ↑(ofPowerSeries Γ R) PowerSeries.X ^ Nat.succ n = ↑(single ↑(Nat.succ n)) 1
. rw [pow_succ, pow_succ, ih, ofPowerSeries_X, mul_comm, single_mul_single, one_mul,
    Nat.cast_succ, add_comm]
case zero
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
⊢ 1 = ↑(single 0) 1
case zero
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
⊢ ↑(ofPowerSeries Γ R) PowerSeries.X ^ Nat.zero = ↑(single ↑Nat.zero) 1
simp
no goals
case zero
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
⊢ 1 = ↑(single 0) 1
rfl
no goals
case succ
Γ : Type u_2
R✝ : Type ?u.2401544
inst✝² : Semiring R✝
inst✝¹ : StrictOrderedSemiring Γ
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
ih : ↑(ofPowerSeries Γ R) PowerSeries.X ^ n = ↑(single ↑n) 1
⊢ ↑(ofPowerSeries Γ R) PowerSeries.X ^ Nat.succ n = ↑(single ↑(Nat.succ n)) 1
rw [pow_succ, pow_succ, ih, ofPowerSeries_X, mul_comm, single_mul_single, one_mul,
  Nat.cast_succ, add_comm]