awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
n : ℕ
⊢ ContinuousMultilinearMap.curryRight.{u, v, w} (𝕜 := 𝕜) (Ei := fun (i : Fin (n + 1)) ↦ E) (G := F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (p n)) =
    p n

Tactic:
LinearIsometryEquiv.apply_symm_apply (continuousMultilinearCurryRightEquiv' 𝕜 n E F) (p n)

Premises used: LinearIsometryEquiv.apply_symm_apply, MultilinearMap.mkContinuous, continuousMultilinearCurryRightEquiv', ContinuousMultilinearMap.curryRight
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
n : ℕ
⊢ ContinuousMultilinearMap.curryRight.{u, v, w} (𝕜 := 𝕜) (Ei := fun (i : Fin (n + 1)) ↦ E) (G := F)
      ((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n E F) :
          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (E →L[𝕜] F)) →
            ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
        (p n)) =
    p n

Tactic:
exact LinearIsometryEquiv.apply_symm_apply (continuousMultilinearCurryRightEquiv' 𝕜 n E F) (p n)

Premises used: LinearIsometryEquiv.apply_symm_apply, continuousMultilinearCurryRightEquiv'
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
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
inst_11 : AddCommMonoid G
inst_12 : Module 𝕜 G
inst_13 : TopologicalSpace G
inst_14 : ContinuousAdd G
inst_15 : ContinuousConstSMul 𝕜 G
f : F →L[𝕜] G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ f.compFormalMultilinearSeries p n = f.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E) (p n)

Tactic:
rfl

Premises used: ContinuousLinearMap.compFormalMultilinearSeries, rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
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
inst_11 : AddCommMonoid G
inst_12 : Module 𝕜 G
inst_13 : TopologicalSpace G
inst_14 : ContinuousAdd G
inst_15 : ContinuousConstSMul 𝕜 G
f : F →L[𝕜] G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
⊢ Eq.{x + 1} (α := G) ((f.compFormalMultilinearSeries p n : (a : (i : Fin n) → E) → G) v : G)
    ((f : (a : F) → G) ((p n : (a : (i : Fin n) → E) → F) v : F) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
⊢ order.{u, v, w} (𝕜 := 𝕜) (E := E) (F := F) 0 = 0

Tactic:
simp [order]

Premises used: FormalMultilinearSeries.order
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
hp : p.order ≠ 0
h : p = 0
⊢ False

Tactic:
simp [h] at hp
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
inst_11 : DecidablePred fun (n : ℕ) ↦ p n ≠ 0
hp : ∃ (n : ℕ), p n ≠ 0
⊢ (sInf fun (x : ℕ) ↦ p x = 0 → False) =
    Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) (fun (x : ℕ) ↦ p x = 0 → False) n) hp

Tactic:
Nat.sInf_def hp

Premises used: Nat.sInf_def
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
inst_11 : DecidablePred fun (n : ℕ) ↦ p n ≠ 0
hp : ∃ (n : ℕ), p n ≠ 0
⊢ p.order = Nat.find (p := fun (n : ℕ) ↦ p n ≠ 0) hp

Tactic:
convert! Nat.sInf_def hp

Premises used: Nat.sInf_def
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
inst_11 : DecidablePred fun (n : ℕ) ↦ p n ≠ 0
hp : p ≠ 0
⊢ p.order = Nat.find (p := fun (n : ℕ) ↦ p n ≠ 0 n) ⋯

Tactic:
order_eq_find _

Premises used: FormalMultilinearSeries.order_eq_find
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
⊢ p.order = 0 ↔ p = 0 ∨ Ne (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) 0

Tactic:
simpa [order, Nat.sInf_eq_zero, FormalMultilinearSeries.ext_iff, eq_empty_iff_forall_notMem]
    using or_comm

Premises used: Nat.sInf_eq_zero, FormalMultilinearSeries.order, FormalMultilinearSeries.ext_iff, Set.eq_empty_iff_forall_notMem, or_comm
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
hp : p ≠ 0
⊢ p.order = 0 ↔ Ne (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 0) ↦ E) F) (p 0) 0

Tactic:
simp [order_eq_zero_iff', hp]

Premises used: FormalMultilinearSeries.order_eq_zero_iff'
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
hp : p ≠ 0
⊢ Ne (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin p.order) ↦ E) F) (p p.order) 0

Tactic:
Nat.sInf_mem (FormalMultilinearSeries.ne_iff.1 hp)

Premises used: Set.Mem, setOf, FormalMultilinearSeries.order, Nat.sInf_mem, FormalMultilinearSeries.ne_iff, Iff.mp, Not
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
hp : p.order ≠ 0
⊢ Ne (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin p.order) ↦ E) F) (p p.order) 0

Tactic:
apply_order_ne_zero (ne_zero_of_order_ne_zero hp)

Premises used: FormalMultilinearSeries.ne_zero_of_order_ne_zero, FormalMultilinearSeries.apply_order_ne_zero
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : Semiring 𝕜
n : ℕ
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
hp : n < p.order
⊢ p n = 0

Tactic:
by_contra <| Nat.notMem_of_lt_sInf hp

Premises used: Nat.notMem_of_lt_sInf, by_contra
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n) = p n

Tactic:
(p n).mkPiRing_apply_one_eq_self

Premises used: ContinuousMultilinearMap.mkPiRing_apply_one_eq_self, FormalMultilinearSeries.coeff
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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).toMultilinearMap (M₁ := fun (i : Fin n) ↦ 𝕜) : (a : (i : Fin n) → 𝕜) → E) fun (i : Fin n) ↦
      HSMul.hSMul (β := 𝕜) (y i) (1 i)) =
    HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) (∏ i : Fin n, y i)
      (((p n).toMultilinearMap (M₁ := fun (i : Fin n) ↦ 𝕜) : (a : (i : Fin n) → 𝕜) → E) 1 : E)

