internlm/Lean-Github huggingface dataset:
Theorem: SuperAtC.superNearC'
Proof state before:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ AnalyticOn ℂ (f c') (ball 0 r)
Tactic:
apply fa.comp₂ analyticOn_const (analyticOn_id _)
Proof state after:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ ∀ x ∈ ball 0 r, (c', x) ∈ ball (c, 0) (min r0 r1)
Theorem: SuperAtC.superNearC'
Proof state before:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ ∀ x ∈ ball 0 r, (c', x) ∈ ball (c, 0) (min r0 r1)
Tactic:
intro z zm
Proof state after:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) (min r0 r1)
Theorem: SuperAtC.superNearC'
Proof state before:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) (min r0 r1)
Tactic:
apply Metric.ball_subset_ball (by bound : r ≤ r2)
Proof state after:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) r
Theorem: SuperAtC.superNearC'
Proof state before:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) r
Tactic:
simp only [← ball_prod_same, Set.mem_prod, m, true_and_iff]
Proof state after:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ z ∈ ball 0 r
Theorem: SuperAtC.superNearC'
Proof state before:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ z ∈ ball 0 r
Tactic:
exact zm
Proof state after:
no goals
Theorem: SuperAtC.superNearC'
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ r ≤ r2
Tactic:
bound
Proof state after:
no goals
Theorem: SuperAtC.superNearC'
Proof state before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
simp only [Complex.dist_eq, Prod.dist_eq, sub_zero, max_lt_iff, and_imp, g2, g0] at gs
Proof state after:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Theorem: SuperAtC.superNearC'
Proof state before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq] at m
Proof state after:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Theorem: SuperAtC.superNearC'
Proof state before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
intro z zr
Proof state after:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
z : ℂ
zr : Complex.abs z < r
⊢ Complex.abs (g (f c') d z - 1) < 1 / 4
Theorem: SuperAtC.superNearC'
Proof state before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
z : ℂ
zr : Complex.abs z < r
⊢ Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
exact @gs ⟨c', z⟩ (lt_of_lt_of_le m rr4) (lt_of_lt_of_le zr rr4)
Proof state after:
no goals
Theorem: SuperAtC.superNearC'
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ u = ⋃ c, v c
Tactic:
apply Set.ext
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ ∀ (x : ℂ), x ∈ u ↔ x ∈ ⋃ c, v c
Theorem: SuperAtC.superNearC'
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ ∀ (x : ℂ), x ∈ u ↔ x ∈ ⋃ c, v c
Tactic:
intro c
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ c ∈ ⋃ c, v c
Theorem: SuperAtC.superNearC'
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ c ∈ ⋃ c, v c
Tactic:
rw [Set.mem_iUnion]
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ ∃ i, c ∈ v i
Theorem: SuperAtC.superNearC'
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ ∃ i, c ∈ v i
Tactic:
constructor
Proof state after:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u → ∃ i, c ∈ v i

case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ (∃ i, c ∈ v i) → c ∈ u
Theorem: SuperAtC.superNearC'
Proof state before:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u → ∃ i, c ∈ v i
Tactic:
intro m
Proof state after:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ ∃ i, c ∈ v i
Theorem: SuperAtC.superNearC'
Proof state before:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ ∃ i, c ∈ v i
Tactic:
use⟨c, m⟩
Proof state after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ c ∈ v ⟨c, m⟩
Theorem: SuperAtC.superNearC'
Proof state before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ c ∈ v ⟨c, m⟩
Tactic:
rcases choose_spec (h c m) with ⟨rp, _, _⟩
Proof state after:
case h.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
rp : choose ⋯ > 0
left✝ : ball c (choose ⋯) ⊆ u
right✝ : ball (c, 0) (choose ⋯) ⊆ w ∧ SuperNearC f d (ball c (choose ⋯)) (ball (c, 0) (choose ⋯))
⊢ c ∈ v ⟨c, m⟩
Theorem: SuperAtC.superNearC'
Proof state before:
case h.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
rp : choose ⋯ > 0
left✝ : ball c (choose ⋯) ⊆ u
right✝ : ball (c, 0) (choose ⋯) ⊆ w ∧ SuperNearC f d (ball c (choose ⋯)) (ball (c, 0) (choose ⋯))
⊢ c ∈ v ⟨c, m⟩
Tactic:
exact mem_ball_self rp
Proof state after:
no goals
Theorem: SuperAtC.superNearC'
Proof state before:
case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ (∃ i, c ∈ v i) → c ∈ u
Tactic:
intro m
Proof state after:
case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : ∃ i, c ∈ v i
⊢ c ∈ u
Theorem: SuperAtC.superNearC'
Proof state before:
case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : ∃ i, c ∈ v i
⊢ c ∈ u
Tactic:
rcases m with ⟨i, m⟩
Proof state after:
case h.mpr.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
i : ↑u
m : c ∈ v i
⊢ c ∈ u
Theorem: SuperAtC.superNearC'
Proof state before:
case h.mpr.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
i : ↑u
m : c ∈ v i
⊢ c ∈ u
Tactic:
rcases choose_spec (h _ i.mem) with ⟨_, us, _⟩
Proof state after:
case h.mpr.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
i : ↑u
m : c ∈ v i
left✝ : choose ⋯ > 0
us : ball (↑i) (choose ⋯) ⊆ u
right✝ : ball (↑i, 0) (choose ⋯) ⊆ w ∧ SuperNearC f d (ball (↑i) (choose ⋯)) (ball (↑i, 0) (choose ⋯))
⊢ c ∈ u