[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ ↑(constantCoeff R) (invUnitsSub u) = 1 /ₚ u
[PROOFSTEP]
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ invUnitsSub u * X = invUnitsSub u * ↑(C R) ↑u - 1
[PROOFSTEP]
ext (_ | n)
[GOAL]
case h.zero
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ ↑(coeff R Nat.zero) (invUnitsSub u * X) = ↑(coeff R Nat.zero) (invUnitsSub u * ↑(C R) ↑u - 1)
[PROOFSTEP]
simp
[GOAL]
case h.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
n : ℕ
⊢ ↑(coeff R (Nat.succ n)) (invUnitsSub u * X) = ↑(coeff R (Nat.succ n)) (invUnitsSub u * ↑(C R) ↑u - 1)
[PROOFSTEP]
simp [n.succ_ne_zero, pow_succ]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ invUnitsSub u * (↑(C R) ↑u - X) = 1
[PROOFSTEP]
simp [mul_sub, sub_sub_cancel]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
⊢ ↑(map f) (invUnitsSub u) = invUnitsSub (↑(Units.map ↑f) u)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑(coeff S n✝) (↑(map f) (invUnitsSub u)) = ↑(coeff S n✝) (invUnitsSub (↑(Units.map ↑f) u))
[PROOFSTEP]
simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ ↑f ↑(u ^ (n✝ + 1))⁻¹ = ↑(↑(Units.map ↑f) (u ^ (n✝ + 1)))⁻¹
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(constantCoeff A) (exp A) = 1
[PROOFSTEP]
rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(algebraMap ℚ A) (1 / ↑0!) = 1
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit0 n)) (sin A) = 0
[PROOFSTEP]
rw [sin, coeff_mk, if_pos (even_bit0 n)]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit1 n)) (sin A) = (-1) ^ n * ↑(coeff A (bit1 n)) (exp A)
[PROOFSTEP]
rw [sin, coeff_mk, if_neg n.not_even_bit1, Nat.bit1_div_two, ← mul_one_div, map_mul, map_pow, map_neg, map_one,
  coeff_exp]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit0 n)) (cos A) = (-1) ^ n * ↑(coeff A (bit0 n)) (exp A)
[PROOFSTEP]
rw [cos, coeff_mk, if_pos (even_bit0 n), Nat.bit0_div_two, ← mul_one_div, map_mul, map_pow, map_neg, map_one, coeff_exp]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(coeff A (bit1 n)) (cos A) = 0
[PROOFSTEP]
rw [cos, coeff_mk, if_neg n.not_even_bit1]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(map f) (exp A) = exp A'
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
n✝ : ℕ
⊢ ↑(coeff A' n✝) (↑(map f) (exp A)) = ↑(coeff A' n✝) (exp A')
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(map f) (sin A) = sin A'
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
n✝ : ℕ
⊢ ↑(coeff A' n✝) (↑(map f) (sin A)) = ↑(coeff A' n✝) (sin A')
[PROOFSTEP]
simp [sin, apply_ite f]
[GOAL]
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(map f) (cos A) = cos A'
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
A' : Type u_2
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
n✝ : ℕ
⊢ ↑(coeff A' n✝) (↑(map f) (cos A)) = ↑(coeff A' n✝) (cos A')
[PROOFSTEP]
simp [cos, apply_ite f]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
⊢ ↑(rescale a) (exp A) * ↑(rescale b) (exp A) = ↑(rescale (a + b)) (exp A)
[PROOFSTEP]
ext n
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ↑(coeff A n) (↑(rescale a) (exp A) * ↑(rescale b) (exp A)) = ↑(coeff A n) (↑(rescale (a + b)) (exp A))
[PROOFSTEP]
simp only [coeff_mul, exp, rescale, coeff_mk, MonoidHom.coe_mk, OneHom.coe_mk, coe_mk, factorial,
  Nat.sum_antidiagonal_eq_sum_range_succ_mk, add_pow, sum_mul]
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ (Finset.sum (Finset.range (succ n)) fun x =>
      a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!))) =
    Finset.sum (Finset.range (n + 1)) fun x => a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (succ n) →
      a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
        a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
rintro x hx
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
suffices
  a ^ x * b ^ (n - x) * (algebraMap ℚ A (1 / ↑x.factorial) * algebraMap ℚ A (1 / ↑(n - x).factorial)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n.factorial))
  by convert this using 1 <;> ring
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
this :
  a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_2
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
this :
  a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * ↑(algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!))
[PROOFSTEP]
ring
[GOAL]
case h.e'_3
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
this :
  a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * b ^ (n - x) * ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
