x y : ℂ
⊢ CauSeq.lim (exp' 0) = 1
x y : ℂ
⊢ exp 0 = 1
rw [exp]
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) j) < ε
x y : ℂ
⊢ CauSeq.lim (exp' 0) = 1
refine' lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => _⟩
case h.e'_3
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) j) = 0
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) j) < ε
convert (config := .unfoldSameFun) ε0
case h.e'_3.zero
x y : ℂ
ε : ℝ
ε0 : ε > 0
hj : Nat.zero ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) Nat.zero) = 0

case h.e'_3.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : Nat.succ j ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) (Nat.succ j)) = 0
case h.e'_3
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) j) = 0
cases' j with j j
no goals
case h.e'_3.zero
x y : ℂ
ε : ℝ
ε0 : ε > 0
hj : Nat.zero ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) Nat.zero) = 0
exact absurd hj (not_le_of_gt zero_lt_one)
case h.e'_3.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : Nat.succ j ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
case h.e'_3.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : Nat.succ j ≥ 1
⊢ ↑abs (↑(exp' 0 - const (↑abs) 1) (Nat.succ j)) = 0
dsimp [exp']
case h.e'_3.succ.zero
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj✝ : Nat.succ j ≥ 1
hj : Nat.succ Nat.zero ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ Nat.zero), 0 ^ m / ↑(Nat.factorial m) - 1) = 0

case h.e'_3.succ.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j✝ : ℕ
hj✝ : Nat.succ j✝ ≥ 1
j : ℕ
ih : Nat.succ j ≥ 1 → ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
hj : Nat.succ (Nat.succ j) ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ (Nat.succ j)), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
case h.e'_3.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : Nat.succ j ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
induction' j with j ih
case h.e'_3.succ.zero
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj✝ : Nat.succ j ≥ 1
hj : Nat.succ Nat.zero ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ 0), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
case h.e'_3.succ.zero
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj✝ : Nat.succ j ≥ 1
hj : Nat.succ Nat.zero ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ Nat.zero), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
dsimp [exp']
no goals
case h.e'_3.succ.zero
x y : ℂ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj✝ : Nat.succ j ≥ 1
hj : Nat.succ Nat.zero ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ 0), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
simp [show Nat.succ 0 = 1 from rfl]
case h.e'_3.succ.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j✝ : ℕ
hj✝ : Nat.succ j✝ ≥ 1
j : ℕ
ih : Nat.succ j ≥ 1 → ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
hj : Nat.succ (Nat.succ j) ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ (Nat.succ j)), 0 ^ m / ↑(Nat.factorial m) - 1) =
    ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1)
case h.e'_3.succ.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j✝ : ℕ
hj✝ : Nat.succ j✝ ≥ 1
j : ℕ
ih : Nat.succ j ≥ 1 → ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
hj : Nat.succ (Nat.succ j) ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ (Nat.succ j)), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
rw [← ih (by simp [show 1 = Nat.succ 0 from rfl, Nat.succ_le_succ])]
case h.e'_3.succ.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j✝ : ℕ
hj✝ : Nat.succ j✝ ≥ 1
j : ℕ
ih : Nat.succ j ≥ 1 → ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
hj : Nat.succ (Nat.succ j) ≥ 1
⊢ ↑abs
      (∑ m in range j, 0 ^ m / ↑(Nat.factorial m) + 0 ^ j / ↑(Nat.factorial j) + 0 * 0 ^ j / ↑(Nat.factorial (j + 1)) -
        1) =
    ↑abs (∑ m in range j, 0 ^ m / ↑(Nat.factorial m) + 0 ^ j / ↑(Nat.factorial j) - 1)
case h.e'_3.succ.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j✝ : ℕ
hj✝ : Nat.succ j✝ ≥ 1
j : ℕ
ih : Nat.succ j ≥ 1 → ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
hj : Nat.succ (Nat.succ j) ≥ 1
⊢ ↑abs (∑ m in range (Nat.succ (Nat.succ j)), 0 ^ m / ↑(Nat.factorial m) - 1) =
    ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1)
simp only [sum_range_succ, pow_succ]
no goals
case h.e'_3.succ.succ
x y : ℂ
ε : ℝ
ε0 : ε > 0
j✝ : ℕ
hj✝ : Nat.succ j✝ ≥ 1
j : ℕ
ih : Nat.succ j ≥ 1 → ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
hj : Nat.succ (Nat.succ j) ≥ 1
⊢ ↑abs
      (∑ m in range j, 0 ^ m / ↑(Nat.factorial m) + 0 ^ j / ↑(Nat.factorial j) + 0 * 0 ^ j / ↑(Nat.factorial (j + 1)) -
        1) =
    ↑abs (∑ m in range j, 0 ^ m / ↑(Nat.factorial m) + 0 ^ j / ↑(Nat.factorial j) - 1)
simp
no goals
x y : ℂ
ε : ℝ
ε0 : ε > 0
j✝ : ℕ
hj✝ : Nat.succ j✝ ≥ 1
j : ℕ
ih : Nat.succ j ≥ 1 → ↑abs (∑ m in range (Nat.succ j), 0 ^ m / ↑(Nat.factorial m) - 1) = 0
hj : Nat.succ (Nat.succ j) ≥ 1
⊢ Nat.succ j ≥ 1
simp [show 1 = Nat.succ 0 from rfl, Nat.succ_le_succ]