awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Linear
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 : E × F
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) (F := G)
    (fun (x : E × F) ↦ (((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2) (f.fpowerSeriesBilinear x) x

Tactic:
⟨∞, f.hasFPowerSeriesOnBall_bilinear x⟩

Premises used: ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear, Exists.intro, HasFPowerSeriesAt, Top.top
-- Module: Mathlib.Analysis.Analytic.Linear
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 : E × F
⊢ AnalyticAt 𝕜 (F := G) (fun (x : E × F) ↦ (((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2) x

Tactic:
(f.hasFPowerSeriesAt_bilinear x).analyticAt

Premises used: ContinuousLinearMap.hasFPowerSeriesAt_bilinear, HasFPowerSeriesAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set (E × F)
x : E × F
⊢ AnalyticWithinAt 𝕜 (F := G) (fun (x : E × F) ↦ (((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2) s x

Tactic:
(f.analyticAt_bilinear x).analyticWithinAt

Premises used: AnalyticAt.analyticWithinAt, ContinuousLinearMap.analyticAt_bilinear
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set (E × F)
⊢ AnalyticOnNhd 𝕜 (F := G) (fun (x : E × F) ↦ (((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2) s

Tactic:
fun x _ ↦ f.analyticAt_bilinear x

Premises used: AnalyticOnNhd, ContinuousLinearMap.analyticAt_bilinear
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set (E × F)
⊢ AnalyticOn 𝕜 (F := G) (fun (x : E × F) ↦ (((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2) s

Tactic:
(f.analyticOnNhd_bilinear s).analyticOn

Premises used: ContinuousLinearMap.analyticOnNhd_bilinear, AnalyticOnNhd.analyticOn
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z : E
⊢ AnalyticAt 𝕜 id z

Tactic:
(ContinuousLinearMap.id 𝕜 E).analyticAt z

Premises used: ContinuousLinearMap.analyticAt, ContinuousLinearMap.id
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
z : E
⊢ AnalyticWithinAt 𝕜 id s z

Tactic:
analyticAt_id.analyticWithinAt

Premises used: analyticAt_id, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ AnalyticOnNhd 𝕜 (F := E) (fun (x : E) ↦ x) s

Tactic:
fun _ _ ↦ analyticAt_id

Premises used: AnalyticOnNhd, analyticAt_id
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
⊢ AnalyticOn 𝕜 (F := E) (fun (x : E) ↦ x) s

Tactic:
fun _ _ ↦ analyticWithinAt_id

Premises used: analyticWithinAt_id, AnalyticOn
-- Module: Mathlib.Analysis.Analytic.Linear
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
p : E × F
⊢ AnalyticAt 𝕜 (F := E) (fun (p : E × F) ↦ p.1) p

Tactic:
(ContinuousLinearMap.fst 𝕜 E F).analyticAt p

Premises used: ContinuousLinearMap.analyticAt, ContinuousLinearMap.fst
-- Module: Mathlib.Analysis.Analytic.Linear
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
t : Set (E × F)
p : E × F
⊢ AnalyticWithinAt 𝕜 (F := E) (fun (p : E × F) ↦ p.1) t p

Tactic:
analyticAt_fst.analyticWithinAt

Premises used: analyticAt_fst, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Linear
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
p : E × F
⊢ AnalyticAt 𝕜 (F := F) (fun (p : E × F) ↦ p.2) p

Tactic:
(ContinuousLinearMap.snd 𝕜 E F).analyticAt p

Premises used: ContinuousLinearMap.analyticAt, ContinuousLinearMap.snd
-- Module: Mathlib.Analysis.Analytic.Linear
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
t : Set (E × F)
p : E × F
⊢ AnalyticWithinAt 𝕜 (F := F) (fun (p : E × F) ↦ p.2) t p

Tactic:
analyticAt_snd.analyticWithinAt

Premises used: AnalyticAt.analyticWithinAt, analyticAt_snd
-- Module: Mathlib.Analysis.Analytic.Linear
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
t : Set (E × F)
⊢ AnalyticOnNhd 𝕜 (F := E) (fun (p : E × F) ↦ p.1) t

Tactic:
fun _ _ ↦ analyticAt_fst

Premises used: AnalyticOnNhd, analyticAt_fst
-- Module: Mathlib.Analysis.Analytic.Linear
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
t : Set (E × F)
⊢ AnalyticOn 𝕜 (F := E) (fun (p : E × F) ↦ p.1) t

Tactic:
fun _ _ ↦ analyticWithinAt_fst

Premises used: AnalyticOn, analyticWithinAt_fst
-- Module: Mathlib.Analysis.Analytic.Linear
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
t : Set (E × F)
⊢ AnalyticOnNhd 𝕜 (F := F) (fun (p : E × F) ↦ p.2) t

Tactic:
fun _ _ ↦ analyticAt_snd

Premises used: AnalyticOnNhd, analyticAt_snd
-- Module: Mathlib.Analysis.Analytic.Linear
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
t : Set (E × F)
⊢ AnalyticOn 𝕜 (F := F) (fun (p : E × F) ↦ p.2) t

Tactic:
fun _ _ ↦ analyticWithinAt_snd

Premises used: analyticWithinAt_snd, AnalyticOn
-- Module: Mathlib.Analysis.Analytic.Linear
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
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) x

Tactic:
((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt

Premises used: ContinuousLinearMap.hasFPowerSeriesAt, HasFPowerSeriesAt.analyticAt, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set E
⊢ AnalyticOnNhd.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
fun x _ ↦ f.analyticAt x

Premises used: AnalyticOnNhd, ContinuousLinearEquiv.analyticAt
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set E
x : E
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s x

Tactic:
(f.analyticAt x).analyticWithinAt

Premises used: AnalyticAt.analyticWithinAt, ContinuousLinearEquiv.analyticAt
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set E
⊢ AnalyticOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
fun x _ ↦ f.analyticWithinAt _ x

Premises used: AnalyticOn, ContinuousLinearEquiv.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Linear
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
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) x

Tactic:
((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt

Premises used: ContinuousLinearMap.hasFPowerSeriesAt, LinearIsometryEquiv.toContinuousLinearEquiv, HasFPowerSeriesAt.analyticAt, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set E
⊢ AnalyticOnNhd.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
fun x _ ↦ f.analyticAt x

Premises used: AnalyticOnNhd, LinearIsometryEquiv.analyticAt
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set E
x : E
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s x

Tactic:
(f.analyticAt x).analyticWithinAt

Premises used: LinearIsometryEquiv.analyticAt, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Linear
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
s : Set E
⊢ AnalyticOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
fun x _ ↦ f.analyticWithinAt _ x

Premises used: AnalyticOn, LinearIsometryEquiv.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.OfScalars
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 : ℕ
rw :
  c n = 0 ∨
      Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) 0 ↔
    c n = 0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0 ↔ c n = 0

Tactic:
rw [ofScalars, smul_eq_zero]

Premises used: FormalMultilinearSeries.ofScalars, smul_eq_zero
-- Module: Mathlib.Analysis.Analytic.OfScalars
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

Tactic:
or_iff_left (ContinuousMultilinearMap.ext_iff.1.mt <| not_forall_of_exists_not ?_)

Premises used: Function.mt, not_forall_of_exists_not, Iff.mp, or_iff_left, ContinuousMultilinearMap.ext_iff
-- Module: Mathlib.Analysis.Analytic.OfScalars
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 : ℕ
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)
⊢ c n = 0 ∨
      Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) 0 ↔
    c n = 0

Tactic:
refine or_iff_left (ContinuousMultilinearMap.ext_iff.1.mt <| not_forall_of_exists_not ?_)

Premises used: Function.mt, not_forall_of_exists_not, Iff.mp, or_iff_left, ContinuousMultilinearMap.ext_iff
-- Module: Mathlib.Analysis.Analytic.OfScalars
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 : ℕ
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)
⊢ ∃ (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:
use fun _ ↦ 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.OfScalars
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 (α := 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:
simp
-- Module: Mathlib.Analysis.Analytic.OfScalars
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) 0 0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0

Tactic:
rw [ofScalars, hc, zero_smul 𝕜 (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin, zero_smul, FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Analytic.OfScalars
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
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E c : FormalMultilinearSeries 𝕜 E E)
      (0 : FormalMultilinearSeries 𝕜 E E) ↔
    c = 0

Tactic:
simp [FormalMultilinearSeries.ext_iff, funext_iff]

Premises used: funext_iff, FormalMultilinearSeries.ext_iff
-- Module: Mathlib.Analysis.Analytic.OfScalars
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
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E 0 : FormalMultilinearSeries 𝕜 E E)
    (0 : FormalMultilinearSeries 𝕜 E E)

Tactic:
simp [FormalMultilinearSeries.ext_iff]

Premises used: FormalMultilinearSeries.ext_iff
-- Module: Mathlib.Analysis.Analytic.OfScalars
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
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)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E c : FormalMultilinearSeries 𝕜 E E)
    (0 : FormalMultilinearSeries 𝕜 E E)

Tactic:
simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff]

Premises used: FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars, ContinuousMultilinearMap.ext_iff
-- Module: Mathlib.Analysis.Analytic.OfScalars
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
⊢ ∀ (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:
fun _ _ ↦ Subsingleton.allEq _ _

Premises used: ContinuousMultilinearMap.mkPiAlgebraFin, Subsingleton.allEq, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.OfScalars
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
⊢ ∀ (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:
exact fun _ _ ↦ Subsingleton.allEq _ _

Premises used: Subsingleton.allEq
-- Module: Mathlib.Analysis.Analytic.OfScalars
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₂ : ℕ → 𝕜⦄,
    Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E a₁ : FormalMultilinearSeries 𝕜 E E)
        (ofScalars E a₂ : FormalMultilinearSeries 𝕜 E E) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : ℕ → 𝕜⦄,
    Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E a₁ : FormalMultilinearSeries 𝕜 E E)
        (ofScalars E a₂ : FormalMultilinearSeries 𝕜 E E) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.Analysis.Analytic.OfScalars
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)
h₁ : ∀ (n : ℕ), a₁ n = a₂ n
⊢ a₁ = a₂

Tactic:
ext n
-- Module: Mathlib.Analysis.Analytic.OfScalars
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)
n : ℕ
⊢ a₁ n = a₂ n

Tactic:
simpa [ofScalars] using congrArg (fun p ↦ p n fun _ ↦ (1 : E)) h

Premises used: congrArg, FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Analytic.OfScalars
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
c' : ℕ → 𝕜
⊢ Eq (α := FormalMultilinearSeries 𝕜 E E) (ofScalars E c : FormalMultilinearSeries 𝕜 E E)
      (ofScalars E c' : FormalMultilinearSeries 𝕜 E E) ↔
    c = c'

Tactic:
⟨fun e => ofScalars_series_injective 𝕜 E e, _root_.congrArg _⟩

Premises used: congrArg, Iff.intro, FormalMultilinearSeries.ofScalars_series_injective
-- Module: Mathlib.Analysis.Analytic.OfScalars
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 : ℕ
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)
⊢ 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)

Tactic:
rw [ofScalars]

Premises used: FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Analytic.OfScalars
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)
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)
⊢ 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:
cases n
-- Module: Mathlib.Analysis.Analytic.OfScalars
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 (α := 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:
simp
-- Module: Mathlib.Analysis.Analytic.OfScalars
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 + 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:
simp
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_3
inst : NontriviallyNormedField 𝕜
p : ℕ → 𝕜
n : ℕ
⊢ coeff (𝕜 := 𝕜) (ofScalars 𝕜 p) n = p n

Tactic:
simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]

Premises used: FormalMultilinearSeries.coeff, List.prod_ofFn, FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Analytic.OfScalars
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' : ℕ → 𝕜
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)
⊢ ofScalars E (c + c') =
    HAdd.hAdd (α := FormalMultilinearSeries 𝕜 E E) (β := FormalMultilinearSeries 𝕜 E E)
      (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (ofScalars E c' : FormalMultilinearSeries 𝕜 E E)

Tactic:
ext