[PROOFSTEP]
ring
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ a ^ x * b ^ (n - x) * (↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !))
[PROOFSTEP]
congr 1
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(algebraMap ℚ A) (1 / ↑x !) * ↑(algebraMap ℚ A) (1 / ↑(n - x)!) = ↑(Nat.choose n x) * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
rw [← map_natCast (algebraMap ℚ A) (n.choose x), ← map_mul, ← map_mul]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(algebraMap ℚ A) (1 / ↑x ! * (1 / ↑(n - x)!)) = ↑(algebraMap ℚ A) (↑(Nat.choose n x) * (1 / ↑n !))
[PROOFSTEP]
refine' RingHom.congr_arg _ _
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ 1 / ↑x ! * (1 / ↑(n - x)!) = ↑(Nat.choose n x) * (1 / ↑n !)
[PROOFSTEP]
rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ 1 / (↑x ! * ↑(n - x)!) = ↑(Nat.choose n x) / ↑n !
[PROOFSTEP]
symm
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(Nat.choose n x) / ↑n ! = 1 / (↑x ! * ↑(n - x)!)
[PROOFSTEP]
rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / (↑x ! * ↑(n - x)!)
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ≤ n
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑n ! ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / ↑(x ! * (n - x)!)
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ≤ n
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑n ! ≠ 0
[PROOFSTEP]
rw [cast_div_charZero]
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ! * (n - x)! ∣ n !
[PROOFSTEP]
apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx)
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ x ≤ n
[PROOFSTEP]
apply mem_range_succ_iff.1 hx
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
⊢ ↑n ! ≠ 0
[PROOFSTEP]
rintro h
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
h : ↑n ! = 0
⊢ False
[PROOFSTEP]
apply factorial_ne_zero n
[GOAL]
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range (succ n)
h : ↑n ! = 0
⊢ n ! = 0
[PROOFSTEP]
rw [cast_eq_zero.1 h]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A * ↑evalNegHom (exp A) = 1
[PROOFSTEP]
convert exp_mul_exp_eq_exp_add (1 : A) (-1)
[GOAL]
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A = ↑(rescale 1) (exp A)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 = ↑(rescale (1 + -1)) (exp A)
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
⊢ exp A ^ k = ↑(rescale ↑k) (exp A)
[PROOFSTEP]
induction' k with k h
[GOAL]
case zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A ^ zero = ↑(rescale ↑zero) (exp A)
[PROOFSTEP]
simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero, zero_eq, pow_zero (exp A),
  coe_comp]
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (Finset.sum (Finset.range n) fun k => exp A ^ k) =
    mk fun p => Finset.sum (Finset.range n) fun k => ↑(k ^ p) * ↑(algebraMap ℚ A) (↑p !)⁻¹
[PROOFSTEP]
simp only [exp_pow_eq_rescale_exp, rescale]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (Finset.sum (Finset.range n) fun x =>
      ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                    map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (f g : PowerSeries A),
                      OneHom.toFun
                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                          (f * g) =
                        OneHom.toFun
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                            f *
                          OneHom.toFun
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                            g) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{
                        toOneHom :=
                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (f g : PowerSeries A),
                              OneHom.toFun
                                  { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                    map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                  (f * g) =
                                OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    f *
                                  OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    g) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x_1 y : PowerSeries A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : PowerSeries A),
                                OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      g) })
                      (x_1 + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : PowerSeries A),
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        g) })
                        x_1 +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : PowerSeries A),
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        g) })
                        y) }
        (exp A)) =
    mk fun p => Finset.sum (Finset.range n) fun x => ↑(x ^ p) * ↑(algebraMap ℚ A) (↑p !)⁻¹
[PROOFSTEP]
ext
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n n✝ : ℕ
⊢ ↑(coeff A n✝)
      (Finset.sum (Finset.range n) fun x =>
        ↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (f g : PowerSeries A),
                        OneHom.toFun
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                            (f * g) =
                          OneHom.toFun
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                              f *
                            OneHom.toFun
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                              g) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                              map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (f g : PowerSeries A),
                                OneHom.toFun
                                    { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                      map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                    (f * g) =
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      f *
                                    OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      g) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x_1 y : PowerSeries A),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (f g : PowerSeries A),
                                  OneHom.toFun
                                      { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                        map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                      (f * g) =
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        f *
                                      OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        g) })
                        (x_1 + y) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                  map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : PowerSeries A),
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          g) })
                          x_1 +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                  map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (f g : PowerSeries A),
                                    OneHom.toFun
                                        { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                          map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                        (f * g) =
                                      OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          f *
                                        OneHom.toFun
                                          { toFun := fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f,
                                            map_one' := (_ : (fun f => mk fun n => ↑x ^ n * ↑(coeff A n) f) 1 = 1) }
                                          g) })
                          y) }
          (exp A)) =
    ↑(coeff A n✝) (mk fun p => Finset.sum (Finset.range n) fun x => ↑(x ^ p) * ↑(algebraMap ℚ A) (↑p !)⁻¹)
[PROOFSTEP]
simp only [one_div, coeff_mk, cast_pow, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, coeff_exp, factorial,
  LinearMap.map_sum]
