awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
h :
  ∀ (hj : HAdd.hAdd (α := ℕ) 0 1 ≥ 1),
    ‖HSub.hSub (α := ℂ) (∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
have h₁ : ∀ (j : ℕ)
  (ih :
    ∀ (hj : j + 1 ≥ 1), ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0)
  (hj : j + 1 + 1 ≥ 1),
  ‖HSub.hSub (α := ℂ) (∑ m ∈ range (j + 1 + 1), HPow.hPow (α := ℂ) 0 m / (↑m.factorial : ℂ)) 1‖ = 0
Tactic: induction j with
    | zero => simp
    | succ j ih =>
      rw [← ih (by simp)]
      simp only [sum_range_succ, pow_succ]
      simp
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
j : ℕ
⊢ Eq (α := ℂ) (∑ 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 : ℂ)))
have refine : ∀ m ∈ range j,
  (x + y) ^ m / (↑m.factorial : ℂ) =
    ∑ k ∈ range (m + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (m - k) / (↑(m - k).factorial : ℂ))
Tactic: refine Finset.sum_congr rfl fun m _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
⊢ (x + y) ^ m / (↑m.factorial : ℂ) =
    ∑ k ∈ range (m + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (m - k) / (↑(m - k).factorial : ℂ))
have rw : Eq (α := ℂ) (∑ 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: rw [add_pow, div_eq_mul_inv, sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
⊢ Eq (α := ℂ) (∑ 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 : ℂ)))
have refine : ∀ (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: refine Finset.sum_congr rfl fun I hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x y : ℂ
j m : ℕ
h : 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 : ℂ))
have h₁ : Ne (α := ℂ) (↑(m.choose I) : ℂ) 0
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))))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : Ne (α := ℂ) (↑(m.choose I) : ℂ) 0
⊢ x ^ I * y ^ (m - I) * (↑(m.choose I) : ℂ) * (↑m.factorial : ℂ)⁻¹ =
    x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))
have h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
Tactic: have h₂ := Nat.choose_mul_factorial_mul_factorial (Nat.le_of_lt_succ <| Finset.mem_range.1 hi)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : Ne (α := ℂ) (↑(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 : ℂ))
have rw : x ^ I * y ^ (m - I) * (↑(m.choose I) : ℂ) *
    (HMul.hMul (α := ℂ) (↑(m.choose I) : ℂ)⁻¹ (↑I.factorial : ℂ)⁻¹ * (↑(m - I).factorial : ℂ)⁻¹) =
  x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))
Tactic: rw [← h₂, Nat.cast_mul, Nat.cast_mul, mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : Ne (α := ℂ) (↑(m.choose I) : ℂ) 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * y ^ (m - I) * (↑(m.choose I) : ℂ) *
      (HMul.hMul (α := ℂ) (↑(m.choose I) : ℂ)⁻¹ (↑I.factorial : ℂ)⁻¹ * (↑(m - I).factorial : ℂ)⁻¹) =
    x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))
have simp : x ^ I *
    (y ^ (m - I) *
      ((↑I.factorial : ℂ)⁻¹ *
        ((↑(m - I).factorial : ℂ)⁻¹ * HMul.hMul (α := ℂ) (↑(m.choose I) : ℂ)⁻¹ (↑(m.choose I) : ℂ)))) =
  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 : ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
j m : ℕ
h : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : Ne (α := ℂ) (↑(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 : ℂ)⁻¹ * HMul.hMul (α := ℂ) (↑(m.choose I) : ℂ)⁻¹ (↑(m.choose I) : ℂ)))) =
    x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))
have rw : x ^ I * (y ^ (m - I) * ((↑I.factorial : ℂ)⁻¹ * HMul.hMul (α := ℂ) (↑(m - I).factorial : ℂ)⁻¹ 1)) =
  x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))
Tactic: rw [inv_mul_cancel₀ h₁]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x y : ℂ
⊢ cexp (x + y) = cexp x * cexp y
have hj : ∀ (j : ℕ),
  Eq (α := ℂ) (∑ 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: 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_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
hj :
  ∀ (j : ℕ),
    Eq (α := ℂ) (∑ 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
have simp_rw : lim
    (Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
      (fun (n : ℕ) ↦ ∑ m ∈ range n, (x + y) ^ m / (↑m.factorial : ℂ)) sorry) =
  (Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
        (fun (n : ℕ) ↦ ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)) sorry *
      Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
        (fun (n : ℕ) ↦ ∑ m ∈ range n, y ^ m / (↑m.factorial : ℂ)) sorry).lim
Tactic: simp_rw [exp, exp', lim_mul_lim]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
hj :
  ∀ (j : ℕ),
    Eq (α := ℂ) (∑ 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 : ℂ)))
