awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n : ℕ
rw :
  lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) =
    (cexp (↑x : ℂ)).re
rw₁ :
  lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) =
    (exp' (↑x : ℂ)).lim.re
rw₂ : (cauSeqRe (exp' (↑x : ℂ))).lim = (exp' (↑x : ℂ)).lim.re
rw₃ rw₄ : (exp' (↑x : ℂ)).lim.re = (exp' (↑x : ℂ)).lim.re
⊢ lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) = rexp x

Tactic:
rw [exp, Complex.exp, ← cauSeqRe, lim_re]

Premises used: Real.exp, Complex.exp, Complex.cauSeqRe, Complex.lim_re
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
n k : ℕ
h : k ∈ range (n + 1)
⊢ LE.le (α := ℝ) 0 ((fun (k : ℕ) ↦ x ^ k / (↑k ! : ℝ)) k)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
simp :
  1 + x + HPow.hPow (β := ℕ) x 2 / 2 =
    1 / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + x / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 +
      HPow.hPow (β := ℕ) x 2 / (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1)
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 = ∑ i ∈ range 3, x ^ i / (↑i ! : ℝ)

Tactic:
simp only [sum_range_succ, range_one, sum_singleton, _root_.pow_zero, factorial,
          pow_one, mul_one, Nat.mul_one,
          cast_succ]

Premises used: Nat.cast_succ, Nat.mul_one, pow_zero, Finset.sum_singleton, Nat.factorial, pow_one, Finset.range_one, mul_one, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 =
    1 / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + x / HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 +
      HPow.hPow (β := ℕ) x 2 / (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1 + 1)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 < x
nlinarith : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
nlinarith₁ : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → 2 / 2 = 1
nlinarith₂ : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₃ : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → GT.gt (α := ℝ) 2 0
nlinarith₄ :
  1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 →
    HMul.hMul (α := ℝ) 2 1 + 2 * x + 1 * HPow.hPow (β := ℕ) (1 * x) 2 - (2 * x + HMul.hMul (α := ℝ) 2 1) +
        (0 - (0 - x) * (0 - x)) =
      0
⊢ x + 1 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0
inr : ∀ (h : 0 < x), x + 1 ≤ rexp x
⊢ x + 1 ≤ rexp x

Tactic:
rcases eq_or_lt_of_le hx with (rfl | h)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
hx : LE.le (α := ℝ) 0 0
⊢ HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x

Tactic:
(add_one_lt_exp_of_pos h).le

Premises used: LT.lt.le, _private.0.Real.add_one_lt_exp_of_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
h : 0 < x
⊢ x + 1 ≤ rexp x

Tactic:
exact (add_one_lt_exp_of_pos h).le

Premises used: LT.lt.le, _private.0.Real.add_one_lt_exp_of_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : 0 ≤ x
linarith : rexp x < 1 → 0 - x + (rexp x - 1) + (x + 1 - rexp x) = 0
⊢ 1 ≤ rexp x

Tactic:
linarith [add_one_le_exp_of_nonneg hx]

Premises used: _private.0.Real.add_one_le_exp_of_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h : x ≤ 0
rw : 0 < (rexp (-x))⁻¹
⊢ 0 < rexp x

Tactic:
rw [← neg_neg x, Real.exp_neg]

Premises used: neg_neg, Real.exp_neg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h : x ≤ 0
⊢ 0 < (rexp (-x))⁻¹

Tactic:
inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))

Premises used: Iff.mpr, inv_pos, neg_nonneg, zero_lt_one, Real.one_le_exp, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h : x ≤ 0
⊢ 0 < (rexp (-x))⁻¹

Tactic:
exact inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))

Premises used: Iff.mpr, inv_pos, neg_nonneg, zero_lt_one, Real.one_le_exp, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ 0 ≤ rexp x

Tactic:
x.exp_pos.le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ |rexp x| = rexp x

Tactic:
abs_of_pos (exp_pos _)

Premises used: abs_of_pos, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
inl : x ≤ 0 → rexp |x| ≤ rexp x + rexp (-x)
inr : 0 ≤ x → rexp |x| ≤ rexp x + rexp (-x)
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
cases le_total x 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h : x ≤ 0
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]

