-- 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)
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)
rw₅ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((HMul.hMul (α := α) (↑n : α) (↑n.factorial : α))⁻¹ *
        ((↑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 : α) * (HMul.hMul (α := α) (↑n : α) (↑n.factorial : α))⁻¹ *
      ((↑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 : α) * (HMul.hMul (α := α) (↑n.factorial : α) (↑n : α))⁻¹ *
      ((↑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₈ : 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]