-- Mathlib/Data/Complex/Exponential.lean
theorem exp_zero : exp 0 = 1

Proof state:
⊢ (exp' 0).lim = 1

Tactic:
refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩

Result:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) j‖ < ε

Proof state:
case h.e'_3.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
induction' j with j ih

Result:
case h.e'_3.succ.zero
ε : ℝ
ε0 : ε > 0
hj : 0 + 1 ≥ 1
⊢ ‖∑ m ∈ range (0 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

case h.e'_3.succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Proof state:
⊢ cexp 0 = 1

Tactic:
rw [exp]

Result:
⊢ (exp' 0).lim = 1

Proof state:
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ j + 1 ≥ 1

Tactic:
simp [Nat.succ_le_succ]

Result:
no goals

Proof state:
case h.e'_3.zero
ε : ℝ
ε0 : ε > 0
hj : 0 ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) 0‖ = 0

Tactic:
exact absurd hj (not_le_of_gt zero_lt_one)

Result:
no goals

Proof state:
case h.e'_3.succ.zero
ε : ℝ
ε0 : ε > 0
hj : 0 + 1 ≥ 1
⊢ ‖∑ m ∈ {0}, 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
simp [show Nat.succ 0 = 1 from rfl]

Result:
no goals

Proof state:
case h.e'_3.succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range j, 0 ^ m / ↑m.factorial + 0 ^ j / ↑j.factorial + 0 ^ j * 0 / ↑(j + 1).factorial - 1‖ =
    ‖∑ m ∈ range j, 0 ^ m / ↑m.factorial + 0 ^ j / ↑j.factorial - 1‖

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) (j + 1)‖ = 0

Tactic:
dsimp [exp']

Result:
case h.e'_3.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Proof state:
case h.e'_3
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) j‖ = 0

Tactic:
rcases j with - | j

Result:
case h.e'_3.zero
ε : ℝ
ε0 : ε > 0
hj : 0 ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) 0‖ = 0

case h.e'_3.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) (j + 1)‖ = 0

Proof state:
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) j‖ < ε

Tactic:
convert (config := .unfoldSameFun) ε0

Result:
case h.e'_3
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ‖↑(exp' 0 - const (fun x => ‖x‖) 1) j‖ = 0

Proof state:
case h.e'_3.succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖

Tactic:
simp only [sum_range_succ, pow_succ]

Result:
case h.e'_3.succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range j, 0 ^ m / ↑m.factorial + 0 ^ j / ↑j.factorial + 0 ^ j * 0 / ↑(j + 1).factorial - 1‖ =
    ‖∑ m ∈ range j, 0 ^ m / ↑m.factorial + 0 ^ j / ↑j.factorial - 1‖

Proof state:
case h.e'_3.succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
rw [← ih (by simp [Nat.succ_le_succ])]

Result:
case h.e'_3.succ.succ
ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ ‖∑ m ∈ range (j + 1 + 1), 0 ^ m / ↑m.factorial - 1‖ = ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖

Proof state:
case h.e'_3.succ.zero
ε : ℝ
ε0 : ε > 0
hj : 0 + 1 ≥ 1
⊢ ‖∑ m ∈ range (0 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
dsimp [exp']

Result:
case h.e'_3.succ.zero
ε : ℝ
ε0 : ε > 0
hj : 0 + 1 ≥ 1
⊢ ‖∑ m ∈ {0}, 0 ^ m / ↑m.factorial - 1‖ = 0