awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Exponential
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
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 : ℂ))
⊢ 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:
simp only [mul_left_comm (m.choose I : ℂ), mul_assoc, mul_left_comm (m.choose I : ℂ)⁻¹,
      mul_comm (m.choose I : ℂ)]

Premises used: Nat.choose, mul_assoc, mul_left_comm, Nat.cast, Inv.inv, mul_comm
-- Module: Mathlib.Analysis.Complex.Exponential
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
rw :
  x ^ I * (y ^ (m - I) * ((↑I.factorial : ℂ)⁻¹ * HMul.hMul (α := ℂ) (↑(m - I).factorial : ℂ)⁻¹ 1)) =
    x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).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 : ℂ))

Tactic:
rw [inv_mul_cancel₀ h₁]

Premises used: inv_mul_cancel₀
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℂ)⁻¹ * HMul.hMul (α := ℂ) (↑(m - I).factorial : ℂ)⁻¹ 1)) =
    x ^ I / (↑I.factorial : ℂ) * (y ^ (m - I) / (↑(m - I).factorial : ℂ))

Tactic:
simp [div_eq_mul_inv, mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm, div_eq_mul_inv
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℂ)))

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]
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℂ)))
simp_rw :
  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
⊢ cexp (x + y) = cexp x * cexp y

Tactic:
simp_rw [exp, exp', lim_mul_lim]

Premises used: Complex.exp', Complex.exp, CauSeq.lim_mul_lim
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℂ)))
apply :
  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 : ℂ)) ⋯
⊢ 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

Tactic:
apply (lim_eq_lim_of_equiv _).symm

Premises used: CauSeq.lim_eq_lim_of_equiv, Eq.symm
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℂ)))
simp :
  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 : ℕ) ↦
        ∑ i ∈ range n, ∑ 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 : ℂ)) ⋯

Tactic:
simp only [hj]
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℕ) ↦
        ∑ i ∈ range n, ∑ k ∈ range (i + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (i - k) / (↑(i - k).factorial : ℂ)))
      ⋯

Tactic:
cauchy_product (isCauSeq_norm_exp x) (isCauSeq_exp y)

Premises used: Multiset.sum, Multiset.foldr, cauchy_product, Complex.isCauSeq_norm_exp, Complex.isCauSeq_exp, CauSeq.LimZero, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℕ) ↦
        ∑ i ∈ range n, ∑ k ∈ range (i + 1), x ^ k / (↑k.factorial : ℂ) * (y ^ (i - k) / (↑(i - k).factorial : ℂ)))
      ⋯

Tactic:
exact cauchy_product (isCauSeq_norm_exp x) (isCauSeq_exp y)

Premises used: cauchy_product, Complex.isCauSeq_norm_exp, Complex.isCauSeq_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
⊢ cexp ((Multiplicative.toAdd : (a : Multiplicative ℂ) → ℂ) 1) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
⊢ ∀ (x y : Multiplicative ℂ),
    cexp ((Multiplicative.toAdd : (a : Multiplicative ℂ) → ℂ) (x * y)) =
      cexp ((Multiplicative.toAdd : (a : Multiplicative ℂ) → ℂ) x) *
        cexp ((Multiplicative.toAdd : (a : Multiplicative ℂ) → ℂ) y)

Tactic:
simp [exp_add]

Premises used: Complex.exp_add
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
l : List ℂ
⊢ cexp l.sum = (List.map cexp l).prod

Tactic:
map_list_prod (M := Multiplicative ℂ) expMonoidHom l

Premises used: List.sum, Complex.expMonoidHom, map_list_prod, Multiplicative, List.prod
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
s : Multiset ℂ
⊢ cexp s.sum = (Multiset.map cexp s).prod

Tactic:
@MonoidHom.map_multiset_prod (Multiplicative ℂ) ℂ _ _ expMonoidHom s

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, Complex.expMonoidHom, Multiplicative, MonoidHom.map_multiset_prod
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
s : Finset α
f : α → ℂ
⊢ cexp (∑ x ∈ s, f x) = ∏ x ∈ s, cexp (f x)