Tactic:
(p n).toMultilinearMap.map_smul_univ y 1

Premises used: ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_smul_univ, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
h : ∀ (x : Fin n), y x = HSMul.hSMul (β := 𝕜) (y x) (1 x)
⊢ (p n : (a : (i : Fin n) → 𝕜) → E) y = HSMul.hSMul.{u, v, v} (α := 𝕜) (∏ i : Fin n, y i) (p.coeff n)

Tactic:
convert! (p n).toMultilinearMap.map_smul_univ y 1

Premises used: ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_smul_univ, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
x : Fin n
⊢ y x = HSMul.hSMul (β := 𝕜) (y x) (1 x)

Tactic:
simp only [Pi.one_apply, smul_eq_mul, mul_one]

Premises used: Pi.one_apply, smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
rw₁ rw₂ : p.coeff n = 0 ↔ p.coeff n = 0
⊢ p.coeff n = 0 ↔ p n = 0

Tactic:
rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]

Premises used: FormalMultilinearSeries.mkPiRing_coeff_eq, ContinuousMultilinearMap.mkPiRing_eq_zero_iff
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
z : 𝕜
⊢ ((p n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ z) = z ^ n • p.coeff n

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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‖
rw₁ rw₂ : ‖p.coeff n‖ = ‖p.coeff n‖
⊢ ‖p n‖ = ‖p.coeff n‖

Tactic:
rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.norm_mkPiRing]

Premises used: ContinuousMultilinearMap.norm_mkPiRing, FormalMultilinearSeries.mkPiRing_coeff_eq
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
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)
⊢ p.fslope.coeff n = p.coeff (n + 1)

Tactic:
simp only [fslope, coeff, ContinuousMultilinearMap.curryLeft_apply]

Premises used: FormalMultilinearSeries.coeff, ContinuousMultilinearMap.curryLeft_apply, FormalMultilinearSeries.fslope
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
h : Eq.{u + 1} (α := (i : Fin n.succ) → 𝕜) (cons (α := fun (i : Fin (n + 1)) ↦ 𝕜) 1 1) 1
⊢ 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:
congr 1
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ Eq.{u + 1} (α := (i : Fin n.succ) → 𝕜) (cons (α := fun (i : Fin (n + 1)) ↦ 𝕜) 1 1) 1

Tactic:
Fin.cons_self_tail (fun _ => (1 : 𝕜))

Premises used: Fin.cons_self_tail, OfNat.ofNat, Fin.tail
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ Eq.{u + 1} (α := (i : Fin n.succ) → 𝕜) (cons (α := fun (i : Fin (n + 1)) ↦ 𝕜) 1 1) 1

Tactic:
exact Fin.cons_self_tail (fun _ => (1 : 𝕜))

Premises used: Fin.cons_self_tail, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ (fslope^[0] p).coeff n = p.coeff (n + 0)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n 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:
simp [ih, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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)
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))
⊢ (fslope^[k] p).coeff n = p.coeff (n + k)

Tactic:
induction k generalizing p with
  | zero => rfl
  | succ k ih => simp [ih, add_assoc]

Premises used: Fin.succ, add_assoc
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
c : F
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 0) ↦ E) F) (constFormalMultilinearSeries 𝕜 E c 0)
    (ContinuousMultilinearMap.uncurry0 𝕜 E c)

Tactic:
rfl

Premises used: constFormalMultilinearSeries, rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
c : F
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F)
    (constFormalMultilinearSeries 𝕜 E c (n + 1)) 0

Tactic:
rfl

Premises used: constFormalMultilinearSeries, rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
c : F
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n) ↦ E) F) (constFormalMultilinearSeries 𝕜 E c n) 0

Tactic:
Nat.casesOn n (fun hn => (hn rfl).elim) (fun _ _ => rfl) hn

Premises used: Nat.casesOn
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
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)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E F) (constFormalMultilinearSeries 𝕜 E 0 : FormalMultilinearSeries 𝕜 E F)
    (0 : FormalMultilinearSeries 𝕜 E F)

Tactic:
ext n x
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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 :
  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)
⊢ 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:
simp only [FormalMultilinearSeries.zero_apply, ContinuousMultilinearMap.zero_apply,
    constFormalMultilinearSeries]

Premises used: constFormalMultilinearSeries, ContinuousMultilinearMap.zero_apply, FormalMultilinearSeries.zero_apply
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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)
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)
⊢ 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:
induction n
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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
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:
simp only [ContinuousMultilinearMap.uncurry0_apply]

Premises used: ContinuousMultilinearMap.uncurry0_apply
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
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 : ℕ
h :
  ∀ (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:
simp only [constFormalMultilinearSeries.match_1.eq_2, ContinuousMultilinearMap.zero_apply]

Premises used: _private.0.constFormalMultilinearSeries.match_1.eq_2, ContinuousMultilinearMap.zero_apply
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
h :
  ∀ (n : ℕ) (v : (i : Fin n) → E),
    Eq.{x + 1} (α := G) ((p.compContinuousLinearMap 0 n : (a : (i : Fin n) → E) → G) v : G)
      (((constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0) n :
              ContinuousMultilinearMap.{u, 0, v, x} 𝕜 (fun (i : Fin n) ↦ E) G) :
            (a : (i : Fin n) → E) → G)
          v :
        G)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E G) (p.compContinuousLinearMap 0)
    (constFormalMultilinearSeries 𝕜 E ((p 0 : (a : (i : Fin 0) → F) → G) 0))

Tactic:
ext n v