Theorem: inv_mem_t (Ray/Dynamics/Multibrot/Bottcher.lean)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ z⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
simp only [mem_setOf, map_inv₀]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs z)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs z)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
refine inv_lt_inv_of_lt (lt_of_lt_of_le (by norm_num) (le_max_left _ _)) ?_
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ max 16 (Complex.abs c / 2) < Complex.abs z

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ max 16 (Complex.abs c / 2) < Complex.abs z
Tactic:
exact lt_of_lt_of_le (max_lt c16 (half_lt_self (lt_trans (by norm_num) c16))) cz
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 16
Tactic:
norm_num
State after:
no goals