internlm/Lean-Github huggingface dataset:
Theorem: Super.potential_eq_zero
Proof state before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a
Tactic:
rw [not_exists] at r
Proof state after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ∃ n, (f c)^[n] z = a
Theorem: Super.potential_eq_zero
Proof state before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ∃ n, (f c)^[n] z = a
Tactic:
simp only [s.potential_eq_one r, one_ne_zero] at h
Proof state after:
no goals
Theorem: Super.potential_eq_zero
Proof state before:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ (∃ n, (f c)^[n] z = a) → s.potential c z = 0
Tactic:
intro p
Proof state after:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ∃ n, (f c)^[n] z = a
⊢ s.potential c z = 0
Theorem: Super.potential_eq_zero
Proof state before:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ∃ n, (f c)^[n] z = a
⊢ s.potential c z = 0
Tactic:
rcases p with ⟨n, p⟩
Proof state after:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
⊢ s.potential c z = 0
Theorem: Super.potential_eq_zero
Proof state before:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
⊢ s.potential c z = 0
Tactic:
have nz : d^n > 0 := pow_pos s.dp _
Proof state after:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
nz : d ^ n > 0
⊢ s.potential c z = 0
Theorem: Super.potential_eq_zero
Proof state before:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
nz : d ^ n > 0
⊢ s.potential c z = 0
Tactic:
rw [← pow_eq_zero_iff nz.ne', ← s.potential_eqn_iter n, p, s.potential_a]
Proof state after:
no goals
Theorem: UpperSemicontinuous.potential
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ UpperSemicontinuous (uncurry s.potential)
Tactic:
intro ⟨c, z⟩
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✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
Theorem: UpperSemicontinuous.potential
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✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
by_cases r : ∃ n, (c, (f c)^[n] z) ∈ s.near
Proof state after:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)

case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
Theorem: UpperSemicontinuous.potential
Proof state before:
case pos
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
exact (ContinuousAt.potential_of_reaches s r).upperSemicontinuousAt
Proof state after:
no goals
Theorem: UpperSemicontinuous.potential
Proof state before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
simp only [uncurry, UpperSemicontinuousAt, s.potential_eq_one (not_exists.mp r)]
Proof state after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ (y : ℝ), 1 < y → ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), s.potential x'.1 x'.2 < y
Theorem: UpperSemicontinuous.potential
Proof state before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ (y : ℝ), 1 < y → ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), s.potential x'.1 x'.2 < y
Tactic:
exact fun y y1 ↦ eventually_of_forall fun p ↦ lt_of_le_of_lt s.potential_le_one y1
Proof state after:
no goals
Theorem: Super.preimage_eq'
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
⊢ f c z = a ↔ z = a
Tactic:
have e := o.eq_a c z
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
e : f c z = a → z = a
⊢ f c z = a ↔ z = a
Theorem: Super.preimage_eq'
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
e : f c z = a → z = a
⊢ f c z = a ↔ z = a
Tactic:
refine ⟨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 : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
e : f c z = a → z = a
⊢ z = a → f c z = a
Theorem: Super.preimage_eq'
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
e : f c z = a → z = a
⊢ z = a → f c z = a
Tactic:
intro 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
e✝ : f c z = a → z = a
e : z = a
⊢ f c z = a
Theorem: Super.preimage_eq'
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
e✝ : f c z = a → z = a
e : z = a
⊢ f c z = a
Tactic:
simp only [e, s.f0]
Proof state after:
no goals
Theorem: Super.preimage_eq
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
o : OnePreimage s
n : ℕ
⊢ (f c)^[n] z = a ↔ z = a
Tactic:
induction' n with n h
Proof state after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
⊢ (f c)^[0] z = a ↔ z = a

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
o : OnePreimage s
n : ℕ
h : (f c)^[n] z = a ↔ z = a
⊢ (f c)^[n + 1] z = a ↔ z = a
Theorem: Super.preimage_eq
Proof state before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
o : OnePreimage s
⊢ (f c)^[0] z = a ↔ z = a

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
o : OnePreimage s
n : ℕ
h : (f c)^[n] z = a ↔ z = a
⊢ (f c)^[n + 1] z = a ↔ z = a
Tactic:
simp only [Function.iterate_zero_apply]
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
o : OnePreimage s
n : ℕ
h : (f c)^[n] z = a ↔ z = a
⊢ (f c)^[n + 1] z = a ↔ z = a
Theorem: Super.preimage_eq
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
o : OnePreimage s
n : ℕ
h : (f c)^[n] z = a ↔ z = a
⊢ (f c)^[n + 1] z = a ↔ z = a
Tactic:
simp only [Function.iterate_succ_apply', s.preimage_eq', h]
Proof state after:
no goals
Theorem: Super.potential_eq_zero_of_onePreimage
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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ s.potential c z = 0 ↔ z = a
Tactic:
constructor
Proof state after:
case mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ s.potential c z = 0 → z = a

case mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ z = a → s.potential c z = 0
Theorem: Super.potential_eq_zero_of_onePreimage
Proof state before:
case mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ s.potential c z = 0 → z = a
Tactic:
intro h
Proof state after:
case mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : s.potential c z = 0
⊢ z = a
Theorem: Super.potential_eq_zero_of_onePreimage
Proof state before:
case mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : s.potential c z = 0
⊢ z = a
Tactic:
rw [s.potential_eq_zero] at h
Proof state after:
case mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : ∃ n, (f c)^[n] z = a
⊢ z = a
Theorem: Super.potential_eq_zero_of_onePreimage
Proof state before:
case mp
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : ∃ n, (f c)^[n] z = a
⊢ z = a
Tactic:
rcases h with ⟨n, h⟩
Proof state after:
case mp.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : (f c)^[n] z = a
⊢ z = a
Theorem: Super.potential_eq_zero_of_onePreimage
Proof state before:
case mp.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : (f c)^[n] z = a
⊢ z = a
Tactic:
rw [s.preimage_eq] at h
Proof state after:
case mp.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : z = a
⊢ z = a
Theorem: Super.potential_eq_zero_of_onePreimage
Proof state before:
case mp.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : ℕ
h : z = a
⊢ z = a
Tactic:
exact h
Proof state after:
no goals
Theorem: Super.potential_eq_zero_of_onePreimage
Proof state before:
case mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ z = a → s.potential c z = 0
Tactic:
intro h
Proof state after:
case mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : z = a
⊢ s.potential c z = 0
Theorem: Super.potential_eq_zero_of_onePreimage
Proof state before:
case mpr
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
h : z = a
⊢ s.potential c z = 0
Tactic:
simp only [h, s.potential_a]
Proof state after:
no goals
Theorem: Super.potential_ne_zero
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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ s.potential c z ≠ 0 ↔ z ≠ a
Tactic:
simp only [Ne, s.potential_eq_zero_of_onePreimage]
Proof state after:
no goals
Theorem: Super.potential_pos
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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.potential c z ↔ z ≠ a
Tactic:
rw [← s.potential_ne_zero 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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.potential c z ↔ s.potential c z ≠ 0
Theorem: Super.potential_pos
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✝ : ℂ
a z : S
d n : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.potential c z ↔ s.potential c z ≠ 0
Tactic:
use ne_of_gt, fun ne ↦ ne.symm.lt_of_le s.potential_nonneg
Proof state after:
no goals
Theorem: Super.no_jump
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
Tactic:
have h : ∀ q : ℂ × S, f q.1 q.2 = a → q.2 = a := fun _ ↦ by simp only [s.preimage_eq', imp_self]
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
Theorem: Super.no_jump
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
Tactic:
contrapose h
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ¬∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Theorem: Super.no_jump
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ¬∀ᶠ (p : ℂ × S) in 𝓝 (c, a), ∀ (q : ℂ × S), p = s.fp q → q ∈ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
simp only [Filter.not_eventually, not_forall, exists_prop] at h
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Theorem: Super.no_jump
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
set t := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Theorem: Super.no_jump
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
have tc : IsClosed t := by
  refine (IsCompact.image ?_ s.fpa.continuous).isClosed
  exact ((isCompact_closedBall _ _).prod isCompact_univ).inter_right no.isClosed_compl
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Theorem: Super.no_jump
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
have th : ∃ᶠ p in 𝓝 (c, a), p ∈ t := by
  have mb : ∀ᶠ p : ℂ × S in 𝓝 (c, a), p.1 ∈ closedBall c 1 :=
    continuousAt_fst.eventually_mem_nhd (Metric.closedBall_mem_nhds _ zero_lt_one)
  refine (h.and_eventually mb).mp (eventually_of_forall fun p i ↦ ?_)
  rcases i with ⟨⟨q, qp, m⟩, b⟩
  simp only [Prod.ext_iff] at qp; simp only [qp.1] at b
  simp only [Set.mem_image, Set.mem_compl_iff, Set.mem_inter_iff, Set.mem_prod_eq, Set.mem_univ,
    and_true_iff, Prod.ext_iff, t]
  use q, ⟨b, m⟩, qp.1.symm, qp.2.symm
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Theorem: Super.no_jump
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a
Tactic:
have m := th.mem_of_closed tc
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✝ : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
n : Set (ℂ × S)
no : IsOpen n
na : (c, a) ∈ n
h : ∃ᶠ (x : ℂ × S) in 𝓝 (c, a), ∃ x_1, x = s.fp x_1 ∧ x_1 ∉ n
t : Set (ℂ × S) := s.fp '' (closedBall c 1 ×ˢ univ ∩ nᶜ)
tc : IsClosed t
th : ∃ᶠ (p : ℂ × S) in 𝓝 (c, a), p ∈ t
m : (c, a) ∈ t
⊢ ¬∀ (q : ℂ × S), f q.1 q.2 = a → q.2 = a