Tactic:
map_prod (M := Multiplicative ℂ) expMonoidHom f s

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, Complex.expMonoidHom, map_prod, Finset.prod, Multiplicative, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
⊢ cexp (n • x) = cexp x ^ n

Tactic:
@MonoidHom.map_pow (Multiplicative ℂ) ℂ _ _ expMonoidHom _ _

Premises used: Complex.expMonoidHom, MonoidHom.map_pow
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x a p : ℂ
n : ℕ
rw : cexp (a * (↑n : ℂ) * x / p) = cexp (n • (a * x / p))
⊢ cexp (a * (↑n : ℂ) * x / p) = cexp (a * x / p) ^ n

Tactic:
rw [← Complex.exp_nsmul]

Premises used: Complex.exp_nsmul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x a p : ℂ
n : ℕ
⊢ cexp (a * (↑n : ℂ) * x / p) = cexp (n • (a * x / p))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Complex.Exponential
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
rw₃ rw₄ : Eq (α := ℂ) 1 1
⊢ cexp ((↑0 : ℂ) * x) = HPow.hPow (β := ℕ) (cexp x) 0

Tactic:
rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]

Premises used: Complex.exp_zero, MulZeroClass.zero_mul, pow_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.Complex.Exponential
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
rw₅ rw₆ : cexp ((↑n : ℂ) * x) * cexp x = cexp ((↑n : ℂ) * x) * cexp x
⊢ cexp ((↑n.succ : ℂ) * x) = cexp x ^ n.succ

Tactic:
rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]

Premises used: add_mul, Complex.exp_add, pow_succ, Nat.cast_add_one, one_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
h : cexp x = 0
rw : x + -x = 0 * cexp (-x)
⊢ Eq (α := ℂ) 0 1

Tactic:
rw [← exp_zero, ← add_neg_cancel x, exp_add, h]

Premises used: add_neg_cancel, Complex.exp_add, Complex.exp_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
h : cexp x = 0
⊢ x + -x = 0 * cexp (-x)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
rw : cexp (x + -x) = cexp x * (cexp x)⁻¹
⊢ cexp (-x) = (cexp x)⁻¹

