awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IteratedFDeriv (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x)) (iteratedFDeriv 𝕜 n f x)
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
  (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)
Tactic: rw [← iteratedFDerivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Linear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
m : ℕ
hm : LE.le (α := ℕ) 2 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (f.fpowerSeries x 0) 0
have linarith : HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Linear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
m : ℕ
hm : LE.le (α := ℕ) 2 0
linarith : HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 0 = 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (f.fpowerSeries x 0) 0
have linarith₁ : GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Linear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
m : ℕ
hm : LE.le (α := ℕ) 2 1
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (f.fpowerSeries x 1) 0
have linarith : -1 + HSub.hSub (α := ℤ) 2 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Linear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y : E × F
h : Membership.mem (γ := Set (E × F)) (Metric.eball 0 ∞) y
⊢ HasSum
    (fun (n : ℕ) ↦ (f.fpowerSeriesBilinear x (n + 3) : (a : (i : Fin (n + 3)) → E × F) → G) fun (x : Fin (n + 3)) ↦ y)
    (HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →L[𝕜] G) (x + y).1 : F →L[𝕜] G) : (a : F) → G) (x + y).2 : G)
      (∑ i ∈ Finset.range 3, (f.fpowerSeriesBilinear x i : (a : (i : Fin i) → E × F) → G) fun (x : Fin i) ↦ y : G))
have simp : HasSum
  (fun (n : ℕ) ↦ (f.fpowerSeriesBilinear x (n + 3) : (a : (i : Fin (n + 3)) → E × F) → G) fun (x : Fin (n + 3)) ↦ y)
  (HAdd.hAdd (β := G)
      (HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2 : G)
        ((((f.deriv₂ : (a : E × F) → E × F →L[𝕜] G) (x.1, x.2) : E × F →L[𝕜] G) : (a : E × F) → G) (y.1, y.2) : G))
      ((((f : (a : E) → F →L[𝕜] G) y.1 : F →L[𝕜] G) : (a : F) → G) y.2 : G) -
    HAdd.hAdd (β := G)
      (HAdd.hAdd (β := G)
        (HAdd.hAdd (α := G) (β := G)
          (∑ i ∈ Finset.range 0, (f.fpowerSeriesBilinear x i : (a : (i : Fin i) → E × F) → G) fun (x : Fin i) ↦ y : G)
          ((f.fpowerSeriesBilinear x 0 : (a : (i : Fin 0) → E × F) → G) fun (x : Fin 0) ↦ y : G))
        ((f.fpowerSeriesBilinear x 1 : (a : (i : Fin 1) → E × F) → G) fun (x : Fin 1) ↦ y : G))
      ((f.fpowerSeriesBilinear x 2 : (a : (i : Fin 2) → E × F) → G) fun (x : Fin 2) ↦ y : G))
Tactic: simp only [Finset.sum_range_succ, Prod.fst_add, Prod.snd_add, f.map_add_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
inst_5 : Nontrivial E
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0 ↔ c n = 0
have rw : c n = 0 ∨
    Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) 0 ↔
  c n = 0
Tactic: rw [ofScalars, smul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
inst_5 : Nontrivial E
n : ℕ
⊢ c n = 0 ∨
      Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) 0 ↔
    c n = 0
have refine : ∃ (x : (i : Fin n) → E),
  ¬Eq (α := E) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E : (a : (i : Fin n) → E) → E) x : E)
      ((0 : (a : (i : Fin n) → E) → E) x : E)
Tactic: refine or_iff_left (ContinuousMultilinearMap.ext_iff.1.mt <| not_forall_of_exists_not ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
inst_5 : Nontrivial E
n : ℕ
⊢ ∃ (x : (i : Fin n) → E),
    ¬Eq (α := E) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E : (a : (i : Fin n) → E) → E) x : E)
        ((0 : (a : (i : Fin n) → E) → E) x : E)
have h : ¬Eq (α := E) ((ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E : (a : (i : Fin n) → E) → E) fun (x : Fin n) ↦ 1 : E)
    ((0 : (a : (i : Fin n) → E) → E) fun (x : Fin n) ↦ 1 : E)
Tactic: use fun _ ↦ 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
hc : c n = 0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
have rw : HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
    (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
  0
Tactic: rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
hc : c n = 0
rw :
  HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) 0
    (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
  0
Tactic: rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
hc : c n = 0
rw :
  HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    0
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) 0
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
have rw₂ : Eq.{u_2 + 1} (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) 0 0
Tactic: rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
inst_5 : Subsingleton E
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E c : FormalMultilinearSeries 𝕜 E E)
    (0 : FormalMultilinearSeries 𝕜 E E)