⊢ lim
      (Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
        (fun (n : ℕ) ↦ ∑ m ∈ range n, (x + y) ^ m / (↑m.factorial : ℂ)) ⋯) =
    (Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
          (fun (n : ℕ) ↦ ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)) ⋯ *
        Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
          (fun (n : ℕ) ↦ ∑ m ∈ range n, y ^ m / (↑m.factorial : ℂ)) ⋯).lim
have apply : Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
      (fun (n : ℕ) ↦ ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)) sorry *
    Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
      (fun (n : ℕ) ↦ ∑ m ∈ range n, y ^ m / (↑m.factorial : ℂ)) sorry ≈
  Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
    (fun (n : ℕ) ↦ ∑ m ∈ range n, (x + y) ^ m / (↑m.factorial : ℂ)) sorry
Tactic: apply (lim_eq_lim_of_equiv _).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℂ
hj :
  ∀ (j : ℕ),
    Eq (α := ℂ) (∑ 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 : ℂ)))
⊢ Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
        (fun (n : ℕ) ↦ ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)) ⋯ *
      Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
        (fun (n : ℕ) ↦ ∑ m ∈ range n, y ^ m / (↑m.factorial : ℂ)) ⋯ ≈
    Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
      (fun (n : ℕ) ↦ ∑ m ∈ range n, (x + y) ^ m / (↑m.factorial : ℂ)) ⋯
have simp : Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
      (fun (n : ℕ) ↦ ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)) sorry *
    Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
      (fun (n : ℕ) ↦ ∑ m ∈ range n, y ^ m / (↑m.factorial : ℂ)) sorry ≈
  Subtype.mk (p := fun (f : ℕ → ℂ) ↦ IsCauSeq (α := ℝ) (fun (x : ℂ) ↦ ‖x‖) f)
    (fun (n : ℕ) ↦
      ∑ i ∈ range n, ∑ k ∈ range (i + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (i - k) / (↑(i - k).factorial : ℂ)))
    sorry
