Theorem: ray_surj (Ray/Dynamics/Multibrot/Isomorphism.lean)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ray d '' ball 0 1 = multibrotExt d
Tactic:
rw [← bottcher_surj d]
State after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ray d '' (bottcher d '' multibrotExt d) = multibrotExt d

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ray d '' (bottcher d '' multibrotExt d) = multibrotExt d
Tactic:
apply Set.ext
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : 𝕊), x ∈ ray d '' (bottcher d '' multibrotExt d) ↔ x ∈ multibrotExt d

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : 𝕊), x ∈ ray d '' (bottcher d '' multibrotExt d) ↔ x ∈ multibrotExt d
Tactic:
intro c
State after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ ray d '' (bottcher d '' multibrotExt d) ↔ c ∈ multibrotExt d

State before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ ray d '' (bottcher d '' multibrotExt d) ↔ c ∈ multibrotExt d
Tactic:
simp only [← image_comp, mem_image]
State after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) ↔ c ∈ multibrotExt d

State before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) ↔ c ∈ multibrotExt d
Tactic:
constructor
State after:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) → c ∈ multibrotExt d

case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ multibrotExt d → ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c

State before:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) → c ∈ multibrotExt d
Tactic:
intro ⟨e, m, ec⟩
State after:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : (ray d ∘ bottcher d) e = c
⊢ c ∈ multibrotExt d

State before:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : (ray d ∘ bottcher d) e = c
⊢ c ∈ multibrotExt d
Tactic:
simp only [Function.comp, ray_bottcher m] at ec
State after:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : e = c
⊢ c ∈ multibrotExt d

State before:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : e = c
⊢ c ∈ multibrotExt d
Tactic:
rwa [← ec]
State after:
no goals

State before:
case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ multibrotExt d → ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c
Tactic:
intro m
State after:
case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c

State before:
case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c
Tactic:
use c, m, ray_bottcher m
State after:
no goals