have simp_rw : ∀ (n : ℕ) (x : (i : Fin n) → E),
  Eq (α := E)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) :
          (a : (i : Fin n) → E) → E)
        x :
      E)
    ((0 n : (a : (i : Fin n) → E) → E) x : E)
Tactic: simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
inst_5 : Nontrivial E
a₁ a₂ : ℕ → 𝕜
h :
  Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E a₁ : FormalMultilinearSeries 𝕜 E E)
    (ofScalars E a₂ : FormalMultilinearSeries 𝕜 E E)
⊢ a₁ = a₂
have h₁ : ∀ (n : ℕ), a₁ n = a₂ n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
⊢ Eq (α := E) ((ofScalars E c n : (a : (i : Fin n) → E) → E) fun (x : Fin n) ↦ 0 : E)
    (Pi.single (M := fun (x : ℕ) ↦ E) 0 (HSMul.hSMul (β := (fun (x : ℕ) ↦ E) 0) (c 0) 1) n : E)
have rw : Eq (α := E)
  ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
          (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) :
        (a : (i : Fin n) → E) → E)
      fun (x : Fin n) ↦ 0 :
    E)
  (Pi.single (M := fun (x : ℕ) ↦ E) 0 (HSMul.hSMul (β := (fun (x : ℕ) ↦ E) 0) (c 0) 1) n : E)
Tactic: rw [ofScalars]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
⊢ Eq (α := E)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) :
          (a : (i : Fin n) → E) → E)
        fun (x : Fin n) ↦ 0 :
      E)
    (Pi.single (M := fun (x : ℕ) ↦ E) 0 (HSMul.hSMul (β := (fun (x : ℕ) ↦ E) 0) (c 0) 1) n : E)
have zero : Eq (α := E)
  ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) E) (c 0)
          (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 E) :
        (a : (i : Fin 0) → E) → E)
      fun (x : Fin 0) ↦ 0 :
    E)
  (Pi.single (M := fun (x : ℕ) ↦ E) 0 (HSMul.hSMul (β := (fun (x : ℕ) ↦ E) 0) (c 0) 1) 0 : E)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
zero :
  Eq (α := E)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) E) (c 0)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 E) :
          (a : (i : Fin 0) → E) → E)
        fun (x : Fin 0) ↦ 0 :
      E)
    (Pi.single (M := fun (x : ℕ) ↦ E) 0 (HSMul.hSMul (β := (fun (x : ℕ) ↦ E) 0) (c 0) 1) 0 : E)
⊢ Eq (α := E)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) :
          (a : (i : Fin n) → E) → E)
        fun (x : Fin n) ↦ 0 :
      E)
    (Pi.single (M := fun (x : ℕ) ↦ E) 0 (HSMul.hSMul (β := (fun (x : ℕ) ↦ E) 0) (c 0) 1) n : E)
