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

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ ↑c ∈ multibrotExt d ↔ c ∉ multibrot d
Tactic:
simp only [multibrotExt, mem_union, mem_singleton_iff, coe_eq_inf_iff, or_false_iff, mem_image,
  mem_compl_iff, coe_eq_coe, not_iff_not]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∃ x ∈ multibrot d, x = c) ↔ c ∈ multibrot d

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∃ x ∈ multibrot d, x = c) ↔ c ∈ multibrot d
Tactic:
constructor
State after:
case mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∃ x ∈ multibrot d, x = c) → c ∈ multibrot d

case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c

State before:
case mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∃ x ∈ multibrot d, x = c) → c ∈ multibrot d

case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c
Tactic:
intro ⟨x, m, e⟩
State after:
case mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c x : ℂ
m : x ∈ multibrot d
e : x = c
⊢ c ∈ multibrot d

case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c

State before:
case mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c x : ℂ
m : x ∈ multibrot d
e : x = c
⊢ c ∈ multibrot d

case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c
Tactic:
rw [e] at m
State after:
case mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c x : ℂ
m : c ∈ multibrot d
e : x = c
⊢ c ∈ multibrot d

case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c

State before:
case mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c x : ℂ
m : c ∈ multibrot d
e : x = c
⊢ c ∈ multibrot d

case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c
Tactic:
exact m
State after:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c

State before:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c
Tactic:
intro m
State after:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ ∃ x ∈ multibrot d, x = c

State before:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ ∃ x ∈ multibrot d, x = c
Tactic:
use c, m
State after:
no goals