internlm/Lean-Github huggingface dataset:
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ s
Tactic:
refine _root_.trans ?_ bs
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ closedBall (c.1, c.2) t
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ closedBall (c.1, c.2) t
Tactic:
simp_rw [← ball_prod_same, ← closedBall_prod_same, Set.prod_subset_prod_iff]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t ∨ ball c0' v = ∅ ∨ ball c.2 v = ∅
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t ∨ ball c0' v = ∅ ∨ ball c.2 v = ∅
Tactic:
apply Or.inl
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t
Tactic:
use _root_.trans (Metric.ball_subset_ball vr.le) us
Proof state after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c.2 v ⊆ closedBall c.2 t
Theorem: Pair.hartogs
Proof state before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c.2 v ⊆ closedBall c.2 t
Tactic:
have r1t := le_of_ball_subset_closedBall u.r1p.le tp.le us
Proof state after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
r1t : r1 ≤ t
⊢ ball c.2 v ⊆ closedBall c.2 t
Theorem: Pair.hartogs
Proof state before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
r1t : r1 ≤ t
⊢ ball c.2 v ⊆ closedBall c.2 t
Tactic:
exact _root_.trans Metric.ball_subset_closedBall
    (Metric.closedBall_subset_closedBall (_root_.trans vr.le r1t))
