internlm/Lean-Github huggingface dataset:
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0✝ z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ closedBall c0 re ∧ z0 ∈ {a | ∀ z1 ∈ closedBall c1 r, ‖f (a, z1)‖ ≤ ↑b}
⊢ z0 ∈ closedBall c0 re
Tactic:
exact z0b.left
Proof state after:
no goals
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
⊢ ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
Tactic:
intro z zs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z ∈ ball c0' t ×ˢ ball c1 r
⊢ ‖f z‖ ≤ ↑b
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z ∈ ball c0' t ×ˢ ball c1 r
⊢ ‖f z‖ ≤ ↑b
Tactic:
rw [Set.mem_prod] at zs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
⊢ ‖f z‖ ≤ ↑b
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
⊢ ‖f z‖ ≤ ↑b
Tactic:
have zb := _root_.trans ts s's zs.left
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ S b
⊢ ‖f z‖ ≤ ↑b
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ S b
⊢ ‖f z‖ ≤ ↑b
Tactic:
rw [← hS] at zb
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ ‖f z‖ ≤ ↑b
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ ‖f z‖ ≤ ↑b
Tactic:
simp only [Metric.mem_ball, Metric.mem_closedBall, le_min_iff, Set.mem_setOf_eq] at zb zs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
⊢ ‖f z‖ ≤ ↑b
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
⊢ ‖f z‖ ≤ ↑b
Tactic:
have zb' := zb.right z.snd zs.right.le
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f (z.1, z.2)‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f (z.1, z.2)‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b
Tactic:
simp only [Prod.mk.eta] at zb'
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f z‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b
Theorem: on_subdisk
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f z‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b
Tactic:
exact zb'
Proof state after:
no goals
Theorem: diam_ball_eq
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
by_cases r0 : 0 = r
Proof state after:
case pos
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : 0 = r
⊢ Metric.diam (ball c r) = 2 * r

case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
⊢ Metric.diam (ball c r) = 2 * r
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
have rp' := Ne.lt_of_le r0 rp
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
clear r0
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
apply le_antisymm (Metric.diam_ball rp)
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ 2 * r ≤ Metric.diam (ball c r)
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ 2 * r ≤ Metric.diam (ball c r)
Tactic:
apply le_of_forall_small_le_add rp'
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ ∀ (e : ℝ), 0 < e → e < r → 2 * r ≤ Metric.diam (ball c r) + e
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ ∀ (e : ℝ), 0 < e → e < r → 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
intro e ep er
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
have m : ∀ t : ℝ, |t| ≤ 1 → c + t * (r - e / 2) ∈ ball c r := by
  intro t t1
  simp only [Complex.dist_eq, Metric.mem_ball, add_sub_cancel_left, AbsoluteValue.map_mul,
    Complex.abs_ofReal]
  have re : r - e / 2 ≥ 0 := by linarith [_root_.trans (half_lt_self ep) er]
  calc |t| * abs (↑r - ↑e / 2 : ℂ)
    _ = |t| * abs (↑(r - e / 2) : ℂ) := by
      simp only [Complex.ofReal_sub, Complex.ofReal_div, Complex.ofReal_one]
      norm_num
    _ = |t| * (r - e / 2) := by rw [Complex.abs_ofReal, abs_of_nonneg re]
    _ ≤ 1 * (r - e / 2) := mul_le_mul_of_nonneg_right t1 re
    _ = r - e / 2 := by ring
    _ < r - 0 := (sub_lt_sub_left (by linarith) r)
    _ = r := by ring
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
have lo :=
  Metric.dist_le_diam_of_mem Metric.isBounded_ball (m 1 (by norm_num)) (m (-1) (by norm_num))
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
have e : abs (2 * ↑r - ↑e : ℂ) = 2 * r - e := by
  have re : 2 * r - e ≥ 0 := by trans r - e; linarith; simp only [sub_nonneg, er.le]
  calc abs (2 * ↑r - ↑e : ℂ)
    _ = abs (↑(2 * r - e) : ℂ) := by
      simp only [Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_one]
      norm_num
    _ = 2 * r - e := by rw [Complex.abs_ofReal, abs_of_nonneg re]
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e✝ / 2)) (c + ↑(-1) * (↑r - ↑e✝ / 2)) ≤ Metric.diam (ball c r)
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e✝ / 2)) (c + ↑(-1) * (↑r - ↑e✝ / 2)) ≤ Metric.diam (ball c r)
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Tactic:
simp only [Complex.dist_eq, Complex.ofReal_one, one_mul, Complex.ofReal_neg, neg_mul, neg_sub,
  add_sub_add_left_eq_sub] at lo
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : Complex.abs (↑r - ↑e✝ / 2 - (↑e✝ / 2 - ↑r)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Theorem: diam_ball_eq
Proof state before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : Complex.abs (↑r - ↑e✝ / 2 - (↑e✝ / 2 - ↑r)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Tactic:
ring_nf at lo
Proof state after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : Complex.abs (↑r * 2 - ↑e✝) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