Tactic: simp only [hj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x a p : ℂ
n : ℕ
⊢ cexp (a * (↑n : ℂ) * x / p) = cexp (a * x / p) ^ n
have rw : cexp (a * (↑n : ℂ) * x / p) = cexp (n • (a * x / p))
Tactic: rw [← Complex.exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
⊢ cexp ((↑0 : ℂ) * x) = HPow.hPow (β := ℕ) (cexp x) 0
have rw : cexp (0 * x) = HPow.hPow (β := ℕ) (cexp x) 0
Tactic: rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
rw : cexp (0 * x) = HPow.hPow (β := ℕ) (cexp x) 0
⊢ cexp ((↑0 : ℂ) * x) = HPow.hPow (β := ℕ) (cexp x) 0
have rw₁ : cexp 0 = HPow.hPow (β := ℕ) (cexp x) 0
Tactic: rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
rw : cexp (0 * x) = HPow.hPow (β := ℕ) (cexp x) 0
rw₁ : cexp 0 = HPow.hPow (β := ℕ) (cexp x) 0
⊢ cexp ((↑0 : ℂ) * x) = HPow.hPow (β := ℕ) (cexp x) 0
have rw₂ : 1 = HPow.hPow (β := ℕ) (cexp x) 0
Tactic: rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
rw : cexp (0 * x) = HPow.hPow (β := ℕ) (cexp x) 0
rw₁ : cexp 0 = HPow.hPow (β := ℕ) (cexp x) 0
rw₂ : 1 = HPow.hPow (β := ℕ) (cexp x) 0
⊢ cexp ((↑0 : ℂ) * x) = HPow.hPow (β := ℕ) (cexp x) 0
have rw₃ : Eq (α := ℂ) 1 1
Tactic: rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
⊢ cexp ((↑n.succ : ℂ) * x) = cexp x ^ n.succ
have rw : cexp ((↑n.succ : ℂ) * x) = cexp x ^ n * cexp x
Tactic: rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
rw : cexp ((↑n.succ : ℂ) * x) = cexp x ^ n * cexp x
⊢ cexp ((↑n.succ : ℂ) * x) = cexp x ^ n.succ
have rw₁ : cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x) = cexp x ^ n * cexp x
Tactic: rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
rw : cexp ((↑n.succ : ℂ) * x) = cexp x ^ n * cexp x
rw₁ : cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x) = cexp x ^ n * cexp x
⊢ cexp ((↑n.succ : ℂ) * x) = cexp x ^ n.succ
have rw₂ : cexp ((↑n : ℂ) * x + 1 * x) = cexp x ^ n * cexp x
Tactic: rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
rw : cexp ((↑n.succ : ℂ) * x) = cexp x ^ n * cexp x
rw₁ : cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x) = cexp x ^ n * cexp x
rw₂ : cexp ((↑n : ℂ) * x + 1 * x) = cexp x ^ n * cexp x
⊢ cexp ((↑n.succ : ℂ) * x) = cexp x ^ n.succ
have rw₃ : cexp ((↑n : ℂ) * x) * cexp (1 * x) = cexp x ^ n * cexp x
Tactic: rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
rw : cexp ((↑n.succ : ℂ) * x) = cexp x ^ n * cexp x
rw₁ : cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x) = cexp x ^ n * cexp x
rw₂ : cexp ((↑n : ℂ) * x + 1 * x) = cexp x ^ n * cexp x
rw₃ : cexp ((↑n : ℂ) * x) * cexp (1 * x) = cexp x ^ n * cexp x
⊢ cexp ((↑n.succ : ℂ) * x) = cexp x ^ n.succ
have rw₄ : cexp ((↑n : ℂ) * x) * cexp (1 * x) = cexp ((↑n : ℂ) * x) * cexp x
Tactic: rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
rw : cexp ((↑n.succ : ℂ) * x) = cexp x ^ n * cexp x
rw₁ : cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x) = cexp x ^ n * cexp x
rw₂ : cexp ((↑n : ℂ) * x + 1 * x) = cexp x ^ n * cexp x
rw₃ : cexp ((↑n : ℂ) * x) * cexp (1 * x) = cexp x ^ n * cexp x
rw₄ : cexp ((↑n : ℂ) * x) * cexp (1 * x) = cexp ((↑n : ℂ) * x) * cexp x
⊢ cexp ((↑n.succ : ℂ) * x) = cexp x ^ n.succ
have rw₅ : cexp ((↑n : ℂ) * x) * cexp x = cexp ((↑n : ℂ) * x) * cexp x
Tactic: rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
h : cexp x = 0
⊢ Eq (α := ℂ) 0 1
have rw : x + -x = 0 * cexp (-x)
Tactic: rw [← exp_zero, ← add_neg_cancel x, exp_add, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
⊢ cexp (-x) = (cexp x)⁻¹
have rw : cexp (x + -x) = cexp x * (cexp x)⁻¹
Tactic: rw [← mul_right_inj' (exp_ne_zero x), ← exp_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
z : ℂ
n : ℤ
⊢ cexp ((↑n : ℂ) * z) = cexp z ^ n
have ofNat : ∀ (a : ℕ), cexp ((↑(Int.ofNat a) : ℂ) * z) = cexp z ^ Int.ofNat a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
z : ℂ
n : ℤ
ofNat : ∀ (a : ℕ), cexp ((↑(Int.ofNat a) : ℂ) * z) = cexp z ^ Int.ofNat a
⊢ cexp ((↑n : ℂ) * z) = cexp z ^ n
have negSucc : ∀ (a : ℕ), cexp ((↑(Int.negSucc a) : ℂ) * z) = cexp z ^ Int.negSucc a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
⊢ cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x)
have simp : (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (starRingEnd ℂ : (a : ℂ) → ℂ) (exp' x).lim
Tactic: simp only [exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
⊢ (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (starRingEnd ℂ : (a : ℂ) → ℂ) (exp' x).lim
have rw : (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (cauSeqConj (exp' x)).lim
Tactic: rw [← lim_conj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
⊢ (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (cauSeqConj (exp' x)).lim
have refine : ∀ (x_1 : ℕ), (↑(exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : ℕ → ℂ) x_1 = (↑(cauSeqConj (exp' x)) : ℕ → ℂ) x_1
Tactic: refine congr_arg CauSeq.lim (CauSeq.ext fun _ => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
x_1 : ℕ
⊢ (↑(exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : ℕ → ℂ) x_1 = (↑(cauSeqConj (exp' x)) : ℕ → ℂ) x_1
have dsimp : Eq (α := ℂ) (∑ m ∈ range x_1, HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) m / (↑m.factorial : ℂ) : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ m ∈ range x_1, x ^ m / (↑m.factorial : ℂ)) : ℂ)
Tactic: dsimp [exp', Function.comp_def, cauSeqConj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
x_1 : ℕ
⊢ Eq (α := ℂ) (∑ m ∈ range x_1, HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) m / (↑m.factorial : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ m ∈ range x_1, x ^ m / (↑m.factorial : ℂ)) : ℂ)
have rw : Eq (α := ℂ) (∑ m ∈ range x_1, HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) m / (↑m.factorial : ℂ))
  (∑ x_2 ∈ range x_1, (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ x_2 / (↑x_2.factorial : ℂ)))
Tactic: rw [map_sum (starRingEnd _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
x_1 : ℕ
⊢ Eq (α := ℂ) (∑ m ∈ range x_1, HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) m / (↑m.factorial : ℂ))
    (∑ x_2 ∈ range x_1, (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ x_2 / (↑x_2.factorial : ℂ)))
have refine : ∀ n ∈ range x_1,
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n / (↑n.factorial : ℂ))
Tactic: refine sum_congr rfl fun n _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
x_1 n : ℕ
h : n ∈ range x_1
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n / (↑n.factorial : ℂ))
have rw : HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n.factorial : ℂ) : ℂ)
Tactic: rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
x_1 n : ℕ
h : n ∈ range x_1
rw :
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n.factorial : ℂ) : ℂ)
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n / (↑n.factorial : ℂ))
have rw₁ : HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
  HDiv.hDiv (β := ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n.factorial : ℂ) : ℂ)
Tactic: rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
x_1 n : ℕ
h : n ∈ range x_1
rw :
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n.factorial : ℂ) : ℂ)
rw₁ :
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    HDiv.hDiv (β := ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n.factorial : ℂ) : ℂ)
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n / (↑n.factorial : ℂ))
have rw₂ : HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑(↑n.factorial : ℝ) : ℂ) =
  HDiv.hDiv (β := ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑(↑n.factorial : ℝ) : ℂ) : ℂ)
Tactic: rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
x_1 n : ℕ
h : n ∈ range x_1
rw :
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n.factorial : ℂ) : ℂ)
rw₁ :
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    HDiv.hDiv (β := ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑n.factorial : ℂ) : ℂ)
rw₂ :
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑(↑n.factorial : ℝ) : ℂ) =
    HDiv.hDiv (β := ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑(↑n.factorial : ℝ) : ℂ) : ℂ)
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n / (↑n.factorial : ℂ))
have rw₃ : HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑(↑n.factorial : ℝ) : ℂ) =
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑(↑n.factorial : ℝ) : ℂ)
Tactic: rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (↑x : ℂ)) = cexp (↑x : ℂ)
have rw : cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cexp (↑x : ℂ)
Tactic: rw [← exp_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
rw : cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cexp (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (↑x : ℂ)) = cexp (↑x : ℂ)
have rw₁ : cexp (↑x : ℂ) = cexp (↑x : ℂ)
Tactic: rw [← exp_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
⊢ (cexp (↑x : ℂ)).im = 0
have rw : (↑(cexp (↑x : ℂ)).re : ℂ).im = 0
Tactic: rw [← ofReal_exp_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
rw : (↑(cexp (↑x : ℂ)).re : ℂ).im = 0
⊢ (cexp (↑x : ℂ)).im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_exp_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
h : rexp x = 0
⊢ cexp (↑x : ℂ) = 0
have h₁ : (↑(cexp (↑x : ℂ)).re : ℂ) = (↑0 : ℂ)
Tactic: rw [exp, ← ofReal_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ ∑ i ∈ range n, x ^ i / (↑i ! : ℝ) ≤
    lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯)
have refine : ∀ (j : ℕ) (hj : j ≥ n),
  (↑(const abs (∑ i ∈ range n, x ^ i / (↑i ! : ℝ))) : ℕ → ℝ) j ≤
    (↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) sorry) : ℕ → ℝ)
      j
Tactic: refine le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ (↑(const abs (∑ i ∈ range n, x ^ i / (↑i ! : ℝ))) : ℕ → ℝ) j ≤
    (↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) : ℕ → ℝ)
      j
have simp : LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, ((↑x : ℂ) ^ i / (↑i ! : ℂ)).re)
Tactic: simp only [exp', const_apply, re_sum]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, ((↑x : ℂ) ^ i / (↑i ! : ℂ)).re)
have norm_cast : LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, x ^ i / (↑i ! : ℝ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, x ^ i / (↑i ! : ℝ))
have refine : ∀ x_1 ∈ range j, x_1 ∉ range n → 0 ≤ x ^ x_1 / (↑x_1 ! : ℝ)
Tactic: refine sum_le_sum_of_subset_of_nonneg (range_mono hj) fun _ _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) = rexp x
have rw : lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) sorry) =
  (cexp (↑x : ℂ)).re
Tactic: rw [exp, Complex.exp, ← cauSeqRe, lim_re]