Theorem: uneven_is_cauchy (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
⊢ unevenSeries' u r z1 = cauchyPowerSeries (fun z0 => f (z0, z1)) c0 r
Tactic:
funext
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = cauchyPowerSeries (fun z0 => f (z0, z1)) c0 r x✝

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = cauchyPowerSeries (fun z0 => f (z0, z1)) c0 r x✝
Tactic:
rw [unevenSeries', cauchyPowerSeries]
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝) (unevenTerm' u r z1 x✝) =
    ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝)
      ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r), (z - c0)⁻¹ ^ x✝ • (z - c0)⁻¹ • f (z, z1))

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝) (unevenTerm' u r z1 x✝) =
    ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝)
      ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r), (z - c0)⁻¹ ^ x✝ • (z - c0)⁻¹ • f (z, z1))
Tactic:
rfl
State after:
no goals