Proof state after:
no goals
Theorem: Pair.hartogs_at
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
c : ℂ × ℂ
fa0 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z0 => f (z0, p.2)) p.1
fa1 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z1 => f (p.1, z1)) p.2
⊢ AnalyticAt ℂ f c
Tactic:
rcases eventually_nhds_iff.mp (fa0.and fa1) with ⟨s, fa, o, cs⟩
Proof state after:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
c : ℂ × ℂ
fa0 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z0 => f (z0, p.2)) p.1
fa1 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z1 => f (p.1, z1)) p.2
s : Set (ℂ × ℂ)
fa : ∀ x ∈ s, AnalyticAt ℂ (fun z0 => f (z0, x.2)) x.1 ∧ AnalyticAt ℂ (fun z1 => f (x.1, z1)) x.2
o : IsOpen s
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs_at
Proof state before:
case intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
c : ℂ × ℂ
fa0 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z0 => f (z0, p.2)) p.1
fa1 : ∀ᶠ (p : ℂ × ℂ) in 𝓝 c, AnalyticAt ℂ (fun z1 => f (p.1, z1)) p.2
s : Set (ℂ × ℂ)
fa : ∀ x ∈ s, AnalyticAt ℂ (fun z0 => f (z0, x.2)) x.1 ∧ AnalyticAt ℂ (fun z1 => f (x.1, z1)) x.2
o : IsOpen s
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
exact Pair.hartogs o (fun c0 c1 m ↦ (fa _ m).1) (fun c0 c1 m ↦ (fa _ m).2) c cs
Proof state after:
no goals
Theorem: d_pos
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < d
Tactic:
linarith [two_le_d d]
Proof state after:
no goals
Theorem: d_gt_one
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 < d
Tactic:
linarith [two_le_d d]
Proof state after:
no goals
Theorem: d_minus_one_pos
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 < d - 1
Tactic:
have h := two_le_d d
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
h : 2 ≤ d
⊢ 0 < d - 1
Theorem: d_minus_one_pos
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
h : 2 ≤ d
⊢ 0 < d - 1
Tactic:
omega
Proof state after:
no goals
Theorem: one_le_d_minus_one
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≤ d - 1
Tactic:
have h := two_le_d d
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
h : 2 ≤ d
⊢ 1 ≤ d - 1
Theorem: one_le_d_minus_one
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
h : 2 ≤ d
⊢ 1 ≤ d - 1
Tactic:
omega
Proof state after:
no goals
Theorem: two_le_cast_d
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 2 ≤ ↑2
Tactic:
norm_num
Proof state after:
no goals
Theorem: multibrotExt_coe
Proof 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]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∃ x ∈ multibrot d, x = c) ↔ c ∈ multibrot d
Theorem: multibrotExt_coe
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∃ x ∈ multibrot d, x = c) ↔ c ∈ multibrot d
Tactic:
constructor
Proof 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
Theorem: multibrotExt_coe
Proof 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⟩
Proof 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
Theorem: multibrotExt_coe
Proof 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
Proof 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
Theorem: multibrotExt_coe
Proof 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
Proof state after:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c
Theorem: multibrotExt_coe
Proof state before:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∃ x ∈ multibrot d, x = c
Tactic:
intro m
Proof state after:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ ∃ x ∈ multibrot d, x = c
Theorem: multibrotExt_coe
Proof state before:
case mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ ∃ x ∈ multibrot d, x = c
Tactic:
use c, m
Proof state after:
no goals
Theorem: coe_preimage_multibrotExt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (fun z => ↑z) ⁻¹' multibrotExt d = (multibrot d)ᶜ
Tactic:
apply Set.ext
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ x ∈ (multibrot d)ᶜ
Theorem: coe_preimage_multibrotExt
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ x ∈ (multibrot d)ᶜ
Tactic:
intro z
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ z ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ z ∈ (multibrot d)ᶜ
Theorem: coe_preimage_multibrotExt
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ z ∈ (fun z => ↑z) ⁻¹' multibrotExt d ↔ z ∈ (multibrot d)ᶜ
Tactic:
simp only [mem_compl_iff, mem_preimage, multibrotExt_coe]
Proof state after:
no goals
Theorem: f_0'
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ f' d c 0 = c
Tactic:
simp only [lift_coe', f', zero_pow (d_ne_zero _), zero_add]
Proof state after:
no goals
Theorem: f_0
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ f d c 0 = ↑c
Tactic:
simp only [f, ← coe_zero, lift_coe', f', zero_pow (d_ne_zero _), zero_add]
Proof state after:
no goals
Theorem: deriv_f'
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Tactic:
have h : HasDerivAt (f' d c) (d * z ^ (d - 1) + 0) z :=
  (hasDerivAt_pow _ _).add (hasDerivAt_const _ _)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1) + 0) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Theorem: deriv_f'
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1) + 0) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Tactic:
simp only [add_zero] at h
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1)) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Theorem: deriv_f'
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
h : HasDerivAt (f' d c) (↑d * z ^ (d - 1)) z
⊢ deriv (f' d c) z = ↑d * z ^ (d - 1)
Tactic:
exact h.deriv
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ Tendsto (uncurry (f' d)) (𝓝 c ×ˢ atInf) atInf
Tactic:
simp only [atInf_basis.tendsto_right_iff, Complex.norm_eq_abs, Set.mem_setOf_eq,
  forall_true_left, uncurry, Metric.eventually_nhds_prod_iff]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ ∀ (i : ℝ),
    ∃ ε > 0,
      ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i_1 : ℂ}, pa i_1 → i < Complex.abs (f' d x i_1)
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ ∀ (i : ℝ),
    ∃ ε > 0,
      ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i_1 : ℂ}, pa i_1 → i < Complex.abs (f' d x i_1)
Tactic:
intro r
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i : ℂ}, pa i → r < Complex.abs (f' d x i)
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ℂ) in atInf, pa i) ∧ ∀ {x : ℂ}, dist x c < ε → ∀ {i : ℂ}, pa i → r < Complex.abs (f' d x i)
Tactic:
use 1, zero_lt_one, fun z ↦ max r 0 + abs c + 1 < abs z
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ (∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i) ∧
    ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)
Theorem: tendsto_f'_atInf
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ (∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i) ∧
    ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)
Tactic:
constructor
Proof state after:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i

case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)
Theorem: tendsto_f'_atInf
Proof state before:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ᶠ (i : ℂ) in atInf, max r 0 + Complex.abs c + 1 < Complex.abs i
Tactic:
refine (eventually_atInf (max r 0 + abs c + 1)).mp (eventually_of_forall fun w h ↦ ?_)
Proof state after:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : ‖w‖ > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w
Theorem: tendsto_f'_atInf
Proof state before:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : ‖w‖ > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w
Tactic:
simp only [Complex.norm_eq_abs] at h
Proof state after:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : Complex.abs w > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w
Theorem: tendsto_f'_atInf
Proof state before:
case h.left
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
w : ℂ
h : Complex.abs w > max r 0 + Complex.abs c + 1
⊢ max r 0 + Complex.abs c + 1 < Complex.abs w
Tactic:
exact h
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
⊢ ∀ {x : ℂ}, dist x c < 1 → ∀ {i : ℂ}, max r 0 + Complex.abs c + 1 < Complex.abs i → r < Complex.abs (f' d x i)
Tactic:
intro e ec z h
Proof state after:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : dist e c < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)
Theorem: tendsto_f'_atInf
Proof state before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : dist e c < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)
Tactic:
simp only [Complex.dist_eq] at ec
Proof state after:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)
Theorem: tendsto_f'_atInf
Proof state before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ r < Complex.abs (f' d e z)
Tactic:
have zz : abs z ≤ abs (z ^ d) := by
  rw [Complex.abs.map_pow]
  refine le_self_pow ?_ (d_ne_zero _)
  exact le_trans (le_add_of_nonneg_left (add_nonneg (le_max_right _ _) (Complex.abs.nonneg _)))
    h.le
Proof state after:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ r < Complex.abs (f' d e z)
Theorem: tendsto_f'_atInf
Proof state before:
case h.right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ r < Complex.abs (f' d e z)
Tactic:
calc abs (f' d e z)
  _ = abs (z ^ d + e) := rfl
  _ = abs (z ^ d + (c + (e - c))) := by ring_nf
  _ ≥ abs (z ^ d) - abs (c + (e - c)) := by bound
  _ ≥ abs (z ^ d) - (abs c + abs (e - c)) := by bound
  _ ≥ abs z - (abs c + 1) := by bound
  _ > max r 0 + abs c + 1 - (abs c + 1) := by bound
  _ = max r 0 := by ring_nf
  _ ≥ r := le_max_left _ _
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ Complex.abs z ≤ Complex.abs (z ^ d)
Tactic:
rw [Complex.abs.map_pow]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z ^ d
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ Complex.abs z ≤ Complex.abs z ^ d
Tactic:
refine le_self_pow ?_ (d_ne_zero _)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ 1 ≤ Complex.abs z
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
⊢ 1 ≤ Complex.abs z
Tactic:
exact le_trans (le_add_of_nonneg_left (add_nonneg (le_max_right _ _) (Complex.abs.nonneg _)))
  h.le
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d + e) = Complex.abs (z ^ d + (c + (e - c)))
Tactic:
ring_nf
Proof state after:
no goals