internlm/Lean-Github huggingface dataset:
Theorem: ChartedSpace.t1Space
Proof state before:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
have e : t = (chartAt A y).source ∩ chartAt A y ⁻¹'
    ((chartAt A y).target \ {chartAt A y x}) := by
  apply Set.ext; intro z
  simp only [mem_diff, mem_singleton_iff, mem_inter_iff, mem_preimage]; constructor
  intro ⟨zm, zx⟩; use zm, PartialEquiv.map_source _ zm, (PartialEquiv.injOn _).ne zm xm zx
  intro ⟨zm, _, zx⟩; use zm, ((PartialEquiv.injOn _).ne_iff zm xm).mp zx
Proof state after:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
e :
  t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
case pos
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
e :
  t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
use t
Proof state after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
e :
  t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
⊢ x ∉ t ∧ IsOpen t ∧ y ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ t = (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Tactic:
apply Set.ext
Proof state after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∀ (x_1 : M),
    x_1 ∈ t ↔
      x_1 ∈
        (_root_.chartAt A y).source ∩
          ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Theorem: ChartedSpace.t1Space
Proof state before:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
⊢ ∀ (x_1 : M),
    x_1 ∈ t ↔
      x_1 ∈
        (_root_.chartAt A y).source ∩
          ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Tactic:
intro z
Proof state after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈
      (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Theorem: ChartedSpace.t1Space
Proof state before:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈
      (_root_.chartAt A y).source ∩ ↑(_root_.chartAt A y) ⁻¹' ((_root_.chartAt A y).target \ {↑(_root_.chartAt A y) x})
Tactic:
simp only [mem_diff, mem_singleton_iff, mem_inter_iff, mem_preimage]
Proof state after:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x
Theorem: ChartedSpace.t1Space
Proof state before:
case h
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t ↔
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x
Tactic:
constructor
Proof state after:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t →
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ t →
    z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Tactic:
intro ⟨zm, zx⟩
Proof state after:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
zx : z ∉ {x}
⊢ z ∈ (_root_.chartAt A y).source ∧
    ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
case h.mp
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
zx : z ∉ {x}
⊢ z ∈ (_root_.chartAt A y).source ∧
    ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x

case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Tactic:
use zm, PartialEquiv.map_source _ zm, (PartialEquiv.injOn _).ne zm xm zx
Proof state after:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
⊢ z ∈ (_root_.chartAt A y).source ∧
      ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target ∧ ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x →
    z ∈ t
Tactic:
intro ⟨zm, _, zx⟩
Proof state after:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
left✝ : ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target
zx : ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x
⊢ z ∈ t
Theorem: ChartedSpace.t1Space
Proof state before:
case h.mpr
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∈ (_root_.chartAt A y).source
t : Set M := (_root_.chartAt A y).source \ {x}
z : M
zm : z ∈ (_root_.chartAt A y).source
left✝ : ↑(_root_.chartAt A y) z ∈ (_root_.chartAt A y).target
zx : ¬↑(_root_.chartAt A y) z = ↑(_root_.chartAt A y) x
⊢ z ∈ t
Tactic:
use zm, ((PartialEquiv.injOn _).ne_iff zm xm).mp zx
Proof state after:
no goals
Theorem: ChartedSpace.t1Space
Proof state before:
case neg
A M : Type
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace A M
inst✝ : T1Space A
x y : M
m : y ≠ x
xm : x ∉ (_root_.chartAt A y).source
⊢ ∃ t, x ∉ t ∧ IsOpen t ∧ y ∈ t
Tactic:
use(chartAt A y).source, xm, (chartAt A y).open_source, mem_chart_source A y
Proof state after:
no goals
Theorem: ChartedSpace.regularSpace
Proof state before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
⊢ RegularSpace M
Tactic:
apply RegularSpace.ofExistsMemNhdsIsClosedSubset
Proof state after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
⊢ ∀ (x : M), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Theorem: ChartedSpace.regularSpace
Proof state before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
⊢ ∀ (x : M), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
intro x s n
Proof state after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Theorem: ChartedSpace.regularSpace
Proof state before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
set t := (chartAt A x).target ∩ (chartAt A x).symm ⁻¹' ((chartAt A x).source ∩ s)
Proof state after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Theorem: ChartedSpace.regularSpace
Proof state before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
have cn : (chartAt A x).source ∈ 𝓝 x :=
  (chartAt A x).open_source.mem_nhds (mem_chart_source A x)
Proof state after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Theorem: ChartedSpace.regularSpace
Proof state before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
have tn : t ∈ 𝓝 (chartAt A x x) := by
  apply Filter.inter_mem ((chartAt A x).open_target.mem_nhds (mem_chart_target A x))
  apply ((chartAt A x).continuousAt_symm (mem_chart_target _ _)).preimage_mem_nhds
  rw [(chartAt A x).left_inv (mem_chart_source _ _)]; exact Filter.inter_mem cn n
Proof state after:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
tn : t ∈ 𝓝 (↑(_root_.chartAt A x) x)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Theorem: ChartedSpace.regularSpace
Proof state before:
case h
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
tn : t ∈ 𝓝 (↑(_root_.chartAt A x) x)
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Tactic:
rcases local_compact_nhds tn with ⟨u, un, ut, uc⟩
Proof state after:
case h.intro.intro.intro
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
tn : t ∈ 𝓝 (↑(_root_.chartAt A x) x)
u : Set A
un : u ∈ 𝓝 (↑(_root_.chartAt A x) x)
ut : u ⊆ t
uc : IsCompact u
⊢ ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
Theorem: ChartedSpace.regularSpace
Proof state before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ t ∈ 𝓝 (↑(_root_.chartAt A x) x)
Tactic:
apply Filter.inter_mem ((chartAt A x).open_target.mem_nhds (mem_chart_target A x))
Proof state after:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s) ∈ 𝓝 (↑(_root_.chartAt A x) x)
Theorem: ChartedSpace.regularSpace
Proof state before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s) ∈ 𝓝 (↑(_root_.chartAt A x) x)
Tactic:
apply ((chartAt A x).continuousAt_symm (mem_chart_target _ _)).preimage_mem_nhds
Proof state after:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 (↑(_root_.chartAt A x).symm (↑(_root_.chartAt A x) x))
Theorem: ChartedSpace.regularSpace
Proof state before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 (↑(_root_.chartAt A x).symm (↑(_root_.chartAt A x) x))
Tactic:
rw [(chartAt A x).left_inv (mem_chart_source _ _)]
Proof state after:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 x
Theorem: ChartedSpace.regularSpace
Proof state before:
A M : Type
inst✝⁴ : TopologicalSpace A
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace A M
inst✝¹ : T2Space M
inst✝ : LocallyCompactSpace A
x : M
s : Set M
n : s ∈ 𝓝 x
t : Set A := (_root_.chartAt A x).target ∩ ↑(_root_.chartAt A x).symm ⁻¹' ((_root_.chartAt A x).source ∩ s)
cn : (_root_.chartAt A x).source ∈ 𝓝 x
⊢ (_root_.chartAt A x).source ∩ s ∈ 𝓝 x
Tactic:
exact Filter.inter_mem cn n
Proof state after:
no goals
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (⋯.potential c ↑z))
Tactic:
set s := superF d
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => Complex.abs ((f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 (s.potential c ↑z))
Tactic:
suffices h : Tendsto (fun n ↦ (abs ((f' d c)^[n] z) *
    s.potential c ↑((f' d c)^[n] z)) ^ (-((d ^ n : ℕ) : ℝ)⁻¹))
    atTop (𝓝 1) by
  replace h := h.mul_const (s.potential c z)
  simp only [div_mul_cancel₀ _ potential_pos.ne', one_mul, ← f_f'_iter, s.potential_eqn_iter,
    Real.mul_rpow (Complex.abs.nonneg _) (pow_nonneg s.potential_nonneg _),
    Real.pow_rpow_inv_natCast s.potential_nonneg (pow_ne_zero _ (d_ne_zero d)),
    Real.rpow_neg (pow_nonneg s.potential_nonneg _), ← div_eq_mul_inv] at h
  exact h
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z) * s.potential c ↑((f' d c)^[n] z)) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => (Complex.abs ((f' d c)^[n] z) * s.potential c ↑((f' d c)^[n] z)) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)
Tactic:
simp only [← s.abs_bottcher, ← Complex.abs.map_mul, mul_comm _ (s.bottcher _ _)]
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ Tendsto (fun n => Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) atTop (𝓝 1)
Tactic:
rw [Metric.tendsto_atTop]
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < ε
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < ε
Tactic:
intro r rp
Proof state after:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
r : ℝ
rp : r > 0
⊢ ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r
Theorem: tendsto_potential
Proof state before:
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
r : ℝ
rp : r > 0
⊢ ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r
Tactic:
rcases Metric.tendsto_atTop.mp ((bottcher_large_approx d c).comp (tendsto_iter_atInf d z3 cz))
    (min (1 / 2) (r / 4)) (by bound) with ⟨n, h⟩
Proof state after:
case intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
r : ℝ
rp : r > 0
n : ℕ
h : ∀ n_1 ≥ n, dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) n_1) 1 < min (1 / 2) (r / 4)
⊢ ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r
Theorem: tendsto_potential
Proof state before:
case intro
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
r : ℝ
rp : r > 0
n : ℕ
h : ∀ n_1 ≥ n, dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) n_1) 1 < min (1 / 2) (r / 4)
⊢ ∃ N, ∀ n ≥ N, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n] z) * (f' d c)^[n] z) ^ (-(↑(d ^ n))⁻¹)) 1 < r
Tactic:
use n
Proof state after:
case h
c z : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d OnePoint.infty := superF d
r : ℝ
rp : r > 0
n : ℕ
h : ∀ n_1 ≥ n, dist (((fun z => ⋯.bottcher c ↑z * z) ∘ fun n => (f' d c)^[n] z) n_1) 1 < min (1 / 2) (r / 4)
⊢ ∀ n_1 ≥ n, dist (Complex.abs (s.bottcher c ↑((f' d c)^[n_1] z) * (f' d c)^[n_1] z) ^ (-(↑(d ^ n_1))⁻¹)) 1 < r