Premises used: abs_of_nonpos, abs_of_nonneg, Real.exp_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h : 0 ≤ x
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]

Premises used: abs_of_nonpos, abs_of_nonneg, Real.exp_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
h : x < y
rw : rexp x < rexp (y - x) * rexp x
⊢ rexp x < rexp y

Tactic:
rw [← sub_add_cancel y x, Real.exp_add]

Premises used: sub_add_cancel, Real.exp_add
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
h : x < y
linarith : y - x + 1 ≤ 1 → x - y + (y - x + 1 - 1) = 0
⊢ 1 < y - x + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
h : x < y
linarith : y - x < 0 → x - y + (y - x - 0) = 0
⊢ 0 ≤ y - x

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x) * rexp x

Tactic:
exact (lt_mul_iff_one_lt_left (exp_pos _)).2
      (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))

Premises used: Iff.mpr, _private.0.Real.add_one_le_exp_of_nonneg, lt_mul_iff_one_lt_left, lt_of_lt_of_le, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
⊢ Monotone rexp

Tactic:
exp_strictMono.monotone

Premises used: StrictMono.monotone, Real.exp_strictMono
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
h : x ≤ y
⊢ rexp x ≤ rexp y

Tactic:
exp_monotone h

Premises used: Real.exp_monotone
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
⊢ rexp x < rexp y ↔ x < y

Tactic:
exp_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Real.exp_strictMono
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
⊢ rexp x ≤ rexp y ↔ x ≤ y

Tactic:
exp_strictMono.le_iff_le

Premises used: Real.exp_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
⊢ Function.Injective rexp

Tactic:
exp_strictMono.injective

Premises used: Real.exp_strictMono, StrictMono.injective
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x y : ℝ
⊢ rexp x = rexp y ↔ x = y

Tactic:
exp_injective.eq_iff

Premises used: Function.Injective.eq_iff, Real.exp_injective
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ rexp x = 1 ↔ x = 0

Tactic:
exp_injective.eq_iff' exp_zero

Premises used: Function.Injective.eq_iff', Real.exp_injective, Real.exp_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
rw : rexp 0 < rexp x ↔ 0 < x
rw₁ rw₂ : 0 < x ↔ 0 < x
⊢ 1 < rexp x ↔ 0 < x

Tactic:
rw [← exp_zero, exp_lt_exp]

Premises used: Real.exp_lt_exp, Real.exp_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
rw : rexp x < rexp 0 ↔ x < 0
rw₁ rw₂ : x < 0 ↔ x < 0
⊢ rexp x < 1 ↔ x < 0

Tactic:
rw [← exp_zero, exp_lt_exp]

Premises used: Real.exp_lt_exp, Real.exp_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ rexp x ≤ 1 ↔ x ≤ 0

Tactic:
exp_zero ▸ exp_le_exp

Premises used: Eq.rec, Real.exp_le_exp, Real.exp_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ 1 ≤ rexp x ↔ 0 ≤ x

Tactic:
exp_zero ▸ exp_le_exp

Premises used: Eq.rec, Real.exp_le_exp, Real.exp_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ Eq.{u_1 + 1} (α := α) (∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := α) 1 (↑m.factorial : α))
    (∑ m ∈ range (j - n), HDiv.hDiv (α := α) 1 (↑(m + n).factorial : α))

Tactic:
sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_

Premises used: HSub.hSub, HAdd.hAdd, Finset.sum_nbij'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
refine_1 : ∀ a ∈ {m ∈ range j | n ≤ m}, (fun (x : ℕ) ↦ x - n) a ∈ range (j - n)
refine_2 : ∀ a ∈ range (j - n), (fun (x : ℕ) ↦ x + n) a ∈ {m ∈ range j | n ≤ m}
refine_3 : ∀ a ∈ {m ∈ range j | n ≤ m}, (fun (x : ℕ) ↦ x + n) ((fun (x : ℕ) ↦ x - n) a) = a
refine_4 : ∀ a ∈ range (j - n), (fun (x : ℕ) ↦ x - n) ((fun (x : ℕ) ↦ x + n) a) = a
refine_5 :
  ∀ a ∈ {m ∈ range j | n ≤ m},
    HDiv.hDiv (α := α) 1 (↑a.factorial : α) = HDiv.hDiv (α := α) 1 (↑((fun (x : ℕ) ↦ x - n) a + n).factorial : α)
