internlm/Lean-Github huggingface dataset:
Theorem: duals_lim_tendsto_maxLog_norm
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
b : ℝ
x : E
⊢ Filter.Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) x‖)) atTop (𝓝 (maxLog b ‖x‖))
Tactic:
rw [maxLog_norm_eq_duals_iSup]
Proof state after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
b : ℝ
x : E
⊢ Filter.Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) x‖)) atTop (𝓝 (⨆ n, maxLog b ‖(duals n) x‖))
Theorem: duals_lim_tendsto_maxLog_norm
Proof state before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
b : ℝ
x : E
⊢ Filter.Tendsto (⇑(partialSups fun k => maxLog b ‖(duals k) x‖)) atTop (𝓝 (⨆ n, maxLog b ‖(duals n) x‖))
Tactic:
exact Csupr.has_lim _ (duals_bddAbove (monotone_maxLog _) _)
Proof state after:
no goals
Theorem: isPathConnected_multibrotExt
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (multibrotExt d)
Tactic:
rw [← ray_surj d]
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ray d '' ball 0 1)
Theorem: isPathConnected_multibrotExt
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ray d '' ball 0 1)
Tactic:
apply IsPathConnected.image_of_continuousOn
Proof state after:
case sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ball 0 1)

case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)
Theorem: isPathConnected_multibrotExt
Proof state before:
case sc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsPathConnected (ball 0 1)

case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)
Tactic:
exact (convex_ball _ _).isPathConnected (Metric.nonempty_ball.mpr one_pos)
Proof state after:
case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)
Theorem: isPathConnected_multibrotExt
Proof state before:
case fc
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ContinuousOn (ray d) (ball 0 1)
Tactic:
exact (rayHolomorphic d).continuousOn
Proof state after:
no goals
Theorem: isPathConnected_potential_levelset
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ IsPathConnected (potential d ⁻¹' {p})
Tactic:
rw [e]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ IsPathConnected (ray d '' sphere 0 p)
Theorem: isPathConnected_potential_levelset
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ IsPathConnected (ray d '' sphere 0 p)
Tactic:
apply (isPathConnected_sphere p0).image_of_continuousOn
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ ContinuousOn (ray d) (sphere 0 p)
Theorem: isPathConnected_potential_levelset
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ ContinuousOn (ray d) (sphere 0 p)
Tactic:
exact (rayHolomorphic d).continuousOn.mono (Metric.sphere_subset_ball p1)
Proof state after:
no goals
Theorem: isPathConnected_potential_levelset
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
⊢ potential d ⁻¹' {p} = ray d '' sphere 0 p
Tactic:
apply Set.ext
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
⊢ ∀ (x : 𝕊), x ∈ potential d ⁻¹' {p} ↔ x ∈ ray d '' sphere 0 p
Theorem: isPathConnected_potential_levelset
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
⊢ ∀ (x : 𝕊), x ∈ potential d ⁻¹' {p} ↔ x ∈ ray d '' sphere 0 p
Tactic:
intro c
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ c ∈ potential d ⁻¹' {p} ↔ c ∈ ray d '' sphere 0 p
Theorem: isPathConnected_potential_levelset
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ c ∈ potential d ⁻¹' {p} ↔ c ∈ ray d '' sphere 0 p
Tactic:
simp only [mem_preimage, mem_singleton_iff, ← abs_bottcher, mem_image, mem_sphere,
  Complex.dist_eq, sub_zero]
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p ↔ ∃ x, Complex.abs x = p ∧ ray d x = c
Theorem: isPathConnected_potential_levelset
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p ↔ ∃ x, Complex.abs x = p ∧ ray d x = c
Tactic:
constructor
Proof state after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p → ∃ x, Complex.abs x = p ∧ ray d x = c

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ (∃ x, Complex.abs x = p ∧ ray d x = c) → Complex.abs (bottcher d c) = p
Theorem: isPathConnected_potential_levelset
Proof state before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p → ∃ x, Complex.abs x = p ∧ ray d x = c
Tactic:
intro h
Proof state after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ∃ x, Complex.abs x = p ∧ ray d x = c
Theorem: isPathConnected_potential_levelset
Proof state before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ∃ x, Complex.abs x = p ∧ ray d x = c
Tactic:
use bottcher d c
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ Complex.abs (bottcher d c) = p ∧ ray d (bottcher d c) = c
Theorem: isPathConnected_potential_levelset
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ Complex.abs (bottcher d c) = p ∧ ray d (bottcher d c) = c
Tactic:
use h
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ray d (bottcher d c) = c
Theorem: isPathConnected_potential_levelset
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ray d (bottcher d c) = c
Tactic:
rw [ray_bottcher]
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ c ∈ multibrotExt d
Theorem: isPathConnected_potential_levelset
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ c ∈ multibrotExt d
Tactic:
rw [← potential_lt_one, ← abs_bottcher, h]
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ p < 1
Theorem: isPathConnected_potential_levelset
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ p < 1
Tactic:
exact p1
Proof state after:
no goals
Theorem: isPathConnected_potential_levelset
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ (∃ x, Complex.abs x = p ∧ ray d x = c) → Complex.abs (bottcher d c) = p
Tactic:
intro ⟨e, ep, ec⟩
Proof state after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs (bottcher d c) = p
Theorem: isPathConnected_potential_levelset
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs (bottcher d c) = p
Tactic:
rw [← ec, bottcher_ray]
Proof state after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs e = p

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1
Theorem: isPathConnected_potential_levelset
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs e = p

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1
Tactic:
exact ep
Proof state after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1
Theorem: isPathConnected_potential_levelset
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1
Tactic:
simp only [mem_ball, Complex.dist_eq, sub_zero, ep, p1]
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsConnected (multibrotExt d)ᶜ
Tactic:
refine ⟨⟨((0 : ℂ) : 𝕊),?_⟩,?_⟩
Proof 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)ᶜ
Theorem: isConnected_compl_multibrotExt
Proof 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⟩
Proof 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)ᶜ
Theorem: isConnected_compl_multibrotExt
Proof 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]
Proof 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)
Theorem: isConnected_compl_multibrotExt
Proof 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 _ _ _ _ ?_ _ ?_ ?_ ?_
Proof 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)
Theorem: isConnected_compl_multibrotExt
Proof 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]
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (multibrotExt d)ᶜ = ⋂ p, potential d ⁻¹' Ici ↑p
Tactic:
apply Set.ext
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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]
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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⟩
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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 ⊢
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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 ⊢
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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⟩
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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⟩
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof 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⟩
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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⟩⟩, ?_, ?_⟩
Proof 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, ⋯⟩
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof 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, ⋯⟩
Theorem: isConnected_compl_multibrotExt
Proof 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 ⊢
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof 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, ⋯⟩
Theorem: isConnected_compl_multibrotExt
Proof 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 ⊢
Proof 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
Theorem: isConnected_compl_multibrotExt
Proof 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
Proof state after:
no goals
Theorem: isConnected_compl_multibrotExt
Proof 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⟩
Proof 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⟩)