internlm/Lean-Github huggingface dataset:
Theorem: SuperAtC.superNearC'
Proof state before:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rh : r ≤ 1 / 2 := le_trans (min_le_right _ _) (min_le_right _ _)
Proof state after:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Theorem: SuperAtC.superNearC'
Proof state before:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rr4 : r ≤ r4 := le_trans (min_le_right _ _) (min_le_left r4 _)
Proof state after:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Theorem: SuperAtC.superNearC'
Proof state before:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rc : ball c r ⊆ u := le_trans (Metric.ball_subset_ball (by bound)) rc
Proof state after:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Theorem: SuperAtC.superNearC'
Proof state before:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rw : ball (c, 0) r ⊆ w :=
  _root_.trans (Metric.ball_subset_ball (le_trans (min_le_left _ _) (min_le_right _ _))) rw
Proof state after:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Theorem: SuperAtC.superNearC'
Proof state before:
case intro.intro.intro.intro.intro.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
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
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
use r, rp, rc, rw
Proof state after:
case right
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
⊢ SuperNearC f d (ball c r) (ball (c, 0) r)
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))
⊢ r2 ≤ r1
Tactic:
bound
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
⊢ ∀ {p : ℂ × ℂ}, p ∈ ball (c, 0) (min r0 r1) → p.1 ∈ u
Tactic:
intro p m
Proof state after:
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
p : ℂ × ℂ
m : p ∈ ball (c, 0) (min r0 r1)
⊢ p.1 ∈ u
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
p : ℂ × ℂ
m : p ∈ ball (c, 0) (min r0 r1)
⊢ p.1 ∈ u
Tactic:
simp only [← ball_prod_same, Set.mem_prod] at m
Proof state after:
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
p : ℂ × ℂ
m : p.1 ∈ ball c (min r0 r1) ∧ p.2 ∈ ball 0 (min r0 r1)
⊢ p.1 ∈ u
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
p : ℂ × ℂ
m : p.1 ∈ ball c (min r0 r1) ∧ p.2 ∈ ball 0 (min r0 r1)
⊢ p.1 ∈ u
Tactic:
exact rc m.1
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
⊢ 0 < min r0 r1
Tactic:
bound
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
⊢ 1 / 4 > 0
Tactic:
norm_num
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))
⊢ 0 < r
Tactic:
bound
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
⊢ r ≤ r2
Tactic:
bound
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
⊢ ∀ {p : ℂ × ℂ}, p ∈ ball (c, 0) r → p.1 ∈ ball c r
Tactic:
intro p m
Proof state after:
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
p : ℂ × ℂ
m : p ∈ ball (c, 0) r
⊢ p.1 ∈ ball c r
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
p : ℂ × ℂ
m : p ∈ ball (c, 0) r
⊢ p.1 ∈ ball c r
Tactic:
simp only [← ball_prod_same, Set.mem_prod] at m
Proof state after:
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
p : ℂ × ℂ
m : p.1 ∈ ball c r ∧ p.2 ∈ ball 0 r
⊢ p.1 ∈ ball c r
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
p : ℂ × ℂ
m : p.1 ∈ ball c r ∧ p.2 ∈ ball 0 r
⊢ p.1 ∈ ball c r
Tactic:
exact Metric.ball_subset_ball (by linarith) m.1
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
p : ℂ × ℂ
m : p.1 ∈ ball c r ∧ p.2 ∈ ball 0 r
⊢ r ≤ r
Tactic:
linarith
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_1 : ℂ}, c_1 ∈ ball c r → SuperNear (f c_1) d {z | (c_1, z) ∈ ball (c, 0) r}
Tactic:
intro c' m
Proof state after:
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
⊢ SuperNear (f c') d {z | (c', z) ∈ ball (c, 0) r}
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
⊢ SuperNear (f c') d {z | (c', z) ∈ ball (c, 0) r}
Tactic:
simp only [← ball_prod_same, Set.mem_prod, m, true_and_iff]
Proof state after:
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
⊢ SuperNear (f c') d {z | z ∈ ball 0 r}
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
⊢ SuperNear (f c') d {z | z ∈ ball 0 r}
Tactic:
apply (s.s (rc m)).super_on_ball rp rh
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
⊢ AnalyticOn ℂ (f c') (ball 0 r)

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