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 : closedBall 0 p ⊆ t
ot : IsOpen t
⊢ ∃ q, p < q ∧ closedBall 0 q ⊆ t
Tactic:
set u := Complex.abs '' (closedBall 0 (p + 1) \ t)
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 _ ?_)
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

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

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

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, ?_⟩
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

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

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
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 : closedBall 0 p ⊆ t
ot : IsOpen t
u : Set ℝ := ⇑Complex.abs '' (closedBall 0 (p + 1) \ t)
ne : u = ∅
⊢ p < p + 1
Tactic:
bound
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 : 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
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

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

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

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

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

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

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