Theorem: cauchy2_hasSum (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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))
Tactic:
have sum := (cauchy2_hasSum_2d h w0m w1m).antidiagonal_of_2d
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
sum :
  HasSum
    (fun n =>
      (Finset.range (n + 1)).sum fun n1 =>
        w0 ^ (n1, n - n1).2 • w1 ^ (n1, n - n1).1 • h.series2Coeff (n1, n - n1).2 (n1, n - n1).1)
    (f (c0 + w0, c1 + w1))
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
sum :
  HasSum
    (fun n =>
      (Finset.range (n + 1)).sum fun n1 =>
        w0 ^ (n1, n - n1).2 • w1 ^ (n1, n - n1).1 • h.series2Coeff (n1, n - n1).2 (n1, n - n1).1)
    (f (c0 + w0, c1 + w1))
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))
Tactic:
simp only [ge_iff_le] at sum
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
sum :
  HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x)
    (f (c0 + w0, c1 + w1))
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
sum :
  HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x)
    (f (c0 + w0, c1 + w1))
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) (f (c0 + w0, c1 + w1))
Tactic:
generalize ha : f (c0 + w0, c1 + w1) = a
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
sum :
  HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x)
    (f (c0 + w0, c1 + w1))
a : E
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
sum :
  HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x)
    (f (c0 + w0, c1 + w1))
a : E
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
rw [ha] at sum
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
ha : f (c0 + w0, c1 + w1) = a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
clear ha
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
have e : (fun n ↦
    (Finset.range (n + 1)).sum fun n1 ↦ w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    fun n ↦ series2 h n fun _ : Fin n ↦ (w0, w1) := by
  clear sum; funext n
  rw [series2]; simp only [ge_iff_le, ContinuousMultilinearMap.sum_apply]
  simp_rw [termCmmap_apply]
  nth_rw 1 [← Finset.sum_range_reflect]; simp
  apply Finset.sum_congr rfl
  intro n0 n0n'; simp only [Finset.mem_range] at n0n'
  have n0n := Nat.le_of_lt_succ n0n'
  rw [Nat.sub_sub_self n0n, min_eq_left n0n]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
e :
  (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
e :
  (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
⊢ HasSum (fun n => (series2 h n) fun x => (w0, w1)) a
Tactic:
rwa [←e]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
sum : HasSum (fun n => (Finset.range (n + 1)).sum fun x => w0 ^ (n - x) • w1 ^ x • h.series2Coeff (n - x) x) a
⊢ (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
Tactic:
clear sum
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
⊢ (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
⊢ (fun n => (Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) = fun n =>
    (series2 h n) fun x => (w0, w1)
Tactic:
funext n
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (series2 h n) fun x => (w0, w1)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (series2 h n) fun x => (w0, w1)
Tactic:
rw [series2]
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    ((Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))) fun x => (w0, w1)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    ((Finset.range (n + 1)).sum fun n0 => termCmmap ℂ n n0 (h.series2Coeff n0 (n - n0))) fun x => (w0, w1)
Tactic:
simp only [ge_iff_le, ContinuousMultilinearMap.sum_apply]
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun a => (termCmmap ℂ n a (h.series2Coeff a (n - a))) fun x => (w0, w1)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun a => (termCmmap ℂ n a (h.series2Coeff a (n - a))) fun x => (w0, w1)
Tactic:
simp_rw [termCmmap_apply]
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun n1 => w0 ^ (n - n1) • w1 ^ n1 • h.series2Coeff (n - n1) n1) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
nth_rw 1 [← Finset.sum_range_reflect]
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun j =>
      w0 ^ (n - (n + 1 - 1 - j)) • w1 ^ (n + 1 - 1 - j) • h.series2Coeff (n - (n + 1 - 1 - j)) (n + 1 - 1 - j)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun j =>
      w0 ^ (n - (n + 1 - 1 - j)) • w1 ^ (n + 1 - 1 - j) • h.series2Coeff (n - (n + 1 - 1 - j)) (n + 1 - 1 - j)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
simp
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun x => w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ((Finset.range (n + 1)).sum fun x => w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x)) =
    (Finset.range (n + 1)).sum fun x => w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
apply Finset.sum_congr rfl
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x) =
      w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    w0 ^ (n - (n - x)) • w1 ^ (n - x) • h.series2Coeff (n - (n - x)) (n - x) =
      w0 ^ min x n • w1 ^ (n - x) • h.series2Coeff x (n - x)
Tactic:
intro n0 n0n'
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 ∈ Finset.range (n + 1)
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 ∈ Finset.range (n + 1)
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Tactic:
simp only [Finset.mem_range] at n0n'
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Tactic:
have n0n := Nat.le_of_lt_succ n0n'
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
n0n : n0 ≤ n
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
a : E
n n0 : ℕ
n0n' : n0 < n + 1
n0n : n0 ≤ n
⊢ w0 ^ (n - (n - n0)) • w1 ^ (n - n0) • h.series2Coeff (n - (n - n0)) (n - n0) =
    w0 ^ min n0 n • w1 ^ (n - n0) • h.series2Coeff n0 (n - n0)
Tactic:
rw [Nat.sub_sub_self n0n, min_eq_left n0n]
State after:
no goals