have succ : ∀ (n : ℕ),
  Eq (α := E)
    ((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (c (n + 1))
            (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n + 1) E) :
          (a : (i : Fin (n + 1)) → E) → E)
        fun (x : Fin (n + 1)) ↦ 0 :
      E)
    (Pi.single (M := fun (x : ℕ) ↦ E) 0 (HSMul.hSMul (β := (fun (x : ℕ) ↦ E) 0) (c 0) 1) (n + 1) : E)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ ofScalars E (c + c') =
    HAdd.hAdd (α := FormalMultilinearSeries 𝕜 E E) (β := FormalMultilinearSeries 𝕜 E E)
      (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (ofScalars E c' : FormalMultilinearSeries 𝕜 E E)
have h : ∀ (n : ℕ) (x : (i : Fin n) → E),
  Eq (α := E) ((ofScalars E (c + c') n : (a : (i : Fin n) → E) → E) x : E)
    ((HAdd.hAdd (α := FormalMultilinearSeries 𝕜 E E) (β := FormalMultilinearSeries 𝕜 E E)
            (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (ofScalars E c' : FormalMultilinearSeries 𝕜 E E) n :
          (a : (i : Fin n) → E) → E)
        x :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ ofScalars E (c - c') =
    HSub.hSub (α := FormalMultilinearSeries 𝕜 E E) (β := FormalMultilinearSeries 𝕜 E E)
      (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (ofScalars E c' : FormalMultilinearSeries 𝕜 E E)
have h : ∀ (n : ℕ) (x : (i : Fin n) → E),
  Eq (α := E) ((ofScalars E (c - c') n : (a : (i : Fin n) → E) → E) x : E)
    ((HSub.hSub (α := FormalMultilinearSeries 𝕜 E E) (β := FormalMultilinearSeries 𝕜 E E)
            (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (ofScalars E c' : FormalMultilinearSeries 𝕜 E E) n :
          (a : (i : Fin n) → E) → E)
        x :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
x : 𝕜
⊢ ofScalars E (x • c) =
    HSMul.hSMul (β := FormalMultilinearSeries 𝕜 E E) x (ofScalars E c : FormalMultilinearSeries 𝕜 E E)
have h : ∀ (n : ℕ) (x_1 : (i : Fin n) → E),
  Eq (α := E) ((ofScalars E (x • c) n : (a : (i : Fin n) → E) → E) x_1 : E)
    ((HSMul.hSMul (β := FormalMultilinearSeries 𝕜 E E) x (ofScalars E c : FormalMultilinearSeries 𝕜 E E) n :
          (a : (i : Fin n) → E) → E)
        x_1 :
      E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E) :
      FormalMultilinearSeries 𝕜 E E)
    (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
have h : ∀ (n : ℕ) (x : (i : Fin n) → E),
  Eq (α := E)
    ((compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E) n :
          (a : (i : Fin n) → E) → E)
        x :
      E)
    ((ofScalars E (fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k) n : (a : (i : Fin n) → E) → E) x : E)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
x : (i : Fin n) → E
⊢ Eq (α := E)
    ((compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E) n :
          (a : (i : Fin n) → E) → E)
        x :
      E)
    ((ofScalars E (fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k) n : (a : (i : Fin n) → E) → E) x : E)
have h : ∀ (h : Even n),
  Eq (α := E)
    ((compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E) n :
          (a : (i : Fin n) → E) → E)
        x :
      E)
    ((ofScalars E (fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k) n : (a : (i : Fin n) → E) → E) x : E)
Tactic: rcases n.even_or_odd with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
x : (i : Fin n) → E
h :
  ∀ (h : Even n),
    Eq (α := E)
      ((compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E) n :
            (a : (i : Fin n) → E) → E)
          x :
        E)
      ((ofScalars E (fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k) n : (a : (i : Fin n) → E) → E) x : E)
⊢ Eq (α := E)
    ((compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E) n :
          (a : (i : Fin n) → E) → E)
        x :
      E)
    ((ofScalars E (fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k) n : (a : (i : Fin n) → E) → E) x : E)
have h₁ : ∀ (h : Odd n),
  Eq (α := E)
    ((compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E) n :
          (a : (i : Fin n) → E) → E)
        x :
      E)
    ((ofScalars E (fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k) n : (a : (i : Fin n) → E) → E) x : E)
Tactic: rcases n.even_or_odd with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
| Eq (α := FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-f) : FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
        f :
      FormalMultilinearSeries 𝕜 E E)
have lhs : (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-f) : FormalMultilinearSeries 𝕜 E E)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
| (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-f) : FormalMultilinearSeries 𝕜 E E)
have rw : (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) :
  FormalMultilinearSeries 𝕜 E E)
Tactic: rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
| Eq (α := FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-f) : FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
        f :
      FormalMultilinearSeries 𝕜 E E)
have rw : (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) :
  FormalMultilinearSeries 𝕜 E E)
Tactic: lhs; rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-f) : FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
        f :
      FormalMultilinearSeries 𝕜 E E)
have conv : Eq (α := FormalMultilinearSeries 𝕜 E E)
  (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) :
    FormalMultilinearSeries 𝕜 E E)
  (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
      f :
    FormalMultilinearSeries 𝕜 E E)
Tactic: conv => lhs; rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) :
      FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
        f :
      FormalMultilinearSeries 𝕜 E E)
have rw : Eq (α := FormalMultilinearSeries 𝕜 E E)
  (compContinuousLinearMap
      (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E)) f :
    FormalMultilinearSeries 𝕜 E E)
  (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
      f :
    FormalMultilinearSeries 𝕜 E E)
Tactic: rw [← FormalMultilinearSeries.compContinuousLinearMap_comp, ofScalars_comp_neg_id]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : Ring E
inst_2 : Algebra 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
rw :
  Eq (α := FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap
        (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-ContinuousLinearMap.id 𝕜 E)) f :
      FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
        f :
      FormalMultilinearSeries 𝕜 E E)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) :
      FormalMultilinearSeries 𝕜 E E)
    (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
        f :
      FormalMultilinearSeries 𝕜 E E)
have rw₁ : Eq (α := FormalMultilinearSeries 𝕜 E E)
  (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
      f :
    FormalMultilinearSeries 𝕜 E E)
  (compContinuousLinearMap (ofScalars E fun (k : ℕ) ↦ HPow.hPow (α := 𝕜) (-1) k * c k : FormalMultilinearSeries 𝕜 E E)
      f :
    FormalMultilinearSeries 𝕜 E E)
Tactic: rw [← FormalMultilinearSeries.compContinuousLinearMap_comp, ofScalars_comp_neg_id]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) =
    ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
have rw : ‖HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
      (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)‖ =
  ‖c n‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
Tactic: rw [ofScalars, norm_smul]