internlm/Lean-Github huggingface dataset:
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - circleIntegral g c r = circleIntegral (f - g) c r
Tactic:
rw [circleIntegral]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ) =
    circleIntegral (f - g) c r
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
⊢ intervalIntegral fc 0 (2 * π) volume - ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • g (circleMap c r θ) =
    circleIntegral (f - g) c r
Tactic:
generalize hg : (fun θ : ℝ ↦ deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = circleIntegral (f - g) c r
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = circleIntegral (f - g) c r
Tactic:
rw [circleIntegral]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • (f - g) (circleMap c r θ)
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    ∫ (θ : ℝ) in 0 ..2 * π, deriv (circleMap c r) θ • (f - g) (circleMap c r θ)
Tactic:
generalize hfg : (fun θ : ℝ ↦ deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume
Tactic:
have hs : fc - gc = fgc := by
  rw [← hf, ← hg, ← hfg]; funext
  simp only [deriv_circleMap, Algebra.id.smul_eq_mul, Pi.sub_apply, mul_sub_left_distrib]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume = intervalIntegral fgc 0 (2 * π) volume
Tactic:
rw [← hs]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
hs : fc - gc = fgc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume
Tactic:
clear hfg hs fgc
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume =
    intervalIntegral (fc - gc) 0 (2 * π) volume
Tactic:
symm
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
have fci := CircleIntegrable.out fi
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
rw [hf] at fci
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
have gci := CircleIntegrable.out gi
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
rw [hg] at gci
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable gc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fci : IntervalIntegrable fc volume 0 (2 * π)
gci : IntervalIntegrable gc volume 0 (2 * π)
⊢ intervalIntegral (fc - gc) 0 (2 * π) volume =
    intervalIntegral fc 0 (2 * π) volume - intervalIntegral gc 0 (2 * π) volume
Tactic:
exact intervalIntegral.integral_sub fci gci
Proof state after:
no goals
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ fc - gc = fgc
Tactic:
rw [← hf, ← hg, ← hfg]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) =
    fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)
Theorem: circleIntegral_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) =
    fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)
Tactic:
funext
Proof state after:
case h
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
x✝ : ℝ
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ))
      x✝ =
    deriv (circleMap c r) x✝ • (f - g) (circleMap c r x✝)
Theorem: circleIntegral_sub
Proof state before:
case h
f g : ℂ → ℂ
c : ℂ
r : ℝ
fi : CircleIntegrable f c r
gi : CircleIntegrable g c r
fc : ℝ → ℂ
hf : (fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) = fc
gc : ℝ → ℂ
hg : (fun θ => deriv (circleMap c r) θ • g (circleMap c r θ)) = gc
fgc : ℝ → ℂ
hfg : (fun θ => deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
x✝ : ℝ
⊢ ((fun θ => deriv (circleMap c r) θ • f (circleMap c r θ)) - fun θ => deriv (circleMap c r) θ • g (circleMap c r θ))
      x✝ =
    deriv (circleMap c r) x✝ • (f - g) (circleMap c r x✝)
Tactic:
simp only [deriv_circleMap, Algebra.id.smul_eq_mul, Pi.sub_apply, mul_sub_left_distrib]
Proof state after:
no goals
Theorem: circleMap_nz
Proof state before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
⊢ circleMap c (↑r) θ - c ≠ 0
Tactic:
simp only [circleMap_sub_center, Ne, circleMap_eq_center_iff, NNReal.coe_eq_zero]
Proof state after:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
⊢ ¬r = 0
Theorem: circleMap_nz
Proof state before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
⊢ ¬r = 0
Tactic:
intro h
Proof state after:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
h : r = 0
⊢ False
Theorem: circleMap_nz
Proof state before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : r > 0
h : r = 0
⊢ False
Tactic:
rw [h] at rp
Proof state after:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : 0 > 0
h : r = 0
⊢ False
Theorem: circleMap_nz
Proof state before:
c : ℂ
r : ℝ≥0
θ : ℝ
rp : 0 > 0
h : r = 0
⊢ False
Tactic:
simp only [gt_iff_lt, not_lt_zero'] at rp
Proof state after:
no goals
Theorem: cauchy_is_circleIntegrable
Proof state before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ CircleIntegrable (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) c ↑r
Tactic:
refine ContinuousOn.intervalIntegrable ?_
Proof state after:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Theorem: cauchy_is_circleIntegrable
Proof state before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (fun z => w ^ n / (z - c) ^ n * ((z - c)⁻¹ * f z)) (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.mul ?_ ?_
Proof state after:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => w ^ n / (circleMap c (↑r) θ - c) ^ n) (Set.uIcc 0 (2 * π))

case refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹ * f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => w ^ n / (circleMap c (↑r) θ - c) ^ n) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.mul continuousOn_const ?_
Proof state after:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹) (Set.uIcc 0 (2 * π))
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹) (Set.uIcc 0 (2 * π))
Tactic:
apply Continuous.continuousOn
Proof state after:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => ((circleMap c (↑r) θ - c) ^ n)⁻¹
Tactic:
refine Continuous.inv₀ ?_ fun x ↦ pow_ne_zero n (circleMap_nz rp)
Proof state after:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c) ^ n
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c) ^ n
Tactic:
apply Continuous.pow
Proof state after:
case refine_1.h.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun b => circleMap c (↑r) b - c
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_1.h.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun b => circleMap c (↑r) b - c
Tactic:
continuity
Proof state after:
no goals
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹ * f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.mul ?_ ?_
Proof state after:
case refine_2.refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹) (Set.uIcc 0 (2 * π))

