awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 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) =
  (exp' (↑x : ℂ)).lim.re
Tactic: rw [exp, Complex.exp, ← cauSeqRe, lim_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) = rexp x
have rw₂ : (cauSeqRe (exp' (↑x : ℂ))).lim = (exp' (↑x : ℂ)).lim.re
Tactic: rw [exp, Complex.exp, ← cauSeqRe, lim_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ lim (Subtype.mk (p := fun (f : ℕ → ℝ) ↦ IsCauSeq abs f) (fun (n : ℕ) ↦ ((↑(exp' (↑x : ℂ)) : ℕ → ℂ) n).re) ⋯) = rexp x
have rw₃ : (exp' (↑x : ℂ)).lim.re = (exp' (↑x : ℂ)).lim.re
Tactic: rw [exp, Complex.exp, ← cauSeqRe, lim_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 = ∑ i ∈ range 3, x ^ i / (↑i ! : ℝ)
have 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)
Tactic: simp only [sum_range_succ, range_one, sum_singleton, _root_.pow_zero, factorial,
          pow_one, mul_one, Nat.mul_one,
          cast_succ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 < x
⊢ x + 1 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2
have nlinarith : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 < x
nlinarith : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ x + 1 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2
have nlinarith₁ : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → 2 / 2 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ x + 1 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2
have nlinarith₂ : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ x + 1 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2
have nlinarith₃ : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 ≤ x + 1 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ x + 1 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ x + 1 ≤ rexp x
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0
Tactic: rcases eq_or_lt_of_le hx with (rfl | h)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0
⊢ x + 1 ≤ rexp x
have inr : ∀ (h : 0 < x), x + 1 ≤ rexp x
Tactic: rcases eq_or_lt_of_le hx with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 1 ≤ rexp x
have linarith : rexp x < 1 → 0 - x + (rexp x - 1) + (x + 1 - rexp x) = 0
Tactic: linarith [add_one_le_exp_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h : x ≤ 0
⊢ 0 < rexp x
have rw : 0 < (rexp (-x))⁻¹
Tactic: rw [← neg_neg x, Real.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
⊢ rexp |x| ≤ rexp x + rexp (-x)
have inl : x ≤ 0 → rexp |x| ≤ rexp x + rexp (-x)
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
inl : x ≤ 0 → rexp |x| ≤ rexp x + rexp (-x)
⊢ rexp |x| ≤ rexp x + rexp (-x)
have inr : 0 ≤ x → rexp |x| ≤ rexp x + rexp (-x)
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℝ
h : x < y
⊢ rexp x < rexp y
have rw : rexp x < rexp (y - x) * rexp x
Tactic: rw [← sub_add_cancel y x, Real.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℝ
h : x < y
⊢ 1 < y - x + 1
have linarith : y - x + 1 ≤ 1 → x - y + (y - x + 1 - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x y : ℝ
h : x < y
⊢ 0 ≤ y - x
have linarith : y - x < 0 → x - y + (y - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
⊢ 1 < rexp x ↔ 0 < x
have rw : rexp 0 < rexp x ↔ 0 < x
Tactic: rw [← exp_zero, exp_lt_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
rw : rexp 0 < rexp x ↔ 0 < x
⊢ 1 < rexp x ↔ 0 < x
have rw₁ : 0 < x ↔ 0 < x
Tactic: rw [← exp_zero, exp_lt_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
⊢ rexp x < 1 ↔ x < 0
have rw : rexp x < rexp 0 ↔ x < 0
Tactic: rw [← exp_zero, exp_lt_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
rw : rexp x < rexp 0 ↔ x < 0
⊢ rexp x < 1 ↔ x < 0
have rw₁ : x < 0 ↔ x < 0
Tactic: rw [← exp_zero, exp_lt_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : α))
have refine_1 : ∀ a ∈ {m ∈ range j | n ≤ m}, (fun (x : ℕ) ↦ x - n) a ∈ range (j - n)
Tactic: refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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)
⊢ 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 : α))
have refine_2 : ∀ a ∈ range (j - n), (fun (x : ℕ) ↦ x + n) a ∈ {m ∈ range j | n ≤ m}
Tactic: refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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}
⊢ 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 : α))
have refine_3 : ∀ a ∈ {m ∈ range j | n ≤ m}, (fun (x : ℕ) ↦ x + n) ((fun (x : ℕ) ↦ x - n) a) = a
Tactic: refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 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 : α))
have refine_4 : ∀ a ∈ range (j - n), (fun (x : ℕ) ↦ x - n) ((fun (x : ℕ) ↦ x + n) a) = a
Tactic: refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 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 : α))
have refine_5 : ∀ a ∈ {m ∈ range j | n ≤ m},
  HDiv.hDiv (α := α) 1 (↑a.factorial : α) = HDiv.hDiv (α := α) 1 (↑((fun (x : ℕ) ↦ x - n) a + n).factorial : α)
Tactic: refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ 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)⁻¹)
have simp_rw : LE.le.{u_1} (α := α) (∑ x ∈ range (j - n), (↑(x + n).factorial : α)⁻¹)
  (∑ m ∈ range (j - n), ((↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) m)⁻¹)
Tactic: simp_rw [one_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ LE.le.{u_1} (α := α) (∑ x ∈ range (j - n), (↑(x + n).factorial : α)⁻¹)
    (∑ m ∈ range (j - n), ((↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) m)⁻¹)
have h : ∀ i ∈ range (j - n), (↑n.factorial : α) * HPow.hPow (α := α) (↑n.succ : α) i ≤ (↑(i + n).factorial : α)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : α) * HPow.hPow (α := α) (↑n.succ : α) i ≤ (↑(i + n).factorial : α)
have h : n.factorial * n.succ ^ i ≤ (n + i).factorial
Tactic: rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have h₁ : 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))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
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
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have h₂ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0
Tactic: have h₂ : (n.succ : α) ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
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 : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have h₃ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≠ 0
Tactic: have h₃ : (n.factorial * n : α) ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
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
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
Tactic: have h₄ : (n.succ - 1 : α) = n := by simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have rw : (↑n.factorial : α)⁻¹ *
    ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
      ((↑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 : α)
Tactic: rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
          ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
          mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
rw :
  (↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑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 : α)
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have rw₁ : (↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) *
    HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) =
  (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
Tactic: rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
          ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
          mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
rw :
  (↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑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 : α)
rw₁ :
  (↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) *
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have rw₂ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
    ((↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α)))) =
  (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
Tactic: rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
          ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
          mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
rw :
  (↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑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 : α)
rw₁ :
  (↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) *
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₂ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α)))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have rw₃ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
    ((↑n.factorial : α)⁻¹ * (HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
      ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
  (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
Tactic: rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
          ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
          mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
rw :
  (↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑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 : α)
rw₁ :
  (↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) *
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₂ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α)))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₃ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((↑n.factorial : α)⁻¹ * (HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have rw₄ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
    ((HSub.hSub (α := α) (↑n.succ : α) 1 * (↑n.factorial : α))⁻¹ *
      ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
  (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
Tactic: rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
          ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
          mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul, mul_comm]