Theorem: SuperNear.gs (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
by_cases z0 : z = 0
State after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : ¬z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4

State before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [z0, g0, sub_self, AbsoluteValue.map_zero, one_div, inv_nonneg, zero_le_bit0,
  zero_le_one]
State after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ 0 ≤ 4

State before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ 0 ≤ 4
Tactic:
norm_num
State after:
no goals

State before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : ¬z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [g, z0, if_false, s.gs' z0 zt]
State after:
no goals