Theorem: unevenSeries_eq (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 : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
⊢ z1 ∈ closedBall c1 r1 → unevenSeries' u r z1 = unevenSeries u z1
Tactic:
intro z1s
State after:
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 : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenSeries' u r z1 = unevenSeries u z1

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 : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenSeries' u r z1 = unevenSeries u z1
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 : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = unevenSeries u z1 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 : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = unevenSeries u z1 x✝
Tactic:
simp_rw [unevenSeries, unevenSeries', unevenTerm_eq u rp rr1 z1s,
  unevenTerm_eq u u.r1p (le_refl _) z1s]
State after:
no goals