internlm/Lean-Github huggingface dataset:
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
⊢ sInf u ≤ Complex.abs z
Tactic:
refine csInf_le ub (mem_image_of_mem _ ?_)
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
⊢ z ∈ closedBall 0 (p + 1) \ 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 : ¬z ∈ t
⊢ z ∈ closedBall 0 (p + 1) \ t
Tactic:
simp only [mem_diff, mem_closedBall, Complex.dist_eq, sub_zero]
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 ≤ 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
zi : ¬z ∈ t
⊢ Complex.abs z ≤ p + 1 ∧ z ∉ t
Tactic:
use zp, zi
Proof state after:
no goals
Theorem: domain_open'
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 : ℕ
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:
refine ⟨p + 1, by bound, ?_⟩
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 = ∅
⊢ closedBall 0 (p + 1) ⊆ t
Theorem: domain_open'
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 : ℕ
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 = ∅
⊢ closedBall 0 (p + 1) ⊆ t
Tactic:
rw [image_eq_empty, diff_eq_empty] at ne
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 : closedBall 0 (p + 1) ⊆ t
⊢ closedBall 0 (p + 1) ⊆ t
Theorem: domain_open'
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 : ℕ
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 : closedBall 0 (p + 1) ⊆ t
⊢ closedBall 0 (p + 1) ⊆ t
Tactic:
exact ne
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
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u = ∅
⊢ p < p + 1
Tactic:
bound
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
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u.Nonempty
uc : IsClosed u
⊢ ∀ x ∈ u, p < x
Tactic:
intro 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 : ℂ
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
x : ℝ
m : x ∈ u
⊢ p < x
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)
ne : u.Nonempty
uc : IsClosed u
x : ℝ
m : x ∈ u
⊢ p < x
Tactic:
rcases m with ⟨z, ⟨_, mt⟩, e⟩
Proof state after:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : z ∉ t
⊢ p < x
Theorem: domain_open'
Proof state before:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : z ∉ t
⊢ p < x
Tactic:
rw [← e]
Proof state after:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : z ∉ t
⊢ p < Complex.abs z
Theorem: domain_open'
Proof state before:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : z ∉ t
⊢ p < Complex.abs z
Tactic:
contrapose mt
Proof state after:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : ¬p < Complex.abs z
⊢ ¬z ∉ t
Theorem: domain_open'
Proof state before:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : ¬p < Complex.abs z
⊢ ¬z ∉ t
Tactic:
simp only [not_not, not_lt] at mt ⊢
Proof state after:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : Complex.abs z ≤ p
⊢ z ∈ t
Theorem: domain_open'
Proof state before:
case intro.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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : Complex.abs z ≤ p
⊢ z ∈ t
Tactic:
apply sub
Proof state after:
case intro.intro.intro.a
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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : Complex.abs z ≤ p
⊢ z ∈ closedBall 0 p
Theorem: domain_open'
Proof state before:
case intro.intro.intro.a
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
x : ℝ
z : ℂ
e : Complex.abs z = x
left✝ : z ∈ closedBall 0 (p + 1)
mt : Complex.abs z ≤ p
⊢ z ∈ closedBall 0 p
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, mt]
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
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
⊢ p < p + 1
Tactic:
linarith
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 : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
⊢ ∃ q, p < q ∧ {c} ×ˢ closedBall 0 q ⊆ t
Tactic:
have sub : closedBall 0 p ⊆ {b | (c, b) ∈ t} := by
  intro z m; simp only [mem_setOf]; apply sub; exact ⟨mem_singleton _, 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 : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set (ℂ × ℂ)
