-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem changeOrigin_eval_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (x y : E) :
    (p.changeOrigin x).sum y = p.sum (x + y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)
k : ℕ
this : ∀ m ∉ Finset.range n, ((p.changeOriginSeries k m) fun x_1 => x) = 0
m : ℕ
hm : m ∉ Finset.range n
⊢ (((p.changeOriginSeries k m) fun x_1 => x) fun x => y) = 0

Tactic:
rw [this m hm, ContinuousMultilinearMap.zero_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
⊢ (p.changeOrigin x).sum y = p.sum (x + y)

Tactic:
let f (s : Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) : F :=
  p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ ↦ x) fun _ ↦ y

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
⊢ (p.changeOrigin x).sum y = p.sum (x + y)

Proof state:
case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : n ≤ s.fst + s.snd.fst
⊢ (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y) = 0

Tactic:
rw [changeOriginSeriesTerm_bound p hn _ _ _ hs, ContinuousMultilinearMap.zero_apply,
  ContinuousMultilinearMap.zero_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)
hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)
⊢ (p.changeOrigin x).sum y = p.sum (x + y)

Tactic:
have hf : HasSum f ((p.changeOrigin x).sum y) :=
  ((p.changeOrigin x).hasSum_of_finite (fun _ ↦ changeOrigin_finite_of_finite p hn) _)
    |>.sigma_of_hasSum hfk (summable_of_finite_support finsupp)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)
hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)
hf : HasSum f ((p.changeOrigin x).sum y)
⊢ (p.changeOrigin x).sum y = p.sum (x + y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n✝ : ℕ
hn : ∀ (m : ℕ), n✝ ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x => f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 => x) fun x => y)
hfk : ∀ (k : ℕ), HasSum (fun x => f ⟨k, x⟩) ((p.changeOrigin x k) fun x => y)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c => (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩)
    (∑ x_1 : Finset (Fin n),
      ((p.changeOriginSeriesTerm (changeOriginIndexEquiv.symm ⟨n, x_1⟩).fst
            (changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.fst ↑(changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.snd ⋯)
          fun x_2 => x)
        fun x => y)

Tactic:
exact hasSum_fintype fun c ↦ f (changeOriginIndexEquiv.symm ⟨n, c⟩)

Result:
no goals

Proof state:
case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : s ∉ ⇑changeOriginIndexEquiv ⁻¹' (Sigma.fst ⁻¹' {m | m < n})
⊢ f s = 0

Tactic:
simp only [preimage_setOf_eq, changeOriginIndexEquiv_apply_fst, mem_setOf, not_lt] at hs

Result:
case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : n ≤ s.fst + s.snd.fst
⊢ f s = 0

Proof state:
case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
⊢ Function.support f ⊆ ⇑changeOriginIndexEquiv ⁻¹' (Sigma.fst ⁻¹' {m | m < n})

Tactic:
refine fun s ↦ Not.imp_symm fun hs ↦ ?_

Result:
case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s => ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : s ∉ ⇑changeOriginIndexEquiv ⁻¹' (Sigma.fst ⁻¹' {m | m < n})
⊢ f s = 0