Tactic:
rw [← mul_right_inj' (exp_ne_zero x), ← exp_add]

Premises used: Complex.exp_ne_zero, Complex.exp_add, mul_right_inj'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
⊢ cexp (x + -x) = cexp x * (cexp x)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℂ
⊢ cexp (x - y) = cexp x / cexp y

Tactic:
simp [sub_eq_add_neg, exp_add, exp_neg, div_eq_mul_inv]

Premises used: Complex.exp_add, sub_eq_add_neg, Complex.exp_neg, div_eq_mul_inv
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
n : ℤ
ofNat : ∀ (a : ℕ), cexp ((↑(Int.ofNat a) : ℂ) * z) = cexp z ^ Int.ofNat a
negSucc : ∀ (a : ℕ), cexp ((↑(Int.negSucc a) : ℂ) * z) = cexp z ^ Int.negSucc a
⊢ cexp ((↑n : ℂ) * z) = cexp z ^ n

Tactic:
cases n
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
a : ℕ
⊢ cexp ((↑(Int.ofNat a) : ℂ) * z) = cexp z ^ Int.ofNat a

Tactic:
simp [exp_nat_mul]

Premises used: Complex.exp_nat_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
z : ℂ
a : ℕ
⊢ cexp ((↑(Int.negSucc a) : ℂ) * z) = cexp z ^ Int.negSucc a

Tactic:
simp [exp_add, add_mul, pow_add, exp_neg, exp_nat_mul]

Premises used: add_mul, Complex.exp_add, pow_add, Complex.exp_neg, Complex.exp_nat_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
simp : (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (starRingEnd ℂ : (a : ℂ) → ℂ) (exp' x).lim
⊢ cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x)

Tactic:
simp only [exp]

Premises used: Complex.exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
rw : (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (cauSeqConj (exp' x)).lim
⊢ (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (starRingEnd ℂ : (a : ℂ) → ℂ) (exp' x).lim

Tactic:
rw [← lim_conj]

Premises used: Complex.lim_conj
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
⊢ (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (cauSeqConj (exp' x)).lim

Tactic:
congr_arg CauSeq.lim (CauSeq.ext fun _ => ?_)

Premises used: congr_arg, CauSeq.lim, CauSeq.ext
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
refine : ∀ (x_1 : ℕ), (↑(exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : ℕ → ℂ) x_1 = (↑(cauSeqConj (exp' x)) : ℕ → ℂ) x_1
⊢ (exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)).lim = (cauSeqConj (exp' x)).lim

Tactic:
refine congr_arg CauSeq.lim (CauSeq.ext fun _ => ?_)

Premises used: congr_arg, CauSeq.lim, CauSeq.ext
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
x_1 : ℕ
dsimp :
  Eq (α := ℂ) (∑ m ∈ range x_1, HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) m / (↑m.factorial : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ m ∈ range x_1, x ^ m / (↑m.factorial : ℂ)) : ℂ)
⊢ (↑(exp' ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) : ℕ → ℂ) x_1 = (↑(cauSeqConj (exp' x)) : ℕ → ℂ) x_1

Tactic:
dsimp [exp', Function.comp_def, cauSeqConj]

Premises used: Complex.exp', Function.comp_def, Complex.cauSeqConj
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
x_1 : ℕ
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 : ℂ)))
⊢ Eq (α := ℂ) (∑ m ∈ range x_1, HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) m / (↑m.factorial : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (∑ m ∈ range x_1, x ^ m / (↑m.factorial : ℂ)) : ℂ)

Tactic:
rw [map_sum (starRingEnd _)]

Premises used: map_sum, starRingEnd
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℂ)))

Tactic:
sum_congr rfl fun n _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
x_1 : ℕ
refine :
  ∀ n ∈ range x_1,
    HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
      (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n / (↑n.factorial : ℂ))
⊢ 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:
refine sum_congr rfl fun n _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℝ) : ℂ) : ℂ)
rw₃ rw₄ :
  HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑(↑n.factorial : ℝ) : ℂ) =
    HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑(↑n.factorial : ℝ) : ℂ)
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n / (↑n.factorial : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x ^ n / (↑n.factorial : ℂ))

Tactic:
rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]

Premises used: map_pow, map_div₀, Complex.ofReal_natCast, Complex.conj_ofReal
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
rw : cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cexp (↑x : ℂ)
rw₁ rw₂ : cexp (↑x : ℂ) = cexp (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (↑x : ℂ)) = cexp (↑x : ℂ)

Tactic:
rw [← exp_conj, conj_ofReal]

Premises used: Complex.exp_conj, Complex.conj_ofReal
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ (↑(Real.exp x) : ℂ) = cexp (↑x : ℂ)

Tactic:
ofReal_exp_ofReal_re _

Premises used: Real.exp, Complex.ofReal_exp_ofReal_re
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
rw : (↑(cexp (↑x : ℂ)).re : ℂ).im = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (cexp (↑x : ℂ)).im = 0

Tactic:
rw [← ofReal_exp_ofReal_re, ofReal_im]

Premises used: Complex.ofReal_exp_ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ (cexp (↑x : ℂ)).re = Real.exp x

Tactic:
rfl

Premises used: Real.exp, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
⊢ rexp 0 = 1

Tactic:
simp [Real.exp]

Premises used: Real.exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
⊢ rexp (x + y) = rexp x * rexp y

Tactic:
simp [exp_add, exp]

Premises used: Real.exp, Real.exp_add
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
⊢ rexp ((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) 1) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
⊢ ∀ (x y : Multiplicative ℝ),
    rexp ((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) (x * y)) =
      rexp ((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) x) *
        rexp ((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) y)

Tactic:
simp [exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
l : List ℝ
⊢ rexp l.sum = (List.map rexp l).prod

Tactic:
map_list_prod (M := Multiplicative ℝ) expMonoidHom l

Premises used: List.sum, Real.expMonoidHom, map_list_prod, Real.exp, Multiplicative, List.prod
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
s : Multiset ℝ
⊢ rexp s.sum = (Multiset.map rexp s).prod

Tactic:
@MonoidHom.map_multiset_prod (Multiplicative ℝ) ℝ _ _ expMonoidHom s

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, Real.expMonoidHom, Real.exp, Multiplicative, MonoidHom.map_multiset_prod
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ rexp (∑ x ∈ s, f x) = ∏ x ∈ s, rexp (f x)

Tactic:
map_prod (M := Multiplicative ℝ) expMonoidHom f s

Premises used: Multiset.sum, Multiset.foldr, Multiset.prod, Real.expMonoidHom, Real.exp, map_prod, Finset.prod, Multiplicative, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
n : ℕ
⊢ rexp (n • x) = rexp x ^ n

Tactic:
@MonoidHom.map_pow (Multiplicative ℝ) ℝ _ _ expMonoidHom _ _

Premises used: Real.expMonoidHom, Real.exp, MonoidHom.map_pow
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
n : ℕ
⊢ (↑(rexp ((↑n : ℝ) * x)) : ℂ) = (↑(rexp x ^ n) : ℂ)

Tactic:
simp [exp_nat_mul]

Premises used: Real.exp_nat_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h : rexp x = 0
⊢ (↑(cexp (↑x : ℂ)).re : ℂ) = (↑0 : ℂ)

Tactic:
rw [exp, ← ofReal_inj] at h

Premises used: Real.exp, Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h : (↑(cexp (↑x : ℂ)).re : ℂ) = (↑0 : ℂ)
⊢ cexp (↑x : ℂ) = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ (↑(rexp (-x)) : ℂ) = (↑(rexp x)⁻¹ : ℂ)

Tactic:
simp [exp_neg]

Premises used: Real.exp_neg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
⊢ rexp (x - y) = rexp x / rexp y

Tactic:
simp [sub_eq_add_neg, exp_add, exp_neg, div_eq_mul_inv]

Premises used: sub_eq_add_neg, div_eq_mul_inv, Real.exp_neg, Real.exp_add
-- Module: Mathlib.Analysis.Complex.Exponential
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) ⋯)

Tactic:
le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)

