Theorem: coe_preimage_multibrotExt (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun z => ↑z) ⁻¹' multibrotExt d = (multibrot d)ᶜ
Tactic:
apply Set.ext
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ x ∈ (multibrot d)ᶜ

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ x ∈ (multibrot d)ᶜ
Tactic:
intro z
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ z ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ z ∈ (multibrot d)ᶜ

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ z ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ z ∈ (multibrot d)ᶜ
Tactic:
simp only [mem_compl_iff, mem_preimage, multibrotExt_coe]
State after:
no goals