awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
hn : minSmoothness 𝕜 2 ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
h'x : x ∈ s
m : ℕ∞ω
hm : minSmoothness 𝕜 (↑2 : ℕ∞ω) ≤ m
hmn : m ≤ n
m_ne : m ≠ ∞
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 m f (s ∩ u)
h'u : UniqueDiffOn 𝕜 (s ∩ u)
y : ℕ → E
hy : ∀ (n : ℕ), y n ∈ interior s
y_lim : Tendsto y atTop (𝓝 x)
L : ∀ᶠ (k : ℕ) in atTop, y k ∈ u
I : ∀ᶠ (k : ℕ) in atTop, IsSymmSndFDerivWithinAt 𝕜 f s (y k)
A : ContinuousOn (Y := E →L[𝕜] E →L[𝕜] F) (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s) (s ∩ u)
B :
  Tendsto (β := E →L[𝕜] E →L[𝕜] F) (fun (k : ℕ) ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k)) atTop
    (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x))
C :
  ∀ (v w : E),
    Tendsto.{0, u_3} (β := F)
      (fun (k : ℕ) ↦
        ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F))
      atTop
      (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x
have C' : ∀ (v w : E),
  Tendsto.{0, u_3} (β := F)
    (fun (k : ℕ) ↦
      ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F))
    atTop
    (𝓝 ((((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w) : Filter F)
Tactic: have C' (v w : E) : Tendsto (fun k ↦ fderivWithin 𝕜 (fderivWithin 𝕜 f s) s (y k) w v) atTop
      (𝓝 (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v w)) := by
    apply (C v w).congr'
    filter_upwards [I] with k hk using hk v w
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
⊢ DifferentiableWithinAt 𝕜 f t y ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y
have have : ∀ (this : Fintype ι),
  DifferentiableWithinAt 𝕜 f t y ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ DifferentiableWithinAt 𝕜 f t y ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y
have rw : (∀ (i : ι),
    DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i)
      (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t y) ↔
  ∀ (i : ι), DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t y
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableWithinAt_iff,
    differentiableWithinAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
y : H
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y
have have : ∀ (this : Fintype ι),
  DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
y : H
this : Fintype ι
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y
have rw : (∀ (i : ι),
    DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i)
      (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) y) ↔
  ∀ (i : ι), DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) y
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableAt_iff, differentiableAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t
have have : ∀ (this : Fintype ι),
  DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
this : Fintype ι
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t
have rw : (∀ (i : ι),
    DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i)
      (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) t) ↔
  ∀ (i : ι), DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := E i) (fun (x : H) ↦ (f x).ofLp i) t
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableOn_iff, differentiableOn_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i
have have : ∀ (this : Fintype ι),
  Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
this : Fintype ι
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i
have rw : (∀ (i : ι),
    Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦
      ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) ↔
  ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiable_iff, differentiable_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
⊢ HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
have have : ∀ (this : Fintype ι),
  HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
this : Fintype ι
⊢ HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
have rw : (∀ (i : ι),
    HasStrictFDerivAt (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i)
      (comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := E) i)
        ((↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) ∘SL f'))
      y) ↔
  ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasStrictFDerivAt_iff, hasStrictFDerivAt_pi']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
⊢ HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
have have : ∀ (this : Fintype ι),
  HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.WithLp (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
have rw : (∀ (i : ι),
    HasFDerivWithinAt (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i)
      (comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := E) i)
        ((↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) ∘SL f'))
      t y) ↔
  ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
Tactic: rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasFDerivWithinAt_iff, hasFDerivWithinAt_pi']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommMonoid F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ p.removeZero n = p n
have rw : Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n.pred.succ) ↦ E) F) (p.removeZero n.pred.succ)
  (p n.pred.succ)
Tactic: rw [← Nat.succ_pred_eq_of_pos h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommMonoid F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m n : ℕ
v : Fin m → E
w : Fin n → E
h1 : m = n
h2 : ∀ (i : ℕ) (him : i < m) (hin : i < n), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩
⊢ Eq.{w + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) v : F) ((p n : (a : (i : Fin n) → E) → F) w : F)
have subst : ∀ {w : Fin m → E} (h2 : ∀ (i : ℕ) (him hin : i < m), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩),
  Eq.{w + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) v : F) ((p m : (a : (i : Fin m) → E) → F) w : F)
Tactic: subst n
Cleared hypotheses: n, w, h1, h2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommMonoid F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩
⊢ Eq.{w + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) v : F) ((p m : (a : (i : Fin m) → E) → F) w : F)
have h : ∀ (i : ℕ) (hi : i < m), v (⟨i, hi⟩ : Fin m) = w ⟨i, hi⟩
Tactic: congr with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
⊢ (p.unshift z).shift = p
have h : ∀ (n : ℕ), (p.unshift z).shift n = p n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
⊢ (p n : (a : (i : Fin n) → 𝕜) → E) y = HSMul.hSMul.{u, v, v} (α := 𝕜) (∏ i : Fin n, y i) (p.coeff n)
have h : ∀ (x : Fin n), y x = HSMul.hSMul (β := 𝕜) (y x) (1 x)
Tactic: convert! (p n).toMultilinearMap.map_smul_univ y 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ p.coeff n = 0 ↔ p n = 0
have rw : p.coeff n = 0 ↔
  Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) E) (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n))
    0
Tactic: rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
rw :
  p.coeff n = 0 ↔
    Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) E)
      (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n)) 0
⊢ p.coeff n = 0 ↔ p n = 0
have rw₁ : p.coeff n = 0 ↔ p.coeff n = 0
Tactic: rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ ‖p n‖ = ‖p.coeff n‖
have rw : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) E)
    (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n)) =
  ‖p.coeff n‖