sub✝ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub : closedBall 0 p ⊆ {b | (c, b) ∈ t}
⊢ ∃ q, p < q ∧ {c} ×ˢ 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✝ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub : closedBall 0 p ⊆ {b | (c, b) ∈ t}
⊢ ∃ q, p < q ∧ {c} ×ˢ closedBall 0 q ⊆ t
Tactic:
rcases domain_open' sub (o.snd_preimage c) with ⟨q, pq, sub⟩
Proof state after:
case 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
⊢ ∃ q, p < q ∧ {c} ×ˢ closedBall 0 q ⊆ t
Theorem: domain_open
Proof state before:
case 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
⊢ ∃ q, p < q ∧ {c} ×ˢ closedBall 0 q ⊆ t
Tactic:
use q, pq
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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
⊢ {c} ×ˢ closedBall 0 q ⊆ 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
⊢ {c} ×ˢ closedBall 0 q ⊆ t
Tactic:
intro ⟨e, z⟩ ⟨ec, 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
ec : (e, z).1 ∈ {c}
m : (e, z).2 ∈ closedBall 0 q
⊢ (e, 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
ec : (e, z).1 ∈ {c}
m : (e, z).2 ∈ closedBall 0 q
⊢ (e, z) ∈ t
Tactic:
simp only [mem_singleton_iff] at ec
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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
m : (e, z).2 ∈ closedBall 0 q
ec : e = c
⊢ (e, 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
m : (e, z).2 ∈ closedBall 0 q
ec : e = c
⊢ (e, z) ∈ t
Tactic:
replace m := sub 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
ec : e = c
m : (e, z).2 ∈ {b | (c, b) ∈ t}
⊢ (e, 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
ec : e = c
m : (e, z).2 ∈ {b | (c, b) ∈ t}
⊢ (e, z) ∈ t
Tactic:
simp only [← ec, mem_setOf] 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
ec : e = c
m : (e, z) ∈ t
⊢ (e, 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✝¹ : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
sub✝ : closedBall 0 p ⊆ {b | (c, b) ∈ t}
q : ℝ
pq : p < q
sub : closedBall 0 q ⊆ {b | (c, b) ∈ t}
e z : ℂ
ec : e = c
m : (e, z) ∈ t
⊢ (e, z) ∈ t
Tactic:
exact m
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 : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
⊢ closedBall 0 p ⊆ {b | (c, b) ∈ t}
Tactic:
intro z 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 : ℂ
a z✝ : S
d n : ℕ
p✝ : ℝ
s : Super f d a
r : ℂ → ℂ → S
p : ℝ
t : Set (ℂ × ℂ)
sub : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
z : ℂ
m : z ∈ closedBall 0 p
⊢ z ∈ {b | (c, b) ∈ 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 : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
z : ℂ
m : z ∈ closedBall 0 p
⊢ z ∈ {b | (c, b) ∈ t}
Tactic:
simp only [mem_setOf]
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 : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
z : ℂ
m : z ∈ closedBall 0 p
⊢ (c, z) ∈ 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 : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
z : ℂ
m : z ∈ closedBall 0 p
⊢ (c, z) ∈ t
Tactic:
apply sub
Proof state after:
case a
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 : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
z : ℂ
m : z ∈ closedBall 0 p
⊢ (c, z) ∈ {c} ×ˢ closedBall 0 p
Theorem: domain_open
Proof state before:
case a
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 : {c} ×ˢ closedBall 0 p ⊆ t
o : IsOpen t
z : ℂ
m : z ∈ closedBall 0 p
⊢ (c, z) ∈ {c} ×ˢ closedBall 0 p
Tactic:
exact ⟨mem_singleton _, m⟩
Proof state after:
no goals
Theorem: Grow.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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
⊢ r1 c 0 = a
Tactic:
have e := e.self_of_nhdsSet (mem_domain c g.nonneg)
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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : uncurry r0 (c, 0) = uncurry r1 (c, 0)
⊢ r1 c 0 = a
Theorem: Grow.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 r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : uncurry r0 (c, 0) = uncurry r1 (c, 0)
⊢ r1 c 0 = a
Tactic:
simp only [uncurry] at 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 : ℕ
p : ℝ
s : Super f d a
r r0 r1 : ℂ → ℂ → S
g : Grow s c p n r0
e✝ : (𝓝ˢ ({c} ×ˢ closedBall 0 p)).EventuallyEq (uncurry r0) (uncurry r1)
e : r0 c 0 = r1 c 0
⊢ r1 c 0 = a