awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' : ℕ → 𝕜
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:
simp [ofScalars, add_smul]

Premises used: add_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 c' : ℕ → 𝕜
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)
⊢ ofScalars E (c - c') =
    HSub.hSub (α := FormalMultilinearSeries 𝕜 E E) (β := FormalMultilinearSeries 𝕜 E E)
      (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (ofScalars E c' : FormalMultilinearSeries 𝕜 E E)

Tactic:
ext
-- 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' : ℕ → 𝕜
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:
simp [ofScalars, sub_smul]

Premises used: sub_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 : ℕ → 𝕜
x : 𝕜
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)
⊢ ofScalars E (x • c) =
    HSMul.hSMul (β := FormalMultilinearSeries 𝕜 E E) x (ofScalars E c : FormalMultilinearSeries 𝕜 E E)

Tactic:
ext
-- 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 : ℕ → 𝕜
x : 𝕜
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:
simp [ofScalars, smul_smul]

Premises used: smul_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 : ℕ → 𝕜
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)
⊢ 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)

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
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)
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)
⊢ 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)

Premises used: Nat.even_or_odd
-- 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 : ℕ
x : (i : Fin n) → E
h : Even n
⊢ Eq (α := (a : E) → E) (⇑(-ContinuousLinearMap.id 𝕜 E) : (a : E) → E) Neg.neg

Tactic:
rfl
-- 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 : ℕ
x : (i : Fin n) → E
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:
simp [ofScalars, show ((-ContinuousLinearMap.id 𝕜 E : _) : E → E) = Neg.neg by rfl,
    ← List.map_ofFn, h.neg_one_pow]

Premises used: Even.neg_one_pow, List.map_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 : ℕ → 𝕜
n : ℕ
x : (i : Fin n) → E
h : Odd n
⊢ Eq (α := (a : E) → E) (⇑(-ContinuousLinearMap.id 𝕜 E) : (a : E) → E) Neg.neg

Tactic:
rfl
-- 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 : ℕ
x : (i : Fin n) → E
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:
simp [ofScalars, show ((-ContinuousLinearMap.id 𝕜 E : _) : E → E) = Neg.neg by rfl,
    ← List.map_ofFn, h.neg_one_pow]

Premises used: List.map_ofFn, FormalMultilinearSeries.ofScalars, Odd.neg_one_pow
-- 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 : ℕ → 𝕜
f : E →L[𝕜] E
lhs : (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-f) : FormalMultilinearSeries 𝕜 E 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)

Tactic:
lhs
-- 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 : ℕ → 𝕜
f : E →L[𝕜] E
rw :
  (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) :
    FormalMultilinearSeries 𝕜 E E)
| (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) (-f) : FormalMultilinearSeries 𝕜 E E)

Tactic:
rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]

Premises used: ContinuousLinearMap.neg_comp, ContinuousLinearMap.id_comp
-- 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 : ℕ → 𝕜
f : E →L[𝕜] E
rw :
  (compContinuousLinearMap (ofScalars E c : FormalMultilinearSeries 𝕜 E E) ((-ContinuousLinearMap.id 𝕜 E) ∘SL f) :
    FormalMultilinearSeries 𝕜 E 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)

Tactic:
lhs; rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]

Premises used: ContinuousLinearMap.neg_comp, ContinuousLinearMap.id_comp
-- 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 : ℕ → 𝕜
f : E →L[𝕜] E
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)
⊢ 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)

Tactic:
conv => lhs; rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]

Premises used: ContinuousLinearMap.neg_comp, ContinuousLinearMap.id_comp
-- 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 : ℕ → 𝕜
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)
rw₁ 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)
⊢ 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:
rw [← FormalMultilinearSeries.compContinuousLinearMap_comp, ofScalars_comp_neg_id]

Premises used: FormalMultilinearSeries.ofScalars_comp_neg_id, FormalMultilinearSeries.compContinuousLinearMap_comp
-- 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 : ℕ → 𝕜
x : E
n : ℕ
⊢ ((ofScalars E c n : (a : (i : Fin n) → E) → E) fun (x_1 : Fin n) ↦ x) = c n • x ^ n

