awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : (i : Fin n) → E
⊢ Eq.{u_4 + 1} (α := G)
    (∑ x : Composition n, (q.removeZero x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))
    (∑ x : Composition n, (q x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))

Tactic:
Finset.sum_congr rfl fun c _hc => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : (i : Fin n) → E
H :
  ∀ (c : Composition n) (_hc : Membership.mem (γ := Finset (Composition n)) Finset.univ c),
    Eq.{u_4 + 1} (α := G) ((q.removeZero c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
      ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
⊢ Eq.{u_4 + 1} (α := G)
    (∑ x : Composition n, (q.removeZero x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))
    (∑ x : Composition n, (q x.length : (a : (i : Fin x.length) → F) → G) (p.applyComposition x v))

Tactic:
refine Finset.sum_congr rfl fun c _hc => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : 0 < n
v : (i : Fin n) → E
c : Composition n
_hc : Membership.mem (γ := Finset (Composition n)) Finset.univ c
H H₁ :
  Eq.{u_4 + 1} (α := G) ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
    ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
⊢ Eq.{u_4 + 1} (α := G) ((q.removeZero c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)
    ((q c.length : (a : (i : Fin c.length) → F) → G) (p.applyComposition c v) : G)

Tactic:
rw [removeZero_of_pos _ (c.length_pos_of_pos hn)]

Premises used: FormalMultilinearSeries.removeZero_of_pos, Composition.length_pos_of_pos
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
h :
  ∀ (n : ℕ) (x : (i : Fin n) → E),
    Eq.{u_4 + 1} (α := G) ((q.comp p.removeZero n : (a : (i : Fin n) → E) → G) x : G)
      ((q.comp p n : (a : (i : Fin n) → E) → G) x : G)
⊢ Eq (α := FormalMultilinearSeries 𝕜 E G) (q.comp p.removeZero : FormalMultilinearSeries 𝕜 E G)
    (q.comp p : FormalMultilinearSeries 𝕜 E G)

Tactic:
ext n
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
inst_6 : Module 𝕜 G
inst_7 : TopologicalSpace E
inst_8 : TopologicalSpace F
inst_9 : TopologicalSpace G
inst_10 : IsTopologicalAddGroup E
inst_11 : ContinuousConstSMul 𝕜 E
inst_12 : IsTopologicalAddGroup F
inst_13 : ContinuousConstSMul 𝕜 F
inst_14 : IsTopologicalAddGroup G
inst_15 : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : (i : Fin n) → E
⊢ Eq.{u_4 + 1} (α := G) ((q.comp p.removeZero n : (a : (i : Fin n) → E) → G) x : G)
    ((q.comp p n : (a : (i : Fin n) → E) → G) x : G)

Tactic:
simp [FormalMultilinearSeries.comp]

Premises used: FormalMultilinearSeries.comp
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
v : Fin n → E
hbc :
  ∀ (i : Fin c.length),
    Membership.mem (γ := Finset (Fin c.length)) Finset.univ i →
      ‖p.applyComposition c v i‖ ≤
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i)) *
          ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
⊢ ‖f‖ * ∏ i : Fin c.length, ‖p.applyComposition c v i‖ ≤
    ‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i)) *
          ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖

Tactic:
gcongr with i
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
v : Fin n → E
i : Fin c.length
h : Membership.mem (γ := Finset (Fin c.length)) Finset.univ i
⊢ ‖p.applyComposition c v i‖ ≤
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
        (p (c.blocksFun i)) *
      ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖

Tactic:
apply ContinuousMultilinearMap.le_opNorm

Premises used: ContinuousMultilinearMap.le_opNorm
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
v : Fin n → E
rw :
  ‖f‖ *
      HMul.hMul (α := ℝ)
        (∏ x : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
            (p (c.blocksFun x)))
        (∏ x : Fin c.length,
          ∏ j : Fin (c.blocksFun x), ‖(v ∘ (⇑(c.embedding x) : (a : Fin (c.blocksFun x)) → Fin n)) j‖) =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖
rw₁ rw₂ :
  ‖f‖ *
      HMul.hMul (α := ℝ)
        (∏ x : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
            (p (c.blocksFun x)))
        (∏ x : Fin c.length,
          ∏ j : Fin (c.blocksFun x), ‖(v ∘ (⇑(c.embedding x) : (a : Fin (c.blocksFun x)) → Fin n)) j‖) =
    ‖f‖ *
      HMul.hMul (α := ℝ)
        (∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i)))
        (∏ i : Fin c.length,
          ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖)
⊢ ‖f‖ *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i)) *
          ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖

Tactic:
rw [Finset.prod_mul_distrib, mul_assoc]

Premises used: Finset.prod_mul_distrib, mul_assoc
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
v : Fin n → E
rw :
  (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ a : Fin c.length,
        ∏ s : Fin (c.blocksFun a),
          ‖v
              ((c.blocksFinEquiv : (a : (i : Fin c.length) × Fin (c.blocksFun i)) → Fin n)
                (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) a s))‖
⊢ (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin n, ‖v i‖

Tactic:
rw [← c.blocksFinEquiv.prod_comp, ← Finset.univ_sigma_univ, Finset.prod_sigma]

Premises used: Composition.blocksFinEquiv, Finset.prod_sigma, Finset.univ_sigma_univ, Equiv.prod_comp
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
v : Fin n → E
⊢ (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ i : Fin c.length, ∏ j : Fin (c.blocksFun i), ‖(v ∘ (⇑(c.embedding i) : (a : Fin (c.blocksFun i)) → Fin n)) j‖ =
    (‖f‖ *
        ∏ i : Fin c.length,
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
            (p (c.blocksFun i))) *
      ∏ a : Fin c.length,
        ∏ s : Fin (c.blocksFun a),
          ‖v
              ((c.blocksFinEquiv : (a : (i : Fin c.length) × Fin (c.blocksFun i)) → Fin n)
                (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.blocksFun i)) a s))‖

Tactic:
congr
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ 0 ≤
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
      ∏ i : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
          (p (c.blocksFun i))

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
push_cast :
  ‖q.compAlongComposition p c‖ ≤
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
      ∏ x : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
          (p (c.blocksFun x))
⊢ (↑‖q.compAlongComposition p c‖₊ : ℝ) ≤
    (↑(nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
          ∏ i : Fin c.length,
            nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun i)) ↦ E) F)
              (p (c.blocksFun i))) :
      ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ‖q.compAlongComposition p c‖ ≤
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
      ∏ x : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
          (p (c.blocksFun x))

Tactic:
q.compAlongComposition_norm p c

Premises used: FormalMultilinearSeries.compAlongComposition_norm
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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
n : ℕ
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
c : Composition n
⊢ ‖q.compAlongComposition p c‖ ≤
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G) (q c.length) *
      ∏ x : Fin c.length,
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.blocksFun x)) ↦ E) F)
          (p (c.blocksFun x))

Tactic:
exact q.compAlongComposition_norm p c

Premises used: FormalMultilinearSeries.compAlongComposition_norm
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
v : Fin 0 → E
⊢ (id 𝕜 E x 0 : (a : (i : Fin 0) → E) → E) v = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
v : Fin 1 → E
⊢ (id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) v = v 0

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
h : n = 1
v : Fin n → E
subst : ∀ (v : Fin 1 → E), (id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) v = v (⟨0, ⋯⟩ : Fin 1)
⊢ (id 𝕜 E x n : (a : (i : Fin n) → E) → E) v = v (⟨0, ⋯⟩ : Fin n)

Tactic:
subst n
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
v : Fin 1 → E
⊢ (id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) v = v (⟨0, ⋯⟩ : Fin 1)

Tactic:
apply id_apply_one

Premises used: FormalMultilinearSeries.id_apply_one
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
h : LT.lt (α := ℕ) 1 0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E) E) (id 𝕜 E x 0) 0

Tactic:
contradiction
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
h : LT.lt (α := ℕ) 1 1
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) E) (id 𝕜 E x 1) 0

