internlm/Lean-Github huggingface dataset:
Theorem: HolomorphicAt.local_inj''
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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ (𝓝 (f c z)).EventuallyEq (fun w => w) fun z => f c (g c z)
Tactic:
refine ((continuousAt_const.prod continuousAt_id).eventually fg).mp (eventually_of_forall ?_)
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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ ∀ (x : T), f (c, id x).1 (g (c, id x).1 (c, id x).2) = (c, id x).2 → (fun w => w) x = (fun z => f c (g c z)) x
Theorem: HolomorphicAt.local_inj''
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
c : ℂ
z : S
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, g c (f c z))
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
e : (c, z) = (c, g c (f c z))
⊢ ∀ (x : T), f (c, id x).1 (g (c, id x).1 (c, id x).2) = (c, id x).2 → (fun w => w) x = (fun z => f c (g c z)) x
Tactic:
exact fun _ e ↦ e.symm
Proof state after:
no goals
Theorem: HolomorphicAt.local_inj''
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ (c, z) = (c, g c (f c z))
Tactic:
rw [gf.self_of_nhds]
Proof state after:
no goals
Theorem: HolomorphicAt.local_inj'
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
⊢ ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, z, z), f p.1 p.2.1 = f p.1 p.2.2 → p.2.1 = p.2.2
Tactic:
set g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p ↦ ((p.1, p.2.1), (p.1, p.2.2))
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, z, z), f p.1 p.2.1 = f p.1 p.2.2 → p.2.1 = p.2.2
Theorem: HolomorphicAt.local_inj'
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
⊢ ∀ᶠ (p : ℂ × S × S) in 𝓝 (c, z, z), f p.1 p.2.1 = f p.1 p.2.2 → p.2.1 = p.2.2
Tactic:
refine (t.eventually (fa.local_inj'' nc)).mp (eventually_of_forall ?_)
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
⊢ ∀ (x : ℂ × S × S),
    ((g x).1.1 = (g x).2.1 → f (g x).1.1 (g x).1.2 = f (g x).2.1 (g x).2.2 → (g x).1 = (g x).2) →
      f x.1 x.2.1 = f x.1 x.2.2 → x.2.1 = x.2.2
Theorem: HolomorphicAt.local_inj'
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
⊢ ∀ (x : ℂ × S × S),
    ((g x).1.1 = (g x).2.1 → f (g x).1.1 (g x).1.2 = f (g x).2.1 (g x).2.2 → (g x).1 = (g x).2) →
      f x.1 x.2.1 = f x.1 x.2.2 → x.2.1 = x.2.2
Tactic:
intro ⟨e, x, y⟩ inj fe
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
e : ℂ
x y : S
inj :
  (g (e, x, y)).1.1 = (g (e, x, y)).2.1 →
    f (g (e, x, y)).1.1 (g (e, x, y)).1.2 = f (g (e, x, y)).2.1 (g (e, x, y)).2.2 → (g (e, x, y)).1 = (g (e, x, y)).2
fe : f (e, x, y).1 (e, x, y).2.1 = f (e, x, y).1 (e, x, y).2.2
⊢ (e, x, y).2.1 = (e, x, y).2.2
Theorem: HolomorphicAt.local_inj'
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
t : Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
e : ℂ
x y : S
inj :
  (g (e, x, y)).1.1 = (g (e, x, y)).2.1 →
    f (g (e, x, y)).1.1 (g (e, x, y)).1.2 = f (g (e, x, y)).2.1 (g (e, x, y)).2.2 → (g (e, x, y)).1 = (g (e, x, y)).2
fe : f (e, x, y).1 (e, x, y).2.1 = f (e, x, y).1 (e, x, y).2.2
⊢ (e, x, y).2.1 = (e, x, y).2.2
Tactic:
exact (Prod.ext_iff.mp (inj rfl fe)).2
Proof state after:
no goals
Theorem: HolomorphicAt.local_inj'
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Tendsto g (𝓝 (c, z, z)) (𝓝 ((c, z), c, z))
Tactic:
apply Continuous.continuousAt
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous g
Theorem: HolomorphicAt.local_inj'
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous g
Tactic:
apply Continuous.prod_mk
Proof state after:
case h.hf
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.1)

