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))
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)
ext n
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 !)
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))
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]
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 !)
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 !)
apply sum_congr rfl
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 !)
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 !)
rintro x hx
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 !))
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 !)
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
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 !)
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 !))
congr 1
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 !))
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 !)
rw [← map_natCast (algebraMap ℚ A) (n.choose x), ← map_mul, ← map_mul]
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 !)
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 !))
refine' RingHom.congr_arg _ _
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 !
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 !)
rw [mul_one_div (↑(n.choose x) : ℚ), one_div_mul_one_div]
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)!)
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 !
symm
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
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)!)
rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial]
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
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
norm_cast
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 !

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
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
rw [cast_div_charZero]
no goals
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 !)
convert this using 1 <;> ring
no goals
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 !
apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx)
no goals
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
apply mem_range_succ_iff.1 hx
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
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
rintro h
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
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
apply factorial_ne_zero n
no goals
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
rw [cast_eq_zero.1 h]