-- Mathlib/Analysis/Complex/AbelLimit.lean
lemma stolzCone_subset_stolzSet_aux {s : ℝ} (hs : 0 < s) :
    ∃ M ε, 0 < M ∧ 0 < ε ∧ {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M

Proof state:
case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
⊢ {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M

Tactic:
rintro z ⟨hzl, hzr⟩

Result:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : z ∈ {z | 1 - ε < z.re}
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M

Proof state:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : z ∈ {z | 1 - ε < z.re}
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M

Tactic:
rw [Set.mem_setOf_eq, sub_lt_comm, ← one_re, ← sub_re] at hzl

Result:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M

Proof state:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
⊢ z ∈ stolzSet M

Tactic:
have h : z.im ^ 2 = (1 - z).im ^ 2 := by
  simp only [sub_im, one_im, zero_sub, even_two, neg_sq]

Result:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M

Proof state:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
⊢ z ∈ stolzSet M

Tactic:
replace H :=
  H (1 - z).re z.im ((mul_pos_iff_of_pos_left hs).mp <| (abs_nonneg z.im).trans_lt hzr) hzl hzr

Result:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
⊢ z ∈ stolzSet M

Proof state:
s : ℝ
hs : 0 < s
⊢ ∃ M ε, 0 < M ∧ 0 < ε ∧ {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M

Tactic:
peel stolzCone_subset_stolzSet_aux' s with M ε hM hε H

Result:
case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
⊢ {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M

Proof state:
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
⊢ z.im ^ 2 = (1 - z).im ^ 2

Tactic:
simp only [sub_im, one_im, zero_sub, even_two, neg_sq]

Result:
no goals

Proof state:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : √((1 - z).re ^ 2 + z.im ^ 2) < M * (1 - √((1 - (1 - z).re) ^ 2 + z.im ^ 2))
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M

Tactic:
rw [h, ← norm_eq_sqrt_sq_add_sq, ← h, sub_re, one_re, sub_sub_cancel,
  ← norm_eq_sqrt_sq_add_sq] at H

Result:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - ‖z‖)
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M

Proof state:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - ‖z‖)
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M

Tactic:
exact ⟨sub_pos.mp <| (mul_pos_iff_of_pos_left hM).mp <| (norm_nonneg _).trans_lt H, H⟩

Result:
no goals

Proof state:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : z ∈ stolzCone s
⊢ z ∈ stolzSet M

Tactic:
rw [stolzCone, Set.mem_setOf_eq, ← one_re, ← sub_re] at hzr

Result:
case h.h.h.h.intro
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
H : ∀ (x y : ℝ), 0 < x → x < ε → |y| < s * x → √(x ^ 2 + y ^ 2) < M * (1 - √((1 - x) ^ 2 + y ^ 2))
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
⊢ z ∈ stolzSet M