⊢ Eq.{u_1 + 1} (α := α) (∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := α) 1 (↑m.factorial : α))
    (∑ m ∈ range (j - n), HDiv.hDiv (α := α) 1 (↑(m + n).factorial : α))

Tactic:
refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_

Premises used: HSub.hSub, HAdd.hAdd, Finset.sum_nbij'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, (fun (x : ℕ) ↦ x - n) a ∈ range (j - n)

Tactic:
simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]

Premises used: lt_tsub_iff_right, tsub_add_cancel_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), (fun (x : ℕ) ↦ x + n) a ∈ {m ∈ range j | n ≤ m}

Tactic:
simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]

Premises used: lt_tsub_iff_right, tsub_add_cancel_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m}, (fun (x : ℕ) ↦ x + n) ((fun (x : ℕ) ↦ x - n) a) = a

Tactic:
simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]

Premises used: lt_tsub_iff_right, tsub_add_cancel_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ range (j - n), (fun (x : ℕ) ↦ x - n) ((fun (x : ℕ) ↦ x + n) a) = a

Tactic:
simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]

Premises used: lt_tsub_iff_right, tsub_add_cancel_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∀ a ∈ {m ∈ range j | n ≤ m},
    HDiv.hDiv (α := α) 1 (↑a.factorial : α) = HDiv.hDiv (α := α) 1 (↑((fun (x : ℕ) ↦ x - n) a + n).factorial : α)

Tactic:
simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]

Premises used: lt_tsub_iff_right, tsub_add_cancel_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
simp_rw :
  LE.le.{u_1} (α := α) (∑ x ∈ range (j - n), (↑(x + n).factorial : α)⁻¹)
    (∑ m ∈ range (j - n), ((↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) m)⁻¹)
⊢ LE.le.{u_1} (α := α) (∑ m ∈ range (j - n), HDiv.hDiv (α := α) 1 (↑(m + n).factorial : α))
    (∑ m ∈ range (j - n), ((↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) m)⁻¹)

Tactic:
simp_rw [one_div]

Premises used: one_div
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h : ∀ i ∈ range (j - n), (↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) i ≤ (↑(i + n).factorial : α)
⊢ LE.le.{u_1} (α := α) (∑ x ∈ range (j - n), (↑(x + n).factorial : α)⁻¹)
    (∑ m ∈ range (j - n), ((↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) m)⁻¹)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
i : ℕ
h_1 : i ∈ range (j - n)
h : n.factorial * n.succ ^ i ≤ (n + i).factorial
⊢ (↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) i ≤ (↑(i + n).factorial : α)

Tactic:
rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]

Premises used: add_comm, Nat.cast_mul, Nat.cast_pow, Nat.cast_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
i : ℕ
h : i ∈ range (j - n)
⊢ n.factorial * n.succ ^ i ≤ (n + i).factorial

Tactic:
Nat.factorial_mul_pow_le_factorial

Premises used: Nat.factorial_mul_pow_le_factorial
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
i : ℕ
h : i ∈ range (j - n)
⊢ n.factorial * n.succ ^ i ≤ (n + i).factorial

Tactic:
exact Nat.factorial_mul_pow_le_factorial

Premises used: Nat.factorial_mul_pow_le_factorial
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), ((↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) m)⁻¹ =
    HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m)

Tactic:
simp [← mul_sum, mul_comm, inv_pow]

Premises used: Finset.mul_sum, inv_pow, mul_comm
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1

Tactic:
have h₁ : (n.succ : α) ≠ 1 :=
        @Nat.cast_one α _ ▸ mt Nat.cast_inj.1 (mt Nat.succ.inj (pos_iff_ne_zero.1 hn))
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
⊢ Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
⊢ Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0

Tactic:
have h₂ : (n.succ : α) ≠ 0 := by positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
h₂ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0
⊢ HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
h₂ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0
⊢ HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≠ 0

