internlm/Lean-Github huggingface dataset:
Theorem: bottcher_inj
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : ¬z ≠ x
⊢ ¬Complex.abs (bottcher d z) < Complex.abs (bottcher d x)
Tactic:
simp only [not_not, not_lt] at lt ⊢
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : z = x
⊢ Complex.abs (bottcher d x) ≤ Complex.abs (bottcher d z)
Theorem: bottcher_inj
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : bottcher d x ≠ 0
r : 𝕊 → 𝕊
ra : HolomorphicAt I I r x
rx : r x = x
e✝ : ∀ᶠ (x_1 : 𝕊) in 𝓝 x, x_1 ≠ x → r x_1 ≠ x_1 ∧ bottcher d (r x_1) = bottcher d x_1
h : ∃ᶠ (a : 𝕊) in 𝓝 x, Complex.abs (bottcher d a) < Complex.abs (bottcher d x)
z : 𝕊
e : z ≠ x → r z ≠ z ∧ bottcher d (r z) = bottcher d z
lt : z = x
⊢ Complex.abs (bottcher d x) ≤ Complex.abs (bottcher d z)
Tactic:
simp only [lt, le_refl]
Proof state after:
no goals
Theorem: bottcher_inj
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : ¬p ≠ 0
⊢ False
Tactic:
simp only [not_not] at p0
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p = 0
⊢ False
Theorem: bottcher_inj
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) x = 0
p0 : p = 0
⊢ False
Tactic:
rw [(p0i p0).1] at db
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) ∞ = 0
p0 : p = 0
⊢ False
Theorem: bottcher_inj
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
b1 : b < 1
u : Set 𝕊 := {c | potential d c ≤ b}
t0 : Set (𝕊 × 𝕊) := u ×ˢ u
t1 : Set (𝕊 × 𝕊) := {q | bottcher d q.1 = bottcher d q.2 ∧ q ∈ t0}
t2 : Set (𝕊 × 𝕊) := {q | q.1 ≠ q.2 ∧ q ∈ t1}
t2ne : t2.Nonempty
ue : u ⊆ multibrotExt d
t01 : t1 ⊆ t0
t12 : t2 ⊆ t1
uc : IsClosed u
t0c : IsClosed t0
t1c : IsClosed t1
t12' : closure t2 ⊆ t1
t2c' : IsCompact (closure t2)
t2ne' : (closure t2).Nonempty
pc : Continuous fun q => potential d q.1
x : 𝕊
m2 : (x, x) ∈ closure t2
p : ℝ
min : ∀ x ∈ closure t2, p ≤ potential d x.1
xp : potential d x = p
m1 : (x, x) ∈ t1
pb : p ≤ b
xm : x ∈ multibrotExt d
p0i : p = 0 → x = ∞ ∧ x = ∞
db : mfderiv I I (bottcher d) ∞ = 0
p0 : p = 0
⊢ False
Tactic:
exact bottcher_mfderiv_inf_ne_zero db
Proof state after:
no goals
Theorem: rayHolomorphic
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (ray d) (ball 0 1)
Tactic:
rw [← bottcher_surj d]
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (ray d) (bottcher d '' multibrotExt d)
Theorem: rayHolomorphic
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (ray d) (bottcher d '' multibrotExt d)
Tactic:
exact (Classical.choose_spec (ray_exists d)).1
Proof state after:
no goals
Theorem: bottcher_ray
Proof 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
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
m : z ∈ bottcher d '' multibrotExt d
⊢ bottcher d (ray d z) = z
Theorem: bottcher_ray
Proof 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⟩
Proof 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
Theorem: bottcher_ray
Proof 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]
Proof 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
Theorem: bottcher_ray
Proof 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]
Proof 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
Theorem: bottcher_ray
Proof 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
Proof state after:
no goals
Theorem: ray_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ray d '' ball 0 1 = multibrotExt d
Tactic:
rw [← bottcher_surj d]
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ray d '' (bottcher d '' multibrotExt d) = multibrotExt d
Theorem: ray_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ray d '' (bottcher d '' multibrotExt d) = multibrotExt d
Tactic:
apply Set.ext
Proof state after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : 𝕊), x ∈ ray d '' (bottcher d '' multibrotExt d) ↔ x ∈ multibrotExt d
Theorem: ray_surj
Proof state before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : 𝕊), x ∈ ray d '' (bottcher d '' multibrotExt d) ↔ x ∈ multibrotExt d
Tactic:
intro c
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ ray d '' (bottcher d '' multibrotExt d) ↔ c ∈ multibrotExt d
Theorem: ray_surj
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ ray d '' (bottcher d '' multibrotExt d) ↔ c ∈ multibrotExt d
Tactic:
simp only [← image_comp, mem_image]
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) ↔ c ∈ multibrotExt d
Theorem: ray_surj
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) ↔ c ∈ multibrotExt d
Tactic:
constructor
Proof state after:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) → c ∈ multibrotExt d

