case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A ^ zero = ↑(rescale ↑zero) (exp A)

case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = ↑(rescale ↑k) (exp A)
⊢ exp A ^ succ k = ↑(rescale ↑(succ k)) (exp A)
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
⊢ exp A ^ k = ↑(rescale ↑k) (exp A)
induction' k with k h
no goals
case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A ^ zero = ↑(rescale ↑zero) (exp A)
simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero, zero_eq,
  pow_zero (exp A), coe_comp]
no goals
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = ↑(rescale ↑k) (exp A)
⊢ exp A ^ succ k = ↑(rescale ↑(succ k)) (exp A)
simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one,
id_apply, rescale_one] using pow_succ' (exp A) k