case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_2.refine_1
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => (circleMap c (↑r) θ - c)⁻¹) (Set.uIcc 0 (2 * π))
Tactic:
apply Continuous.continuousOn
Proof state after:
case refine_2.refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c)⁻¹
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_2.refine_1.h
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => (circleMap c (↑r) θ - c)⁻¹
Tactic:
refine Continuous.inv₀ (by continuity) fun x ↦ circleMap_nz rp
Proof state after:
no goals
Theorem: cauchy_is_circleIntegrable
Proof state before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => circleMap c (↑r) θ - c
Tactic:
continuity
Proof state after:
no goals
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ ContinuousOn (fun θ => f (circleMap c (↑r) θ)) (Set.uIcc 0 (2 * π))
Tactic:
refine ContinuousOn.comp h (Continuous.continuousOn (by continuity)) ?_
Proof state after:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Set.MapsTo (fun θ => circleMap c (↑r) θ) (Set.uIcc 0 (2 * π)) (closedBall c ↑r)
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Set.MapsTo (fun θ => circleMap c (↑r) θ) (Set.uIcc 0 (2 * π)) (closedBall c ↑r)
Tactic:
intro θ _
Proof state after:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
θ : ℝ
a✝ : θ ∈ Set.uIcc 0 (2 * π)
⊢ (fun θ => circleMap c (↑r) θ) θ ∈ closedBall c ↑r
Theorem: cauchy_is_circleIntegrable
Proof state before:
case refine_2.refine_2
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
θ : ℝ
a✝ : θ ∈ Set.uIcc 0 (2 * π)
⊢ (fun θ => circleMap c (↑r) θ) θ ∈ closedBall c ↑r
Tactic:
exact circleMap_mem_closedBall c (NNReal.coe_nonneg r) θ
Proof state after:
no goals
Theorem: cauchy_is_circleIntegrable
Proof state before:
f : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
h : ContinuousOn f (closedBall c ↑r)
⊢ Continuous fun θ => circleMap c (↑r) θ
Tactic:
continuity
Proof state after:
no goals
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((cauchyPowerSeries f c (↑r) n) fun x => w) - (cauchyPowerSeries g c (↑r) n) fun x => w) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Tactic:
rw [cauchyPowerSeries_apply f c r n w]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (cauchyPowerSeries g c (↑r) n) fun x => w) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (cauchyPowerSeries g c (↑r) n) fun x => w) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Tactic:
rw [cauchyPowerSeries_apply g c r n w]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Theorem: cauchy_sub
Proof state before:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (cauchyPowerSeries (f - g) c (↑r) n) fun x => w
Tactic:
rw [cauchyPowerSeries_apply (f - g) c r n w]
Proof state after:
f g : ℂ → ℂ
c : ℂ
r : ℝ≥0
n : ℕ
w : ℂ
rp : r > 0
cf : ContinuousOn f (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ (((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) -
      (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • g z) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑r), (w / (z - c)) ^ n • (z - c)⁻¹ • (f - g) z