Theorem: cauchy1 (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, r), (z - w)⁻¹ • f z) = f w
Tactic:
refine Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
  Set.countable_empty wm fc ?_
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
⊢ ∀ x ∈ ball c r \ ∅, DifferentiableAt ℂ (fun z => f z) x

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
⊢ ∀ x ∈ ball c r \ ∅, DifferentiableAt ℂ (fun z => f z) x
Tactic:
intro z zm
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ DifferentiableAt ℂ (fun z => f z) z

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ DifferentiableAt ℂ (fun z => f z) z
Tactic:
apply fd z _
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ z ∈ ball c r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : z ∈ ball c r \ ∅
⊢ z ∈ ball c r
Tactic:
simp only [Metric.mem_ball, Set.diff_empty] at zm ⊢
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : dist z c < r
⊢ dist z c < r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b r : ℝ
c w : ℂ
f : ℂ → E
wm : w ∈ ball c r
fc : ContinuousOn f (closedBall c r)
fd : ∀ z ∈ ball c r, DifferentiableAt ℂ f z
z : ℂ
zm : dist z c < r
⊢ dist z c < r
Tactic:
assumption
State after:
no goals