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

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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
m : z ∈ bottcher d '' multibrotExt d
⊢ bottcher d (ray d z) = z
Tactic:
rcases m with ⟨c, m, cz⟩
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
cz : bottcher d c = z
⊢ bottcher d (ray d z) = z

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
cz : bottcher d c = z
⊢ bottcher d (ray d z) = z
Tactic:
nth_rw 1 [← cz]
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
cz : bottcher d c = z
⊢ bottcher d (ray d (bottcher d c)) = z

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
cz : bottcher d c = z
⊢ bottcher d (ray d (bottcher d c)) = z
Tactic:
rw [ray_bottcher m]
State after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
cz : bottcher d c = z
⊢ bottcher d c = z

State before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
c : 𝕊
m : c ∈ multibrotExt d
cz : bottcher d c = z
⊢ bottcher d c = z
Tactic:
exact cz
State after:
no goals