awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
this : Fintype ι
rw :
  (∀ (i : ι),
      Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦
        ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiable_iff, differentiable_pi]

Premises used: differentiable_pi, ContinuousLinearEquiv.comp_differentiable_iff, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
this : Fintype ι
⊢ (∀ (i : ι),
      Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦
        ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable.{u_1, u_4, u_3} 𝕜 (F := E i) fun (x : H) ↦ (f x).ofLp i

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
have :
  ∀ (this : Fintype ι),
    HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
⊢ HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
this : Fintype ι
rw :
  (∀ (i : ι),
      HasStrictFDerivAt (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i)
        (comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := E) i)
          ((↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) ∘SL f'))
        y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
⊢ HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasStrictFDerivAt_iff, hasStrictFDerivAt_pi']

Premises used: hasStrictFDerivAt_pi', PiLp.continuousLinearEquiv, ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      HasStrictFDerivAt (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i)
        (comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := E) i)
          ((↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) ∘SL f'))
        y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
have :
  ∀ (this : Fintype ι),
    HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
⊢ HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
this : Fintype ι
rw :
  (∀ (i : ι),
      HasFDerivWithinAt (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i)
        (comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := E) i)
          ((↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) ∘SL f'))
        t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
⊢ HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasFDerivWithinAt_iff, hasFDerivWithinAt_pi']

Premises used: hasFDerivWithinAt_pi', ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, PiLp.continuousLinearEquiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_4 : NormedSpace 𝕜 H
inst_5 : Finite ι
p : ENNReal
inst_6 : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      HasFDerivWithinAt (fun (x : H) ↦ ((⇑(continuousLinearEquiv p 𝕜 E) : (a : PiLp p E) → (i : ι) → E i) ∘ f) x i)
        (comp (σ₂₃ := RingHom.id 𝕜) (ContinuousLinearMap.proj (φ := E) i)
          ((↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) ∘SL f'))
        t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun (x : H) ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Finite ι
p : ENNReal
inst_4 : Fact (1 ≤ p)
f : PiLp p E
⊢ HasStrictFDerivAt (𝕜 := 𝕜) ofLp (↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) f

Tactic:
have := Fintype.ofFinite ι
  .of_isLittleO <| (Asymptotics.isLittleO_zero _ _).congr_left fun _ => (sub_self _).symm

Premises used: Fintype.ofFinite, sub_self, Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.congr_left, HSub.hSub, nhds, Prod.mk, Prod.fst, HasStrictFDerivAt.of_isLittleO, Eq.symm, WithLp.ofLp, Prod.snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Finite ι
p : ENNReal
inst_4 : Fact (1 ≤ p)
f : (i : ι) → E i
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (toLp p)
    (↑(ContinuousLinearEquiv.symm (continuousLinearEquiv p 𝕜 E)) : ((i : ι) → E i) →L[𝕜] PiLp p E) f

Tactic:
have := Fintype.ofFinite ι
  .of_isLittleO <| (Asymptotics.isLittleO_zero _ _).congr_left fun _ => (sub_self _).symm

Premises used: Fintype.ofFinite, sub_self, Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.congr_left, HSub.hSub, WithLp.toLp, nhds, Prod.mk, Prod.fst, HasStrictFDerivAt.of_isLittleO, Eq.symm, Prod.snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Finite ι
p : ENNReal
inst_4 : Fact (1 ≤ p)
f : PiLp p E
i : ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (fun (f : PiLp p E) ↦ f.ofLp i) (proj p E i) f

Tactic:
have := Fintype.ofFinite ι
  (hasStrictFDerivAt_apply i f).comp f (hasStrictFDerivAt_ofLp (𝕜 := 𝕜) p f)

Premises used: Fintype.ofFinite
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Finite ι
p : ENNReal
inst_4 : Fact (1 ≤ p)
f : PiLp p E
⊢ HasFDerivAt (𝕜 := 𝕜) ofLp (↑(continuousLinearEquiv p 𝕜 E) : PiLp p E →L[𝕜] (i : ι) → E i) f

Tactic:
have := Fintype.ofFinite ι
  (hasStrictFDerivAt_ofLp p f).hasFDerivAt

Premises used: Fintype.ofFinite, HasStrictFDerivAt.hasFDerivAt, PiLp.hasStrictFDerivAt_ofLp
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Finite ι
p : ENNReal
inst_4 : Fact (1 ≤ p)
f : (i : ι) → E i
⊢ HasFDerivAt (𝕜 := 𝕜) (toLp p)
    (↑(ContinuousLinearEquiv.symm (continuousLinearEquiv p 𝕜 E)) : ((i : ι) → E i) →L[𝕜] PiLp p E) f

Tactic:
have := Fintype.ofFinite ι
  (hasStrictFDerivAt_toLp p f).hasFDerivAt

Premises used: Fintype.ofFinite, HasStrictFDerivAt.hasFDerivAt, PiLp.hasStrictFDerivAt_toLp
-- Module: Mathlib.Analysis.Calculus.FDeriv.WithLp
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
inst_3 : Finite ι
p : ENNReal
inst_4 : Fact (1 ≤ p)
f : PiLp p E
i : ι
⊢ HasFDerivAt (𝕜 := 𝕜) (fun (f : PiLp p E) ↦ f.ofLp i) (proj p E i) f

Tactic:
have := Fintype.ofFinite ι
  (hasStrictFDerivAt_apply p f i).hasFDerivAt

Premises used: Fintype.ofFinite, HasStrictFDerivAt.hasFDerivAt, PiLp.hasStrictFDerivAt_apply
-- 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
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n) ↦ E) F) (0 n) 0

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
p q : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ (p + q) n = p n + q n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
𝕜' : 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
inst_11 : Semiring 𝕜'
inst_12 : Module 𝕜' F
inst_13 : ContinuousConstSMul 𝕜' F
inst_14 : SMulCommClass 𝕜 𝕜' F
f : FormalMultilinearSeries 𝕜 E F
n : ℕ
a : 𝕜'
⊢ (a • f) n = a • f n

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
p q : FormalMultilinearSeries 𝕜 E F
h : ∀ (n : ℕ), p n = q n
⊢ p = q

Tactic:
funext h

Premises used: FormalMultilinearSeries, funext
-- 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 q : FormalMultilinearSeries 𝕜 E F
⊢ p ≠ q ↔ ∃ (n : ℕ), p n ≠ q n

Tactic:
Function.ne_iff

Premises used: FormalMultilinearSeries, Function.ne_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
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin 0) ↦ E) F) (p.removeZero 0) 0