Premises used: CauSeq.le_lim, CauSeq.le_of_exists, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
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) ⋯) :
          ℕ → ℝ)
        j
⊢ ∑ i ∈ range n, x ^ i / (↑i ! : ℝ) ≤
    lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯)

Tactic:
refine le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)

Premises used: CauSeq.le_lim, CauSeq.le_of_exists, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
simp : LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, ((↑x : ℂ) ^ i / (↑i ! : ℂ)).re)
⊢ (↑(const abs (∑ i ∈ range n, x ^ i / (↑i ! : ℝ))) : ℕ → ℝ) j ≤
    (↑(Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) : ℕ → ℝ)
      j

Tactic:
simp only [exp', const_apply, re_sum]

Premises used: Complex.exp', CauSeq.const_apply, Complex.re_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
norm_cast : LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, x ^ i / (↑i ! : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, ((↑x : ℂ) ^ i / (↑i ! : ℂ)).re)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, x ^ i / (↑i ! : ℝ))

Tactic:
sum_le_sum_of_subset_of_nonneg (range_mono hj) fun _ _ _ ↦ ?_

Premises used: Finset.sum_le_sum_of_subset_of_nonneg, Finset.range_mono
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
refine : ∀ x_1 ∈ range j, x_1 ∉ range n → 0 ≤ x ^ x_1 / (↑x_1 ! : ℝ)
⊢ LE.le (α := ℝ) (∑ i ∈ range n, x ^ i / (↑i ! : ℝ)) (∑ i ∈ range j, x ^ i / (↑i ! : ℝ))

Tactic:
refine sum_le_sum_of_subset_of_nonneg (range_mono hj) fun _ _ _ ↦ ?_

Premises used: Finset.sum_le_sum_of_subset_of_nonneg, Finset.range_mono
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
x_1 : ℕ
h : x_1 ∈ range j
h_1 : x_1 ∉ range n
⊢ 0 ≤ x ^ x_1 / (↑x_1 ! : ℝ)

Tactic:
positivity