Theorem: isConnected_compl_multibrotExt (Ray/Dynamics/Multibrot/Connected.lean)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsConnected (multibrotExt d)ᶜ
Tactic:
refine ⟨⟨((0 : ℂ) : 𝕊),?_⟩,?_⟩
State after:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑0 ∈ (multibrotExt d)ᶜ

case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPreconnected (multibrotExt d)ᶜ

State before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPreconnected (multibrotExt d)ᶜ
Tactic:
have e : (multibrotExt d)ᶜ = ⋂ p : Ico 0 (1 : ℝ), potential d ⁻¹' Ici p := by
  apply Set.ext; intro z
  simp only [mem_compl_iff, ← potential_lt_one, mem_iInter, mem_preimage, not_lt, mem_Ici]
  constructor; intro p1 ⟨q, m⟩; simp only [Subtype.coe_mk, mem_Ico] at m ⊢; linarith
  intro h; contrapose h; simp only [not_le, not_forall] at h ⊢
  rcases exists_between h with ⟨y, py, y1⟩
  exact ⟨⟨y, ⟨le_trans potential_nonneg py.le, y1⟩⟩, py⟩
State after:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ IsPreconnected (multibrotExt d)ᶜ

State before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ IsPreconnected (multibrotExt d)ᶜ
Tactic:
rw [e]
State after:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ IsPreconnected (⋂ p, potential d ⁻¹' Ici ↑p)

State before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ IsPreconnected (⋂ p, potential d ⁻¹' Ici ↑p)
Tactic:
refine @IsPreconnected.directed_iInter _ _ _ _ ?_ _ ?_ ?_ ?_
State after:
case refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ Nonempty ↑(Ico 0 1)

case refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ Directed Superset fun p => potential d ⁻¹' Ici ↑p

case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ ∀ (a : ↑(Ico 0 1)), IsPreconnected (potential d ⁻¹' Ici ↑a)

case refine_2.refine_4
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ ∀ (a : ↑(Ico 0 1)), IsCompact (potential d ⁻¹' Ici ↑a)

State before:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ↑0 ∈ (multibrotExt d)ᶜ
Tactic:
simp only [mem_compl_iff, multibrotExt_coe, not_not, multibrot_zero]
State after:
no goals

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
Tactic:
apply Set.ext
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : 𝕊), x ∈ (multibrotExt d)ᶜ ↔ x ∈ ⋂ p, potential d ⁻¹' Ici ↑p

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : 𝕊), x ∈ (multibrotExt d)ᶜ ↔ x ∈ ⋂ p, potential d ⁻¹' Ici ↑p
Tactic:
intro z
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ z ∈ (multibrotExt d)ᶜ ↔ z ∈ ⋂ p, potential d ⁻¹' Ici ↑p

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ z ∈ (multibrotExt d)ᶜ ↔ z ∈ ⋂ p, potential d ⁻¹' Ici ↑p
Tactic:
simp only [mem_compl_iff, ← potential_lt_one, mem_iInter, mem_preimage, not_lt, mem_Ici]
State after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ 1 ≤ potential d z ↔ ∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z

State before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ 1 ≤ potential d z ↔ ∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z
Tactic:
constructor
State after:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ 1 ≤ potential d z → ∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z

State before:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ 1 ≤ potential d z → ∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z
Tactic:
intro p1 ⟨q, m⟩
State after:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
p1 : 1 ≤ potential d z
q : ℝ
m : q ∈ Ico 0 1
⊢ ↑⟨q, m⟩ ≤ potential d z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z

State before:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
p1 : 1 ≤ potential d z
q : ℝ
m : q ∈ Ico 0 1
⊢ ↑⟨q, m⟩ ≤ potential d z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z
Tactic:
simp only [Subtype.coe_mk, mem_Ico] at m ⊢
State after:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
p1 : 1 ≤ potential d z
q : ℝ
m : 0 ≤ q ∧ q < 1
⊢ q ≤ potential d z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z

State before:
case h.mp
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
p1 : 1 ≤ potential d z
q : ℝ
m : 0 ≤ q ∧ q < 1
⊢ q ≤ potential d z

case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z
Tactic:
linarith
State after:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z

State before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
⊢ (∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z) → 1 ≤ potential d z
Tactic:
intro h
State after:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : ∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z
⊢ 1 ≤ potential d z

State before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : ∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z
⊢ 1 ≤ potential d z
Tactic:
contrapose h
State after:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : ¬1 ≤ potential d z
⊢ ¬∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z

State before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : ¬1 ≤ potential d z
⊢ ¬∀ (i : ↑(Ico 0 1)), ↑i ≤ potential d z
Tactic:
simp only [not_le, not_forall] at h ⊢
State after:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : potential d z < 1
⊢ ∃ x, potential d z < ↑x

State before:
case h.mpr
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : potential d z < 1
⊢ ∃ x, potential d z < ↑x
Tactic:
rcases exists_between h with ⟨y, py, y1⟩
State after:
case h.mpr.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : potential d z < 1
y : ℝ
py : potential d z < y
y1 : y < 1
⊢ ∃ x, potential d z < ↑x

State before:
case h.mpr.intro.intro
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : 𝕊
h : potential d z < 1
y : ℝ
py : potential d z < y
y1 : y < 1
⊢ ∃ x, potential d z < ↑x
Tactic:
exact ⟨⟨y, ⟨le_trans potential_nonneg py.le, y1⟩⟩, py⟩
State after:
no goals

State before:
case refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ Nonempty ↑(Ico 0 1)
Tactic:
exact Zero.instNonempty
State after:
no goals

State before:
case refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ Directed Superset fun p => potential d ⁻¹' Ici ↑p
Tactic:
intro ⟨a, a0, a1⟩ ⟨b, b0, b1⟩
State after:
case refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
⊢ ∃ z,
    (fun p => potential d ⁻¹' Ici ↑p) ⟨a, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) z ∧
      (fun p => potential d ⁻¹' Ici ↑p) ⟨b, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) z

State before:
case refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
⊢ ∃ z,
    (fun p => potential d ⁻¹' Ici ↑p) ⟨a, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) z ∧
      (fun p => potential d ⁻¹' Ici ↑p) ⟨b, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) z
Tactic:
refine ⟨⟨max a b, mem_Ico.mpr ⟨le_max_of_le_left a0, max_lt a1 b1⟩⟩, ?_, ?_⟩
State after:
case refine_2.refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
⊢ (fun p => potential d ⁻¹' Ici ↑p) ⟨a, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩

case refine_2.refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
⊢ (fun p => potential d ⁻¹' Ici ↑p) ⟨b, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩

State before:
case refine_2.refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
⊢ (fun p => potential d ⁻¹' Ici ↑p) ⟨a, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩
Tactic:
intro z h
State after:
case refine_2.refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩
⊢ z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨a, ⋯⟩

State before:
case refine_2.refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩
⊢ z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨a, ⋯⟩
Tactic:
simp only [mem_preimage, mem_Ici, Subtype.coe_mk, max_le_iff] at h ⊢
State after:
case refine_2.refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : a ≤ potential d z ∧ b ≤ potential d z
⊢ a ≤ potential d z

State before:
case refine_2.refine_2.refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : a ≤ potential d z ∧ b ≤ potential d z
⊢ a ≤ potential d z
Tactic:
exact h.1
State after:
no goals

State before:
case refine_2.refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
⊢ (fun p => potential d ⁻¹' Ici ↑p) ⟨b, ⋯⟩ ⊇ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩
Tactic:
intro z h
State after:
case refine_2.refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩
⊢ z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨b, ⋯⟩

State before:
case refine_2.refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨max a b, ⋯⟩
⊢ z ∈ (fun p => potential d ⁻¹' Ici ↑p) ⟨b, ⋯⟩
Tactic:
simp only [mem_preimage, mem_Ici, Subtype.coe_mk, max_le_iff] at h ⊢
State after:
case refine_2.refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : a ≤ potential d z ∧ b ≤ potential d z
⊢ b ≤ potential d z

State before:
case refine_2.refine_2.refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
a : ℝ
a0 : 0 ≤ a
a1 : a < 1
b : ℝ
b0 : 0 ≤ b
b1 : b < 1
z : 𝕊
h : a ≤ potential d z ∧ b ≤ potential d z
⊢ b ≤ potential d z
Tactic:
exact h.2
State after:
no goals

State before:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ ∀ (a : ↑(Ico 0 1)), IsPreconnected (potential d ⁻¹' Ici ↑a)
Tactic:
intro ⟨p, m⟩
State after:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPreconnected (potential d ⁻¹' Ici ↑⟨p, m⟩)

State before:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPreconnected (potential d ⁻¹' Ici ↑⟨p, m⟩)
Tactic:
simp only [Subtype.coe_mk]
State after:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPreconnected (potential d ⁻¹' Ici p)

State before:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPreconnected (potential d ⁻¹' Ici p)
Tactic:
refine IsConnected.isPreconnected (IsPathConnected.isConnected ?_)
State after:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' Ici p)

State before:
case refine_2.refine_3
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' Ici p)
Tactic:
apply IsPathConnected.of_frontier
State after:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' frontier (Ici p))

case refine_2.refine_3.fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ Continuous (potential d)

case refine_2.refine_3.sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsClosed (Ici p)

State before:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' frontier (Ici p))
Tactic:
rw [frontier_Ici]
State after:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' {p})

State before:
case refine_2.refine_3.pc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsPathConnected (potential d ⁻¹' {p})
Tactic:
exact isPathConnected_potential_levelset _ m.1 m.2
State after:
no goals

State before:
case refine_2.refine_3.fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ Continuous (potential d)
Tactic:
exact potential_continuous
State after:
no goals

State before:
case refine_2.refine_3.sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsClosed (Ici p)
Tactic:
exact isClosed_Ici
State after:
no goals

State before:
case refine_2.refine_4
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
⊢ ∀ (a : ↑(Ico 0 1)), IsCompact (potential d ⁻¹' Ici ↑a)
Tactic:
intro ⟨p, m⟩
State after:
case refine_2.refine_4
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsCompact (potential d ⁻¹' Ici ↑⟨p, m⟩)

State before:
case refine_2.refine_4
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
e : (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
p : ℝ
m : p ∈ Ico 0 1
⊢ IsCompact (potential d ⁻¹' Ici ↑⟨p, m⟩)
Tactic:
exact (isClosed_Ici.preimage potential_continuous).isCompact
State after:
no goals