awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ ∞ ≤ p.radius
have rw : LE.le (α := ℝ≥0∞) ∞ ∞
Tactic: rw [radius_eq_top_of_forall_image_add_eq_zero p n fun _ => hn _ (Nat.le_add_left _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
h : Membership.mem (γ := Set E) (Metric.eball 0 ∞) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum (0 + y))
have rw : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    p.sum
have rw : ContinuousOn p.sum (Metric.eball 0 ∞)
Tactic: rw [← continuousOn_univ, ← Metric.eball_top]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
rw : ContinuousOn p.sum (Metric.eball 0 ∞)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    p.sum
have rw₁ : E
Tactic: rw [← continuousOn_univ, ← Metric.eball_top]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
hkl : n ≤ k + l
⊢ p.changeOriginSeriesTerm k l s hs = 0
have rw : ZeroHomClass
  (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F))
  (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F)
  (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ E)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F))
Tactic: rw [changeOriginSeriesTerm, hn _ hkl, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
⊢ (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)
have h : ∀ (x : E) (x_1 : (i : Fin k) → E),
  Eq.{u_3 + 1} (α := F) (((p.changeOriginSeries k).sum x : (a : (i : Fin k) → E) → F) x_1 : F)
    (((p.changeOriginSeries k).partialSum (n - k) x : (a : (i : Fin k) → E) → F) x_1 : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
⊢ Eq.{u_3 + 1} (α := F) (((p.changeOriginSeries k).sum x : (a : (i : Fin k) → E) → F) x_1 : F)
    (((p.changeOriginSeries k).partialSum (n - k) x : (a : (i : Fin k) → E) → F) x_1 : F)
have h : ∀ b ∉ Finset.range (n - k),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k b : (a : (i : Fin b) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_2 : Fin b) ↦ x)
    0
Tactic: rw [partialSum, FormalMultilinearSeries.sum,
    tsum_eq_sum (f := fun m => p.changeOriginSeries k m (fun _ => x)) (s := Finset.range (n - k))]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : m ∉ Finset.range (n - k)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_2 : Fin m) ↦ x)
    0
have hm₁ : n - k ≤ m
Tactic: rw [Finset.mem_range, not_lt] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : n - k ≤ m
⊢ n ≤ k + m
have rw : n ≤ m + k
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : n - k ≤ m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_2 : Fin m) ↦ x)
    0
have h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
  ((0 : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) fun (x_2 : Fin m) ↦ x) 0
Tactic: rw [p.changeOriginSeries_finite_of_finite hn k (by rw [add_comm]; exact Nat.le_add_of_sub_le hm),
    ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : n - k ≤ m
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((0 : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) fun (x_2 : Fin m) ↦ x) 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_2 : Fin m) ↦ x)
    0
have h₁ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F) 0 0
Tactic: rw [p.changeOriginSeries_finite_of_finite hn k (by rw [add_comm]; exact Nat.le_add_of_sub_le hm),
    ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
⊢ p.changeOrigin x k = 0
have rw : (p.changeOriginSeries k).partialSum (n - k) x = 0
Tactic: rw [changeOrigin, p.changeOriginSeries_sum_eq_partialSum_of_finite hn]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
⊢ (p.changeOriginSeries k).partialSum (n - k) x = 0
have h : ∀ x_1 ∈ Finset.range (n - k),
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k x_1 : (a : (i : Fin x_1) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_2 : Fin x_1) ↦ x)
    0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
m : ℕ
hm : m ∈ Finset.range (n - k)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_1 : Fin m) ↦ x)
    0
have hm₁ : m < n - k
Tactic: rw [Finset.mem_range] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
m : ℕ
hm : m < n - k
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_1 : Fin m) ↦ x)
    0
have h : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
  ((0 : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) fun (x_1 : Fin m) ↦ x) 0
Tactic: rw [p.changeOriginSeries_finite_of_finite hn k (le_add_of_le_left hk),
    ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
hk : n ≤ k
m : ℕ
hm : m < n - k
h :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((0 : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) fun (x_1 : Fin m) ↦ x) 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_1 : Fin m) ↦ x)
    0
have h₁ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F) 0 0
Tactic: rw [p.changeOriginSeries_finite_of_finite hn k (le_add_of_le_left hk),
    ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n k : ℕ
hn : ∀ (m : ℕ), n + k ≤ m → p m = 0
x : ℕ
hm : n ≤ x
⊢ n + k ≤ k + x
have grw : x + k ≤ k + x
Tactic: grw [hm, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n k : ℕ
hn : ∀ (m : ℕ), n + k ≤ m → p m = 0
x : ℕ
hm : n ≤ x
grw : x + k ≤ k + x
⊢ n + k ≤ k + x
have grw₁ : k + x ≤ k + x
Tactic: grw [hm, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
⊢ (Function.support f).Finite
have hs : Set.Finite (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
  (preimage (β := (n : ℕ) × Finset (Fin n))
    (⇑changeOriginIndexEquiv :
      (a : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → (n : ℕ) × Finset (Fin n))
    (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n}))
Tactic: apply Set.Finite.subset (s := changeOriginIndexEquiv ⁻¹' Sigma.fst ⁻¹' {m | m < n})
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
hs :
  Set.Finite (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
    (preimage (β := (n : ℕ) × Finset (Fin n))
      (⇑changeOriginIndexEquiv :
        (a : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → (n : ℕ) × Finset (Fin n))
      (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n}))
⊢ (Function.support f).Finite
have ht : Function.support f ⊆
  preimage (β := (n : ℕ) × Finset (Fin n))
    (⇑changeOriginIndexEquiv :
      (a : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → (n : ℕ) × Finset (Fin n))
    (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n})
Tactic: apply Set.Finite.subset (s := changeOriginIndexEquiv ⁻¹' Sigma.fst ⁻¹' {m | m < n})
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
⊢ Set.Finite (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
    (preimage (β := (n : ℕ) × Finset (Fin n))
      (⇑changeOriginIndexEquiv :
        (a : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → (n : ℕ) × Finset (Fin n))
      (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n}))
have hs : Set.Finite (α := (n : ℕ) × Finset (Fin n)) (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n})
Tactic: apply Set.Finite.preimage (Equiv.injective _).injOn
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
⊢ Set.Finite (α := (n : ℕ) × Finset (Fin n)) (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n})
have hs : Set.Finite (α := (n : ℕ) × Finset (Fin n))
  (⋃ (i : (↑{m : ℕ | m < n} : Type)), range (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) (↑i : ℕ)))
Tactic: simp_rw [← {m | m < n}.iUnion_of_singleton_coe, preimage_iUnion, ← range_sigmaMk]