Theorem: domain_open (Ray/Dynamics/Grow.lean)

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⟩
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

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⟩
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

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
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

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⟩
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

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
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

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
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

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
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

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
State after:
no goals

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
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}

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]
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

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
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

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⟩
State after:
no goals