Tactic: rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.norm_mkPiRing]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
rw :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ 𝕜) E)
      (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n)) =
    ‖p.coeff n‖
⊢ ‖p n‖ = ‖p.coeff n‖
have rw₁ : ‖p.coeff n‖ = ‖p.coeff n‖
Tactic: rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.norm_mkPiRing]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ p.fslope.coeff n = p.coeff (n + 1)
have simp : Eq.{v + 1} (α := E) ((p (n + 1) : (a : (i : Fin n.succ) → 𝕜) → E) (cons (α := fun (i : Fin (n + 1)) ↦ 𝕜) 1 1) : E)
  ((p (n + 1) : (a : (i : Fin (n + 1)) → 𝕜) → E) 1 : E)
Tactic: simp only [fslope, coeff, ContinuousMultilinearMap.curryLeft_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ Eq.{v + 1} (α := E) ((p (n + 1) : (a : (i : Fin n.succ) → 𝕜) → E) (cons (α := fun (i : Fin (n + 1)) ↦ 𝕜) 1 1) : E)
    ((p (n + 1) : (a : (i : Fin (n + 1)) → 𝕜) → E) 1 : E)
have h : Eq.{u + 1} (α := (i : Fin n.succ) → 𝕜) (cons (α := fun (i : Fin (n + 1)) ↦ 𝕜) 1 1) 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
k n : ℕ
⊢ (fslope^[k] p).coeff n = p.coeff (n + k)
have zero : ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E}, (fslope^[0] p).coeff n = p.coeff (n + 0)
Tactic: induction k generalizing p with
  | zero => rfl
  | succ k ih => simp [ih, add_assoc]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
k n : ℕ
zero : ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E}, (fslope^[0] p).coeff n = p.coeff (n + 0)
⊢ (fslope^[k] p).coeff n = p.coeff (n + k)
have succ : ∀ (k : ℕ) (ih : ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E}, (fslope^[k] p).coeff n = p.coeff (n + k))
  {p : FormalMultilinearSeries 𝕜 𝕜 E}, (fslope^[k + 1] p).coeff n = p.coeff (n + (k + 1))
Tactic: induction k generalizing p with
  | zero => rfl
  | succ k ih => simp [ih, add_assoc]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
⊢ Eq (α := FormalMultilinearSeries 𝕜 E F) (constFormalMultilinearSeries 𝕜 E 0 : FormalMultilinearSeries 𝕜 E F)
    (0 : FormalMultilinearSeries 𝕜 E F)
have h : ∀ (n : ℕ) (x : (i : Fin n) → E),
  Eq.{w + 1} (α := F) ((constFormalMultilinearSeries 𝕜 E 0 n : (a : (i : Fin n) → E) → F) x : F)
    ((0 n : (a : (i : Fin n) → E) → F) x : F)
Tactic: ext n x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
n : ℕ
x : (i : Fin n) → E
⊢ Eq.{w + 1} (α := F) ((constFormalMultilinearSeries 𝕜 E 0 n : (a : (i : Fin n) → E) → F) x : F)
    ((0 n : (a : (i : Fin n) → E) → F) x : F)
have h : Eq.{w + 1} (α := F)
  (((match (motive := (x : ℕ) → ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin x) ↦ E) F) n with
          | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
          | x => 0 :
          ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n) ↦ E) F) :
        (a : (i : Fin n) → E) → F)
      x :
    F)
  (0 : F)
Tactic: simp only [FormalMultilinearSeries.zero_apply, ContinuousMultilinearMap.zero_apply,
    constFormalMultilinearSeries]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
n : ℕ
x : (i : Fin n) → E
⊢ Eq.{w + 1} (α := F)
    (((match (motive := (x : ℕ) → ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin x) ↦ E) F) n with
            | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
            | x => 0 :
            ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        x :
      F)
    (0 : F)
have h : ∀ (x : (i : Fin 0) → E),
  Eq.{w + 1} (α := F)
    (((match (motive := (x : ℕ) → ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin x) ↦ E) F) 0 with
            | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
            | x => 0 :
            ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 0) ↦ E) F) :
          (a : (i : Fin 0) → E) → F)
        x :
      F)
    (0 : F)
Tactic: induction n
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FormalMultilinearSeries (goal)
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
n : ℕ
x : (i : Fin n) → E
h :
  ∀ (x : (i : Fin 0) → E),
    Eq.{w + 1} (α := F)
      (((match (motive := (x : ℕ) → ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin x) ↦ E) F) 0 with
              | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
              | x => 0 :
              ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 0) ↦ E) F) :
            (a : (i : Fin 0) → E) → F)
          x :
        F)
      (0 : F)
⊢ Eq.{w + 1} (α := F)
    (((match (motive := (x : ℕ) → ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin x) ↦ E) F) n with
            | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
            | x => 0 :
            ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n) ↦ E) F) :
          (a : (i : Fin n) → E) → F)
        x :
      F)
    (0 : F)
have h₁ : ∀ (n : ℕ),
  (∀ (x : (i : Fin n) → E),
      Eq.{w + 1} (α := F)
        (((match (motive := (x : ℕ) → ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin x) ↦ E) F) n with
                | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
                | x => 0 :
                ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n) ↦ E) F) :
              (a : (i : Fin n) → E) → F)
            x :
          F)
        (0 : F)) →
    ∀ (x : (i : Fin (n + 1)) → E),
      Eq.{w + 1} (α := F)
        (((match (motive := (x : ℕ) → ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin x) ↦ E) F) n + 1 with
                | 0 => ContinuousMultilinearMap.uncurry0 𝕜 E 0
                | x => 0 :
                ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) :
              (a : (i : Fin (n + 1)) → E) → F)
            x :
          F)
        (0 : F)
Tactic: induction n
Cleared hypotheses: n, x