internlm/Lean-Github huggingface dataset:
Theorem: ContinuousOn.circleIntegral
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
Tactic:
apply funext
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ∀ (x : ℂ), f x (circleMap c1 r t) = (uncurry f ∘ fun x => (x, circleMap c1 r t)) x
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
⊢ ∀ (x : ℂ), f x (circleMap c1 r t) = (uncurry f ∘ fun x => (x, circleMap c1 r t)) x
Tactic:
intro t
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
t✝ : ℝ
a✝ : t✝ ∈ Ι 0 (2 * π)
t : ℂ
⊢ f t (circleMap c1 r t✝) = (uncurry f ∘ fun x => (x, circleMap c1 r t✝)) t
Theorem: ContinuousOn.circleIntegral
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
t✝ : ℝ
a✝ : t✝ ∈ Ι 0 (2 * π)
t : ℂ
⊢ f t (circleMap c1 r t✝) = (uncurry f ∘ fun x => (x, circleMap c1 r t✝)) t
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousOn.circleIntegral
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
t : ℝ
a✝ : t ∈ Ι 0 (2 * π)
comp : (fun x => f x (circleMap c1 r t)) = uncurry f ∘ fun x => (x, circleMap c1 r t)
x : ℂ
xs : x ∈ s
⊢ 0 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
⊢ ContinuousOn (fun z => (z - (c + w))⁻¹) (sphere c r)
Tactic:
refine ContinuousOn.inv₀ (ContinuousOn.sub continuousOn_id continuousOn_const) fun z zs ↦ ?_
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ z - (c + w) ≠ 0
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ z - (c + w) ≠ 0
Tactic:
rw [←Complex.abs.ne_zero_iff]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ Complex.abs (z - (c + w)) ≠ 0
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ Complex.abs (z - (c + w)) ≠ 0
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs, mem_sphere_iff_norm] at zs wr
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - (c + w)) ≠ 0
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - (c + w)) ≠ 0
Tactic:
apply ne_of_gt
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ 0 < Complex.abs (z - (c + w))
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ 0 < Complex.abs (z - (c + w))
Tactic:
calc abs (z - (c + w))
  _ = abs (z - c + -w) := by ring_nf
  _ ≥ abs (z - c) - abs (-w) := by bound
  _ = r - abs (-w) := by rw [zs]
  _ = r - abs w := by rw [Complex.abs.map_neg]
  _ > r - r := (sub_lt_sub_left wr _)
  _ = 0 := by ring
Proof state after:
no goals
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - (c + w)) = Complex.abs (z - c + -w)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - c + -w) ≥ Complex.abs (z - c) - Complex.abs (-w)
Tactic:
bound
Proof state after:
no goals
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - c) - Complex.abs (-w) = r - Complex.abs (-w)
Tactic:
rw [zs]
Proof state after:
no goals
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ r - Complex.abs (-w) = r - Complex.abs w
Tactic:
rw [Complex.abs.map_neg]
Proof state after:
no goals
Theorem: ContinuousOn.inv_sphere_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ r - r = 0
Tactic:
ring
Proof state after:
no goals
Theorem: ContinuousOn.cauchy1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun z0 => ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)) (sphere c0 r)
Tactic:
apply ContinuousOn.circleIntegral rp (isCompact_sphere _ _)
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (uncurry fun z0 z1 => (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (uncurry fun z0 z1 => (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.smul
Proof state after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ ^ n1) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ ^ n1) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.pow
Proof state after:
case hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.inv₀
Proof state after:
case hf.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hf.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply Continuous.continuousOn
Proof state after:
case hf.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hf.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact Continuous.sub (Continuous.snd continuous_id) continuous_const
Proof state after:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
intro x xp
Proof state after:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact center_not_in_sphere rp (Set.mem_prod.mp xp).right
Proof state after:
case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.smul
Proof state after:
case hg.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.inv₀
Proof state after:
case hg.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Theorem: ContinuousOn.cauchy1
Proof state before:
case hg.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply Continuous.continuousOn
Proof state after:
case hg.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)