Tactic:
have h₃ : (n.factorial * n : α) ≠ 0 := by positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
h₂ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0
h₃ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≠ 0
⊢ HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
h₂ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0
h₃ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≠ 0
⊢ HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)

Tactic:
have h₄ : (n.succ - 1 : α) = n := by simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
hab : (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) ≤ (↑n.succ : α)
⊢ ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≤
    (↑n.succ : α) / HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
hab : 0 ≤ (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
⊢ (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) ≤ (↑n.succ : α)

Tactic:
apply sub_le_self

Premises used: sub_le_self
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ 0 ≤ (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
rw :
  (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)‖ ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)

Tactic:
rw [← lim_const (abv := norm) (∑ m ∈ range n, _), exp, sub_eq_add_neg,
    ← lim_neg, lim_add, ← lim_norm]

Premises used: sub_eq_add_neg, CauSeq.lim_add, CauSeq.lim_const, Finset.range, Complex.exp, Complex.lim_norm, CauSeq.lim_neg, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)

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

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
refine :
  ∀ (j : ℕ) (hj : j ≥ n),
    (↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))) : ℕ → ℝ) j ≤
      (↑(const abs (‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹))) : ℕ → ℝ) j
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)

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

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
rw :
  norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)

Tactic:
rw [sum_range_sub_sum_range hj]

Premises used: Finset.sum_range_sub_sum_range
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ m / (↑m.factorial : ℂ)) =
    norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ)))

Tactic:
congr_arg norm (sum_congr rfl fun m hm => ?_)

Premises used: Norm.norm, congr_arg, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
refine :
  ∀ (m : ℕ) (hm : m ∈ {m ∈ range j | n ≤ m}), x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))
⊢ norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ m / (↑m.factorial : ℂ)) =
    norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ)))

Tactic:
refine congr_arg norm (sum_congr rfl fun m hm => ?_)

Premises used: Norm.norm, congr_arg, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ {m ∈ range j | n ≤ m}
⊢ m < j ∧ n ≤ m

Tactic:
rw [mem_filter, mem_range] at hm

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
rw : x ^ m / (↑m.factorial : ℂ) = x ^ n * x ^ (m - n) / (↑m.factorial : ℂ)
rw₁ : x ^ m / (↑m.factorial : ℂ) = x ^ (n + (m - n)) / (↑m.factorial : ℂ)
rw₂ rw₃ : x ^ m / (↑m.factorial : ℂ) = x ^ m / (↑m.factorial : ℂ)
⊢ x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))

Tactic:
rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]

Premises used: mul_div_assoc, pow_add, And.right, add_tsub_cancel_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))) ≤
    ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))‖

Tactic:
IsAbsoluteValue.abv_sum norm ..

Premises used: Norm.norm, IsAbsoluteValue.abv_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
simp_rw :
  LE.le (α := ℝ) (∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / (↑x_1.factorial : ℝ)))
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ))
⊢ LE.le (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))‖)
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ))

Tactic:
simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]

Premises used: Complex.norm_pow, Complex.norm_natCast, Complex.norm_div, Complex.norm_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
h : ∀ i ∈ {m ∈ range j | n ≤ m}, ‖x ^ (i - n)‖ ≤ 1
⊢ LE.le (α := ℝ) (∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / (↑x_1.factorial : ℝ)))
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i : ℕ
h_1 : i ∈ {m ∈ range j | n ≤ m}
h : ‖x‖ ^ (i - n) ≤ 1
⊢ ‖x ^ (i - n)‖ ≤ 1

Tactic:
rw [Complex.norm_pow]

Premises used: Complex.norm_pow
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i : ℕ
h : i ∈ {m ∈ range j | n ≤ m}
⊢ ‖x‖ ^ (i - n) ≤ 1

Tactic:
pow_le_one₀ (norm_nonneg _) hx

Premises used: norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i : ℕ
h : i ∈ {m ∈ range j | n ≤ m}
⊢ ‖x‖ ^ (i - n) ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) hx

Premises used: norm_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) =
    ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ)

Tactic:
simp [← mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
hbc :
  ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) ≤
    (↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹
⊢ ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) ≤
    (↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹

Tactic:
sum_div_factorial_le _ _ hn

Premises used: DivInvMonoid.div', Complex.sum_div_factorial_le