case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ multibrotExt d → ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c
Theorem: ray_surj
Proof state before:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ (∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c) → c ∈ multibrotExt d
Tactic:
intro ⟨e, m, ec⟩
Proof state after:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : (ray d ∘ bottcher d) e = c
⊢ c ∈ multibrotExt d
Theorem: ray_surj
Proof state before:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : (ray d ∘ bottcher d) e = c
⊢ c ∈ multibrotExt d
Tactic:
simp only [Function.comp, ray_bottcher m] at ec
Proof state after:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : e = c
⊢ c ∈ multibrotExt d
Theorem: ray_surj
Proof state before:
case h.mp
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c e : 𝕊
m : e ∈ multibrotExt d
ec : e = c
⊢ c ∈ multibrotExt d
Tactic:
rwa [← ec]
Proof state after:
no goals
Theorem: ray_surj
Proof state before:
case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ c ∈ multibrotExt d → ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c
Tactic:
intro m
Proof state after:
case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c
Theorem: ray_surj
Proof state before:
case h.mpr
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ ∃ x ∈ multibrotExt d, (ray d ∘ bottcher d) x = c
Tactic:
use c, m, ray_bottcher m
Proof state after:
no goals
Theorem: global_complex_inverse_fun_open
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have i : ∀ p : ℂ × S, p ∈ s → ComplexInverseFun.Cinv f p.1 p.2 := by
  intro ⟨c, z⟩ m; exact
    { fa := fa _ m
      nc := nc _ m }
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_open
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
generalize hg : (fun c w ↦
  if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_open
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
have ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ q : ℂ × T in 𝓝 (p.1, f p.1 p.2),
    g q.1 q.2 = (i p m).g q.1 q.2 := by
  intro ⟨c, z⟩ m; simp only
  have n := nontrivialHolomorphicAt_of_mfderiv_ne_zero (fa _ m).along_snd (nc _ m); simp only at n
  simp only [n.nhds_eq_map_nhds_param (fa _ m), Filter.eventually_map]
  apply (i _ m).left_inv.mp; apply (so.eventually_mem m).mp
  apply eventually_of_forall; intro ⟨e, w⟩ wm gf
  simp only at gf
  simp only [left _ _ wm, gf]
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_open
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∃ g, HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
use g
Proof state after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_open
Proof state before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s) ∧ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Tactic:
constructor
Proof state after:
case h.left
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ HolomorphicOn (I.prod I) I (uncurry g) ((fun p => (p.1, f p.1 p.2)) '' s)

case h.right
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
i : ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
g : ℂ → T → S
hg : (fun c w => if h : ∃ z, (c, z) ∈ s ∧ f c z = w then choose h else Classical.arbitrary S) = g
left : ∀ (c : ℂ) (z : S), (c, z) ∈ s → g c (f c z) = z
ge : ∀ (p : ℂ × S) (m : p ∈ s), ∀ᶠ (q : ℂ × T) in 𝓝 (p.1, f p.1 p.2), g q.1 q.2 = ⋯.g q.1 q.2
⊢ ∀ p ∈ s, g p.1 (f p.1 p.2) = p.2
Theorem: global_complex_inverse_fun_open
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
⊢ ∀ p ∈ s, ComplexInverseFun.Cinv f p.1 p.2
Tactic:
intro ⟨c, z⟩ m
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ComplexInverseFun.Cinv f (c, z).1 (c, z).2
Theorem: global_complex_inverse_fun_open
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
inst✝ : Nonempty S
s : Set (ℂ × S)
fa : HolomorphicOn (I.prod I) I (uncurry f) s
nc : ∀ p ∈ s, mfderiv I I (f p.1) p.2 ≠ 0
inj : InjOn (fun p => (p.1, f p.1 p.2)) s
so : IsOpen s
c : ℂ
z : S
m : (c, z) ∈ s
⊢ ComplexInverseFun.Cinv f (c, z).1 (c, z).2
Tactic:
exact
{ fa := fa _ m
nc := nc _ m }
Proof state after:
no goals