case h.hg
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.2)
Theorem: HolomorphicAt.local_inj'
Proof state before:
case h.hf
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.1)
Tactic:
exact continuous_fst.prod_mk (continuous_fst.comp continuous_snd)
Proof state after:
no goals
Theorem: HolomorphicAt.local_inj'
Proof state before:
case h.hg
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
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ × S × S → (ℂ × S) × ℂ × S := fun p => ((p.1, p.2.1), p.1, p.2.2)
⊢ Continuous fun x => (x.1, x.2.2)
Tactic:
exact continuous_fst.prod_mk (continuous_snd.comp continuous_snd)
Proof state after:
no goals
Theorem: Super.ext_slice
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
c : ℂ
⊢ {x | (c, x) ∈ s.ext} = ball 0 (s.p c)
Tactic:
apply Set.ext
Proof state after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
c : ℂ
⊢ ∀ (x : ℂ), x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)
Theorem: Super.ext_slice
Proof state before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
c : ℂ
⊢ ∀ (x : ℂ), x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)
Tactic:
intro x
Proof state after:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
c x : ℂ
⊢ x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)
Theorem: Super.ext_slice
Proof state before:
case h
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
c x : ℂ
⊢ x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)
Tactic:
simp only [Super.ext, mem_ball, mem_setOf, Complex.dist_eq, sub_zero]
Proof state after:
no goals
Theorem: Super.isOpen_ext
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ IsOpen s.ext
Tactic:
set f := fun y : ℂ × ℂ ↦ s.p y.1 - abs y.2
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
⊢ IsOpen s.ext
Theorem: Super.isOpen_ext
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
⊢ IsOpen s.ext
Tactic:
have fc : LowerSemicontinuous f :=
  (s.lowerSemicontinuous_p.comp continuous_fst).add
    (Complex.continuous_abs.comp continuous_snd).neg.lowerSemicontinuous
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
⊢ IsOpen s.ext
Theorem: Super.isOpen_ext
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
⊢ IsOpen s.ext
Tactic:
have e : s.ext = f ⁻¹' Ioi 0 :=
  Set.ext fun _ ↦ by simp only [Super.ext, mem_setOf, mem_preimage, mem_Ioi, sub_pos, f]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = f ⁻¹' Ioi 0
⊢ IsOpen s.ext
Theorem: Super.isOpen_ext
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = f ⁻¹' Ioi 0
⊢ IsOpen s.ext
Tactic:
rw [e]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = f ⁻¹' Ioi 0
⊢ IsOpen (f ⁻¹' Ioi 0)
Theorem: Super.isOpen_ext
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = f ⁻¹' Ioi 0
⊢ IsOpen (f ⁻¹' Ioi 0)
Tactic:
exact fc.isOpen_preimage _
Proof state after:
no goals
Theorem: Super.isOpen_ext
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
x✝ : ℂ × ℂ
⊢ x✝ ∈ s.ext ↔ x✝ ∈ f ⁻¹' Ioi 0
Tactic:
simp only [Super.ext, mem_setOf, mem_preimage, mem_Ioi, sub_pos, f]
Proof state after:
no goals
Theorem: Super.mem_ext
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ (c, 0) ∈ s.ext
Tactic:
simp only [Super.ext, mem_setOf, Complex.abs.map_zero, s.p_pos c]
Proof state after:
no goals
Theorem: Super.ext_slice_connected
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ IsConnected {x | (c, x) ∈ s.ext}
Tactic:
rw [s.ext_slice c]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ IsConnected (ball 0 (s.p c))
Theorem: Super.ext_slice_connected
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ IsConnected (ball 0 (s.p c))
Tactic:
exact ⟨⟨(0 : ℂ), mem_ball_self (s.p_pos c)⟩, (convex_ball (0 : ℂ) (s.p c)).isPreconnected⟩
Proof state after:
no goals
Theorem: Super.ext_connected
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ IsConnected s.ext
Tactic:
refine ⟨⟨(0, 0), s.mem_ext 0⟩, isPreconnected_of_forall (0, 0) ?_⟩
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ ∀ y ∈ s.ext, ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ y ∈ t ∧ IsPreconnected t
Theorem: Super.ext_connected
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ ∀ y ∈ s.ext, ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
intro ⟨c, x⟩ m
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ (c, x) ∈ t ∧ IsPreconnected t
Theorem: Super.ext_connected
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ (c, x) ∈ t ∧ IsPreconnected t
Tactic:
use(fun x ↦ (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0}
Proof state after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ⊆ s.ext ∧
    (0, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
      (c, x) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
        IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Theorem: Super.ext_connected
Proof state before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ⊆ s.ext ∧
    (0, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
      (c, x) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
        IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Tactic:
simp only [mem_image, mem_union, union_subset_iff, mem_setOf, mem_prod_eq, mem_univ,
  true_and_iff, mem_singleton_iff, eq_self_iff_true, or_true_iff]
Proof state after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext ∧ univ ×ˢ {0} ⊆ s.ext) ∧
    ((∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0) ∧
      IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Theorem: Super.ext_connected
Proof state before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext ∧ univ ×ˢ {0} ⊆ s.ext) ∧
    ((∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0) ∧
      IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Tactic:
refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
Proof state after:
case h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext

case h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ univ ×ˢ {0} ⊆ s.ext

case h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0

case h.refine_4
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Theorem: Super.ext_connected
Proof state before:
case h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext
Tactic:
intro y n
Proof state after:
case h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y✝ : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : y ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}
⊢ y ∈ s.ext