Tactic:
rfl

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

Tactic:
rfl

Premises used: FormalMultilinearSeries.removeZero, 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
rw :
  Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n.pred.succ) ↦ E) F) (p.removeZero n.pred.succ)
    (p n.pred.succ)
⊢ p.removeZero n = p n

Tactic:
rw [← Nat.succ_pred_eq_of_pos h]

Premises used: Nat.succ_pred_eq_of_pos
-- 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
n : ℕ
h : 0 < n
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, v, w} 𝕜 (fun (i : Fin n.pred.succ) ↦ E) F) (p.removeZero n.pred.succ)
    (p n.pred.succ)

Tactic:
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
p : FormalMultilinearSeries 𝕜 E F
m n : ℕ
v : Fin m → E
w : Fin n → E
h1 : m = n
h2 : ∀ (i : ℕ) (him : i < m) (hin : i < n), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩
subst :
  ∀ {w : Fin m → E} (h2 : ∀ (i : ℕ) (him hin : i < m), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩),
    Eq.{w + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) v : F) ((p m : (a : (i : Fin m) → E) → F) w : F)
⊢ Eq.{w + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) v : F) ((p n : (a : (i : Fin n) → E) → F) w : F)

Tactic:
subst n
-- 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
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩
h : ∀ (i : ℕ) (hi : i < m), v (⟨i, hi⟩ : Fin m) = w ⟨i, hi⟩
⊢ Eq.{w + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) v : F) ((p m : (a : (i : Fin m) → E) → F) w : F)

Tactic:
congr with ⟨i, hi⟩
-- 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
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩
i : ℕ
hi : i < m
⊢ v (⟨i, hi⟩ : Fin m) = w ⟨i, hi⟩

Tactic:
h2 i hi hi
-- 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
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v (⟨i, him⟩ : Fin m) = w ⟨i, hin⟩
i : ℕ
hi : i < m
⊢ v (⟨i, hi⟩ : Fin m) = w ⟨i, hi⟩

Tactic:
exact h2 i hi hi
-- 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
k l : ℕ
h : k = l
h' subst : p k = 0
⊢ p l = 0

Tactic:
subst h
-- 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
k : ℕ
h' : p k = 0
⊢ p k = 0

Tactic:
h'
-- 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
k : ℕ
h' : p k = 0
⊢ p k = 0

Tactic:
exact h'
-- 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
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
n : ℕ
v : Fin n → E
⊢ Eq.{x + 1} (α := G) ((p.compContinuousLinearMap u n : (a : (i : Fin n) → E) → G) v : G)
    ((p n : (a : (i : Fin n) → F) → G) ((⇑u : (a : E) → F) ∘ v) : 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
p : FormalMultilinearSeries 𝕜 E F
⊢ p.compContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) = p

Tactic:
rfl

Premises used: FormalMultilinearSeries.compContinuousLinearMap, MultilinearMap.compLinearMap, ContinuousMultilinearMap.compContinuousLinearMap, rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
G : Type x
H : Type y
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
inst_16 : AddCommMonoid H
inst_17 : Module 𝕜 H
inst_18 : TopologicalSpace H
inst_19 : ContinuousAdd H
inst_20 : ContinuousConstSMul 𝕜 H
p : FormalMultilinearSeries 𝕜 G H
u₁ : F →L[𝕜] G
u₂ : E →L[𝕜] F
⊢ Eq (α := FormalMultilinearSeries 𝕜 E H) (compContinuousLinearMap (p.compContinuousLinearMap u₁) u₂)
    (p.compContinuousLinearMap (u₁ ∘SL u₂))

Tactic:
rfl

Premises used: FormalMultilinearSeries.compContinuousLinearMap, MultilinearMap.compLinearMap, ContinuousMultilinearMap.compContinuousLinearMap, rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : Ring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
f : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ (-f) n = -f n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries
Goal:
𝕜 : Type u
E : Type v
F : Type w
inst : Ring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousConstSMul 𝕜 F
f g : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ (f - g) n = f n - g n

Tactic:
rfl

Premises used: rfl
-- 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
h : ∀ (n : ℕ), (p.unshift z).shift n = p n
⊢ (p.unshift z).shift = p

Tactic:
ext1 n