internlm/Lean-Github huggingface dataset:
Theorem: eqn_near
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✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), (y.1, (f y.1)^[n] (r y.1 y.2)) ∈ s.near
Tactic:
refine ContinuousAt.eventually_mem ?_ (s.isOpen_near.mem_nhds mem)
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✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ContinuousAt (fun y => (y.1, (f y.1)^[n] (r y.1 y.2))) (c, x)
Theorem: eqn_near
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✝ : ℕ
p : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
n : ℕ
r : ℂ → ℂ → S
c x : ℂ
holo : HolomorphicAt (I.prod I) I (uncurry r) (c, x)
mem : (c, (f c)^[n] (r c x)) ∈ s.near
loc : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), s.bottcherNear y.1 ((f y.1)^[n] (r y.1 y.2)) = y.2 ^ d ^ n
⊢ ContinuousAt (fun y => (y.1, (f y.1)^[n] (r y.1 y.2))) (c, x)
Tactic:
exact continuousAt_fst.prod (s.continuousAt_iter continuousAt_fst holo.continuousAt)
Proof state after:
no goals
Theorem: Eqn.congr
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
⊢ Eqn s n r1 x
Tactic:
have s := loc.self_of_nhds
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : uncurry r0 x = uncurry r1 x
⊢ Eqn s✝ n r1 x
Theorem: Eqn.congr
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : uncurry r0 x = uncurry r1 x
⊢ Eqn s✝ n r1 x
Tactic:
simp only [uncurry] at s
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ Eqn s✝ n r1 x
Theorem: Eqn.congr
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ Eqn s✝ n r1 x
Tactic:
exact
  { holo := e.holo.congr loc
    near := by simp only [← s, e.near]
    eqn := by simp only [← s, e.eqn] }
Proof state after:
no goals
Theorem: Eqn.congr
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ (x.1, (f x.1)^[n] (r1 x.1 x.2)) ∈ s✝.near
Tactic:
simp only [← s, e.near]
Proof state after:
no goals
Theorem: Eqn.congr
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ s✝.bottcherNear x.1 ((f x.1)^[n] (r1 x.1 x.2)) = x.2 ^ d ^ n
Tactic:
simp only [← s, e.eqn]
Proof state after:
no goals
Theorem: Eqn.mono
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
⊢ s.bottcherNear x.1 ((f x.1)^[m] (r x.1 x.2)) = x.2 ^ d ^ m
Tactic:
refine Nat.le_induction e.eqn ?_ m nm
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
⊢ ∀ (n_1 : ℕ),
    n ≤ n_1 →
      s.bottcherNear x.1 ((f x.1)^[n_1] (r x.1 x.2)) = x.2 ^ d ^ n_1 →
        s.bottcherNear x.1 ((f x.1)^[n_1 + 1] (r x.1 x.2)) = x.2 ^ d ^ (n_1 + 1)
Theorem: Eqn.mono
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
⊢ ∀ (n_1 : ℕ),
    n ≤ n_1 →
      s.bottcherNear x.1 ((f x.1)^[n_1] (r x.1 x.2)) = x.2 ^ d ^ n_1 →
        s.bottcherNear x.1 ((f x.1)^[n_1 + 1] (r x.1 x.2)) = x.2 ^ d ^ (n_1 + 1)
