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

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

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : Complex.abs (g f d z - 1) ≤ 1 / 4
⊢ g f d z ≠ 0
Tactic:
contrapose h
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : ¬g f d z ≠ 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : ¬g f d z ≠ 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [not_not] at h
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [h]
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (0 - 1) ≤ 1 / 4

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (0 - 1) ≤ 1 / 4
Tactic:
norm_num
State after:
no goals