-- Mathlib/Data/Complex/Exponential.lean
theorem exp_add : exp (x + y) = exp x * exp y

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
have h₂ := Nat.choose_mul_factorial_mul_factorial (Nat.le_of_lt_succ <| Finset.mem_range.1 hi)

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (x + y) ^ m / ↑m.factorial = ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Tactic:
rw [add_pow, div_eq_mul_inv, sum_mul]

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ ∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * ↑(m.choose i) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
rw [← h₂, Nat.cast_mul, Nat.cast_mul, mul_inv, mul_inv]

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * ((↑(m.choose I))⁻¹ * (↑I.factorial)⁻¹ * (↑(m - I).factorial)⁻¹) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Proof state:
x y : ℂ
⊢ cexp (x + y) = cexp x * cexp y

Tactic:
have hj : ∀ j : ℕ, (∑ m ∈ range j, (x + y) ^ m / m.factorial) =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / k.factorial *
        (y ^ (i - k) / (i - k).factorial) := by
  intro j
  refine Finset.sum_congr rfl fun m _ => ?_
  rw [add_pow, div_eq_mul_inv, sum_mul]
  refine Finset.sum_congr rfl fun I hi => ?_
  have h₁ : (m.choose I : ℂ) ≠ 0 :=
    Nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (Nat.choose_pos (Nat.le_of_lt_succ (mem_range.1 hi))))
  have h₂ := Nat.choose_mul_factorial_mul_factorial (Nat.le_of_lt_succ <| Finset.mem_range.1 hi)
  rw [← h₂, Nat.cast_mul, Nat.cast_mul, mul_inv, mul_inv]
  simp only [mul_left_comm (m.choose I : ℂ), mul_assoc, mul_left_comm (m.choose I : ℂ)⁻¹,
    mul_comm (m.choose I : ℂ)]
  rw [inv_mul_cancel₀ h₁]
  simp [div_eq_mul_inv, mul_comm, mul_assoc, mul_left_comm]

Result:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ cexp (x + y) = cexp x * cexp y

Proof state:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ ⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈
    ⟨fun n => ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩

Tactic:
simp only [hj]

Result:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ ⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈
    ⟨fun n => ∑ i ∈ range n, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial), ⋯⟩

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
have h₁ : (m.choose I : ℂ) ≠ 0 :=
  Nat.cast_ne_zero.2 (pos_iff_ne_zero.1 (Nat.choose_pos (Nat.le_of_lt_succ (mem_range.1 hi))))

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Proof state:
x y : ℂ
⊢ ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)

Tactic:
intro j

Result:
x y : ℂ
j : ℕ
⊢ ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
    ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)

Proof state:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ cexp (x + y) = cexp x * cexp y

Tactic:
simp_rw [exp, exp', lim_mul_lim]

Result:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ CauSeq.lim ⟨fun n => ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩ =
    (⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩).lim

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * 1))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
simp [div_eq_mul_inv, mul_comm, mul_assoc, mul_left_comm]

Result:
no goals

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * ((↑(m.choose I))⁻¹ * (↑I.factorial)⁻¹ * (↑(m - I).factorial)⁻¹) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
simp only [mul_left_comm (m.choose I : ℂ), mul_assoc, mul_left_comm (m.choose I : ℂ)⁻¹,
  mul_comm (m.choose I : ℂ)]

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * ((↑(m.choose I))⁻¹ * ↑(m.choose I))))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Proof state:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ CauSeq.lim ⟨fun n => ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩ =
    (⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩).lim

Tactic:
apply (lim_eq_lim_of_equiv _).symm

Result:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ ⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈
    ⟨fun n => ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩

Proof state:
x y : ℂ
j : ℕ
⊢ ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
    ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)

Tactic:
refine Finset.sum_congr rfl fun m _ => ?_

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (x + y) ^ m / ↑m.factorial = ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ ∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * ↑(m.choose i) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Tactic:
refine Finset.sum_congr rfl fun I hi => ?_

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
⊢ x ^ I * y ^ (m - I) * ↑(m.choose I) * (↑m.factorial)⁻¹ = x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)