-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem exp_mul_exp_eq_exp_add [Algebra ℚ A] (a b : A) :
    rescale a (exp A) * rescale b (exp A) = rescale (a + b) (exp A)

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / (↑x ! * ↑(n - x)!)

Tactic:
norm_cast

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / ↑(x ! * (n - x)!)

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ 1 / (↑x ! * ↑(n - x)!) = ↑(n.choose x) / ↑n !

Tactic:
symm

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n.choose x) / ↑n ! = 1 / (↑x ! * ↑(n - x)!)

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / ↑(x ! * (n - x)!)

Tactic:
rw [cast_div_charZero]

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ x ! * (n - x)! ∣ n !

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ x ≤ n

Tactic:
apply mem_range_succ_iff.1 hx

Result:
no goals

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑n ! ≠ 0

Tactic:
rintro h

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ False

Proof state:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∑ x ∈ Finset.range n.succ, a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    ∑ x ∈ Finset.range (n + 1), a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
apply sum_congr rfl

Result:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∀ x ∈ Finset.range n.succ,
    a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
      a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Proof state:
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))

Tactic:
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]

Result:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∑ x ∈ Finset.range n.succ, a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    ∑ x ∈ Finset.range (n + 1), a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n.choose x) / ↑n ! = 1 / (↑x ! * ↑(n - x)!)

Tactic:
rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(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 n.succ
⊢ 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 n.succ
⊢ ↑n ! ≠ 0

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!) = ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
rw [← map_natCast (algebraMap ℚ A) (n.choose x), ← map_mul, ← map_mul]

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (algebraMap ℚ A) (1 / ↑x ! * (1 / ↑(n - x)!)) = (algebraMap ℚ A) (↑(n.choose x) * (1 / ↑n !))

Proof state:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
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

Result:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))

Proof state:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))

Tactic:
congr 1

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!) = ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (algebraMap ℚ A) (1 / ↑x ! * (1 / ↑(n - x)!)) = (algebraMap ℚ A) (↑(n.choose x) * (1 / ↑n !))

Tactic:
refine RingHom.congr_arg _ ?_

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ 1 / ↑x ! * (1 / ↑(n - x)!) = ↑(n.choose x) * (1 / ↑n !)

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ 1 / ↑x ! * (1 / ↑(n - x)!) = ↑(n.choose x) * (1 / ↑n !)

Tactic:
rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div]

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ 1 / (↑x ! * ↑(n - x)!) = ↑(n.choose x) / ↑n !

Proof state:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∀ x ∈ Finset.range n.succ,
    a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
      a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
rintro x hx

Result:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Proof state:
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)

Tactic:
ext n

Result:
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))

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ False

Tactic:
apply factorial_ne_zero n

Result:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ n ! = 0