Tactic:
contradiction
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n_1 n : ℕ
h : 1 < n + 2
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 2)) ↦ E) E) (id 𝕜 E x (n + 2)) 0

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
h : 1 < n
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (id 𝕜 E x n) 0

Tactic:
match n with
    | 0 => contradiction
    | 1 => contradiction
    | n + 2 => rfl
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : ∀ (n : ℕ), p.comp (id 𝕜 E x) n = p n
⊢ p.comp (id 𝕜 E x) = p

Tactic:
ext1 n
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
h : p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n
h₁ :
  ∀ (b : Composition n),
    Membership.mem (γ := Finset (Composition n)) Finset.univ b →
      b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E x) b = 0
h₂ : Composition.ones n ∉ Finset.univ → p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = 0
⊢ ∑ c : Composition n, p.compAlongComposition (id 𝕜 E x) c = p n

Tactic:
rw [Finset.sum_eq_single (Composition.ones n)]

Premises used: Finset.sum_eq_single, Composition.ones
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
h :
  ∀ (v : (i : Fin n) → E),
    Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) (Composition.ones n) : (a : (i : Fin n) → E) → F) v : F)
      ((p n : (a : (i : Fin n) → E) → F) v : F)
⊢ p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n

Tactic:
ext v
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
h :
  Eq.{u_3 + 1} (α := F)
    ((p (Composition.ones n).length : (a : (i : Fin (Composition.ones n).length) → E) → F)
        (applyComposition (id 𝕜 E x) (Composition.ones n) v) :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F) ((p.compAlongComposition (id 𝕜 E x) (Composition.ones n) : (a : (i : Fin n) → E) → F) v : F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)

Tactic:
rw [compAlongComposition_apply]

Premises used: FormalMultilinearSeries.compAlongComposition_apply
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
h :
  ∀ (i : ℕ) (him : i < (Composition.ones n).length) (hin : i < n),
    applyComposition (id 𝕜 E x) (Composition.ones n) v (⟨i, him⟩ : Fin (Composition.ones n).length) = v ⟨i, hin⟩
⊢ Eq.{u_3 + 1} (α := F)
    ((p (Composition.ones n).length : (a : (i : Fin (Composition.ones n).length) → E) → F)
        (applyComposition (id 𝕜 E x) (Composition.ones n) v) :
      F)
    ((p n : (a : (i : Fin n) → E) → F) v : F)

Tactic:
apply p.congr (Composition.ones_length n)

Premises used: FormalMultilinearSeries.congr, Composition.ones_length
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
h :
  (fun (v : Fin n → E) (i : Fin (Composition.ones n).length) ↦
        ((id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ i) : E))
      v ⟨i, him⟩ =
    v (⟨i, hin⟩ : Fin n)
⊢ applyComposition (id 𝕜 E x) (Composition.ones n) v (⟨i, him⟩ : Fin (Composition.ones n).length) = v ⟨i, hin⟩

Tactic:
rw [applyComposition_ones]

Premises used: FormalMultilinearSeries.applyComposition_ones
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
⊢ (fun (v : Fin n → E) (i : Fin (Composition.ones n).length) ↦
        ((id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ i) : E))
      v ⟨i, him⟩ =
    v (⟨i, hin⟩ : Fin n)

Tactic:
congr_arg v ?_

Premises used: congr_arg
-- Module: Mathlib.Analysis.Analytic.Composition
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
v : (i : Fin n) → E
i : ℕ
him : i < (Composition.ones n).length
hin : i < n
h : Fin.castLE ⋯ (⟨i, him⟩ : Fin (Composition.ones n).length) = ⟨i, hin⟩
⊢ (fun (v : Fin n → E) (i : Fin (Composition.ones n).length) ↦
        ((id 𝕜 E x 1 : (a : (i : Fin 1) → E) → E) fun (x : Fin 1) ↦ v (Fin.castLE ⋯ i) : E))
      v ⟨i, him⟩ =
    v (⟨i, hin⟩ : Fin n)

Tactic:
refine congr_arg v ?_

Premises used: congr_arg