Tactic:
intro k nk 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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
k : ℕ
nk : n ≤ k
h : s.bottcherNear x.1 ((f x.1)^[k] (r x.1 x.2)) = x.2 ^ d ^ k
⊢ s.bottcherNear x.1 ((f x.1)^[k + 1] (r x.1 x.2)) = x.2 ^ d ^ (k + 1)
Theorem: Eqn.mono
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
k : ℕ
nk : n ≤ k
h : s.bottcherNear x.1 ((f x.1)^[k] (r x.1 x.2)) = x.2 ^ d ^ k
⊢ s.bottcherNear x.1 ((f x.1)^[k + 1] (r x.1 x.2)) = x.2 ^ d ^ (k + 1)
Tactic:
simp only [h, Function.iterate_succ_apply',
  s.bottcherNear_eqn (s.iter_stays_near' e.near nk), pow_succ, pow_mul]
Proof state after:
no goals
Theorem: mem_domain_self
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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
⊢ (c, x) ∈ {c} ×ˢ closedBall 0 (Complex.abs x)
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, mem_closedBall, Complex.dist_eq,
  sub_zero, true_and_iff, le_refl]
Proof state after:
no goals
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
set u := Complex.abs '' (closedBall 0 (p + 1) \ t)
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
by_cases ne : u = ∅
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u = ∅
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t

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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : ¬u = ∅
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : ¬u = ∅
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
replace ne := nonempty_iff_ne_empty.mpr ne
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
have uc : IsClosed u :=
  (((isCompact_closedBall _ _).diff ot).image Complex.continuous_abs).isClosed
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
have up : ∀ x : ℝ, x ∈ u → p < x := by
  intro x m; rcases m with ⟨z, ⟨_, mt⟩, e⟩; rw [← e]; contrapose mt
  simp only [not_not, not_lt] at mt ⊢
  apply sub; simp only [mem_closedBall, Complex.dist_eq, sub_zero, mt]
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
have ub : BddBelow u := ⟨p, fun _ m ↦ (up _ m).le⟩
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
have iu : sInf u ∈ u := IsClosed.csInf_mem uc ne ub
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
rcases exists_between (up _ iu) with ⟨q, pq, qi⟩
Proof state after:
case neg.intro.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Theorem: domain_open'
Proof state before:
case neg.intro.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
use min q (p + 1), lt_min pq (by linarith)
Proof state after:
case right
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
⊢ closedBall 0 (min q (p + 1)) ⊆ t
Theorem: domain_open'
Proof state before:
case right
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
⊢ closedBall 0 (min q (p + 1)) ⊆ t
Tactic:
intro z m
Proof state after:
case right
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
m : z ∈ closedBall 0 (min q (p + 1))
⊢ z ∈ t
Theorem: domain_open'
Proof state before:
case right
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
m : z ∈ closedBall 0 (min q (p + 1))
⊢ z ∈ t
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, le_min_iff] at m
Proof state after:
case right
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
m : Complex.abs z ≤ q ∧ Complex.abs z ≤ p + 1
⊢ z ∈ t
Theorem: domain_open'
Proof state before:
case right
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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
m : Complex.abs z ≤ q ∧ Complex.abs z ≤ p + 1
⊢ z ∈ t
Tactic:
rcases m with ⟨zq, zp⟩
Proof state after:
case right.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
zq : Complex.abs z ≤ q
zp : Complex.abs z ≤ p + 1
⊢ z ∈ t
Theorem: domain_open'
Proof state before:
case right.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
zq : Complex.abs z ≤ q
zp : Complex.abs z ≤ p + 1
⊢ z ∈ t
Tactic:
have zi := lt_of_le_of_lt zq qi
Proof state after:
case right.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
zq : Complex.abs z ≤ q
zp : Complex.abs z ≤ p + 1
zi : Complex.abs z < sInf u
⊢ z ∈ t
Theorem: domain_open'
Proof state before:
case right.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
zq : Complex.abs z ≤ q
zp : Complex.abs z ≤ p + 1
zi : Complex.abs z < sInf u
⊢ z ∈ t
Tactic:
contrapose zi
Proof state after:
case right.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
zq : Complex.abs z ≤ q
zp : Complex.abs z ≤ p + 1
zi : ¬z ∈ t
⊢ ¬Complex.abs z < sInf u
Theorem: domain_open'
Proof state before:
case right.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
zq : Complex.abs z ≤ q
zp : Complex.abs z ≤ p + 1
zi : ¬z ∈ t
⊢ ¬Complex.abs z < sInf u
Tactic:
simp only [not_lt]
Proof state after:
case right.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 : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set ℂ
sub : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
up : ∀ x ∈ u, p < x
ub : BddBelow u
iu : sInf u ∈ u
q : ℝ
pq : p < q
qi : q < sInf u
z : ℂ
zq : Complex.abs z ≤ q
zp : Complex.abs z ≤ p + 1
zi : ¬z ∈ t
⊢ sInf u ≤ Complex.abs z