Tactic:
simp [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 : ℕ → 𝕜
x : E
⊢ Eq.{u_2 + 1} (α := (n : ℕ) → E) (fun (n : ℕ) ↦ (ofScalars E c n : (a : (i : Fin n) → E) → E) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦ c n • x ^ n

Tactic:
simp [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 : ℕ → 𝕜
x : E
⊢ ofScalarsSum c x = ∑' (n : ℕ), c n • x ^ n

Tactic:
tsum_congr fun n => ofScalars_apply_eq c x n

Premises used: FormalMultilinearSeries.ofScalars_apply_eq, tsum_congr, FormalMultilinearSeries.ofScalarsSum, FormalMultilinearSeries.sum
-- 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.{u_2 + 1} (α := (x : E) → E) (ofScalarsSum c) fun (x : E) ↦ ∑' (n : ℕ), c n • x ^ n

Tactic:
funext (ofScalars_sum_eq c)

Premises used: funext, FormalMultilinearSeries.ofScalars_sum_eq
-- 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 : ℕ → 𝕜
⊢ ofScalarsSum c 0 = HSMul.hSMul (β := E) (c 0) 1

Tactic:
simp [ofScalarsSum_eq_tsum, ← ofScalars_apply_eq, ofScalars_apply_zero]

Premises used: FormalMultilinearSeries.ofScalars_apply_eq, FormalMultilinearSeries.ofScalars_apply_zero, FormalMultilinearSeries.ofScalarsSum_eq_tsum
-- 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
x : E
⊢ ofScalarsSum c x = 0

Tactic:
simp [Subsingleton.eq_zero x, Subsingleton.eq_zero (1 : E)]

Premises used: Subsingleton.eq_zero, 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 : T2Space E
x : E
⊢ ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x)

Tactic:
simp [ofScalars_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Premises used: MulOpposite.op_pow, MulOpposite.op_smul, FormalMultilinearSeries.ofScalars_sum_eq, tsum_op
-- 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 : T2Space E
x : Eᵐᵒᵖ
⊢ ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x)

Tactic:
simp [ofScalars_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]

Premises used: MulOpposite.unop_smul, MulOpposite.unop_pow, tsum_unop, FormalMultilinearSeries.ofScalars_sum_eq
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
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)
rw₁ rw₂ :
  ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
⊢ 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)

Tactic:
rw [ofScalars, norm_smul]

Premises used: norm_smul, FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
simp :
  ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) ≤
    ‖c n‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) ≤ ‖c n‖

Tactic:
simp only [ofScalars_norm_eq_mul]

Premises used: FormalMultilinearSeries.ofScalars_norm_eq_mul
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
⊢ ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) ≤
    ‖c n‖

Tactic:
(mul_le_of_le_one_right (norm_nonneg _)
    (ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos hn))

Premises used: mul_le_of_le_one_right, ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos, norm_nonneg
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
⊢ ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) ≤
    ‖c n‖

Tactic:
exact (mul_le_of_le_one_right (norm_nonneg _)
    (ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos hn))

Premises used: mul_le_of_le_one_right, ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos, norm_nonneg
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
inst_3 : NormOneClass E
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) = ‖c n‖

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
simp_rw : Tendsto (fun (n : ℕ) ↦ ‖c (n + 1)‖ / ‖c n‖ * (↑r' : ℝ)) atTop (𝓝 (↑(r' * r) : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))

Tactic:
simp_rw [norm_mul, norm_norm, mul_div_mul_comm, ← norm_div, pow_succ, mul_div_right_comm,
    div_self (pow_ne_zero _ (NNReal.coe_ne_zero.mpr hr')), one_mul, norm_div, NNReal.norm_eq]

Premises used: Iff.mpr, pow_succ, pow_ne_zero, norm_mul, norm_norm, mul_div_right_comm, norm_div, mul_div_mul_comm, NNReal.coe_ne_zero, one_mul, div_self, NNReal.norm_eq
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ ‖c (n + 1)‖ / ‖c n‖ * (↑r' : ℝ)) atTop (𝓝 (↑(r' * r) : ℝ))

Tactic:
mul_comm r' r ▸ hc.mul tendsto_const_nhds

Premises used: tendsto_const_nhds, Eq.rec, Filter.Tendsto.mul, mul_comm, Eq.symm
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ ‖c (n + 1)‖ / ‖c n‖ * (↑r' : ℝ)) atTop (𝓝 (↑(r' * r) : ℝ))

Tactic:
exact mul_comm r' r ▸ hc.mul tendsto_const_nhds
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
⊢ (↑r⁻¹ : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)

Tactic:
le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
refine :
  ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < (↑r⁻¹ : ℝ≥0∞)),
    (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
⊢ (↑r⁻¹ : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)

Tactic:
refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < (↑r⁻¹ : ℝ≥0∞)
⊢ r' * r < 1

Tactic:
rw [coe_lt_coe, NNReal.lt_inv_iff_mul_lt hr] at hr'

Premises used: ENNReal.coe_lt_coe, NNReal.lt_inv_iff_mul_lt
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
pos : ∀ (hrz : r' = 0), (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
neg : ∀ (hrz : ¬r' = 0), (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
⊢ (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)

Tactic:
by_cases hrz : r' = 0
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : r' = 0
⊢ (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)

Tactic:
simp [hrz]
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
neg :
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
⊢ (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)

Tactic:
apply FormalMultilinearSeries.le_radius_of_summable_norm

Premises used: FormalMultilinearSeries.le_radius_of_summable_norm
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n

Tactic:
Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_

Premises used: Summable.of_norm_bounded_eventually