awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ Injective (α := Fin (c.partSize (c.index j))) (c.emb (c.index j))

Tactic:
(c.emb_strictMono (c.index j)).injective

Premises used: OrderedFinpartition.index, StrictMono.injective, OrderedFinpartition.emb_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ Injective (α := Fin (c.partSize (c.index j))) (c.emb (c.index j))

Tactic:
exact (c.emb_strictMono (c.index j)).injective

Premises used: OrderedFinpartition.index, StrictMono.injective, OrderedFinpartition.emb_strictMono
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
neg :
  Eq.{u_3 + 1} (α := F)
    ((p m : (a : (i : Fin (c.partSize m)) → E) → F) (update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb m) : F)
    ((p m : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m) : F)
⊢ c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) (c.index j)
      ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))
      m

Tactic:
simp only [applyOrderedFinpartition, ne_eq, h, not_false_eq_true,
      update_of_ne]

Premises used: ne_eq, OrderedFinpartition.applyOrderedFinpartition, not_false_eq_true, Function.update_of_ne
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
neg : update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb m = v ∘ c.emb m
⊢ Eq.{u_3 + 1} (α := F)
    ((p m : (a : (i : Fin (c.partSize m)) → E) → F) (update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb m) : F)
    ((p m : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m) : F)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
neg : j ∉ range (c.emb m)
⊢ update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb m = v ∘ c.emb m

Tactic:
apply Function.update_comp_eq_of_notMem_range

Premises used: Function.update_comp_eq_of_notMem_range
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ Disjoint (range (c.emb m)) (range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j)))

Tactic:
have A : Disjoint (range (c.emb m)) (range (c.emb (c.index j))) :=
      c.disjoint (mem_univ m) (mem_univ (c.index j)) h
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j)))
⊢ c.emb (c.index j) (c.invEmbedding j) = j

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j)))
⊢ j ∈ range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j))

Tactic:
have : j ∈ range (c.emb (c.index j)) := mem_range.2 ⟨c.invEmbedding j, by simp⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j)))
this : j ∈ range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j))
⊢ j ∉ range (c.emb m)

Tactic:
Set.disjoint_right.1 A this

Premises used: Set.disjoint_right, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
A : Disjoint (range (c.emb m)) (range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j)))
this : j ∈ range (ι := Fin (c.partSize (c.index j))) (c.emb (c.index j))
⊢ j ∉ range (c.emb m)

Tactic:
exact Set.disjoint_right.1 A this

Premises used: Set.disjoint_right, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
h :
  ∀ (d : Fin c.length),
    c.applyOrderedFinpartition
        (update (β := fun (i : Fin c.length) ↦
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
        v d =
      update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
        ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) d
⊢ c.applyOrderedFinpartition
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
      v =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
      ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m))

Tactic:
ext d
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
d : Fin c.length
pos :
  ∀ (h : d = m),
    c.applyOrderedFinpartition
        (update (β := fun (i : Fin c.length) ↦
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
        v d =
      update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
        ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) d
neg :
  ∀ (h : ¬d = m),
    c.applyOrderedFinpartition
        (update (β := fun (i : Fin c.length) ↦
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
        v d =
      update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
        ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) d
⊢ c.applyOrderedFinpartition
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
      v d =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
      ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) d

Tactic:
by_cases h : d = m
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
d : Fin c.length
h : d = m
pos :
  c.applyOrderedFinpartition
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
      v m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
      ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) m
⊢ c.applyOrderedFinpartition
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
      v d =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
      ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) d

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
d : Fin c.length
h : d = m
⊢ c.applyOrderedFinpartition
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
      v m =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
      ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) m

Tactic:
simp [applyOrderedFinpartition]

Premises used: OrderedFinpartition.applyOrderedFinpartition
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
m : Fin c.length
v : Fin n → E
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
d : Fin c.length
h : ¬d = m
⊢ c.applyOrderedFinpartition
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m q)
      v d =
    update (β := fun (a : Fin c.length) ↦ F) (c.applyOrderedFinpartition p v) m
      ((q : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)) d

Tactic:
simp [h, applyOrderedFinpartition]

Premises used: OrderedFinpartition.applyOrderedFinpartition
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
v : (i : Fin n) → E
i : Fin n
x y : E
⊢ (fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v) : G))
      (update (β := fun (i : Fin n) ↦ E) v i (x + y)) =
    HAdd.hAdd (α := G)
      ((fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v) : G))
        (update (β := fun (i : Fin n) ↦ E) v i x))
      ((fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v) : G))
        (update (β := fun (i : Fin n) ↦ E) v i y))

Tactic:
simp only [applyOrderedFinpartition_update_right,
          ContinuousMultilinearMap.map_update_add]

Premises used: ContinuousMultilinearMap.map_update_add, OrderedFinpartition.applyOrderedFinpartition_update_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c_1.length) ↦ F) G
p : (i : Fin c_1.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c_1.partSize i)) ↦ E) F
v : (i : Fin n) → E
i : Fin n
c : 𝕜
x : E
⊢ (fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c_1.length) → F) → G) (c_1.applyOrderedFinpartition p v) : G))
      (update (β := fun (i : Fin n) ↦ E) v i (c • x)) =
    HSMul.hSMul (β := G) c
      ((fun (v : (i : Fin n) → E) ↦ ((f : (a : (i : Fin c_1.length) → F) → G) (c_1.applyOrderedFinpartition p v) : G))
        (update (β := fun (i : Fin n) ↦ E) v i x))

Tactic:
simp only [applyOrderedFinpartition_update_right,
          ContinuousMultilinearMap.map_update_smul]

Premises used: ContinuousMultilinearMap.map_update_smul, OrderedFinpartition.applyOrderedFinpartition_update_right
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
apply : Continuous (c.applyOrderedFinpartition p)
⊢ Continuous.{u_2, u_4} (X := (i : Fin n) → E) (Y := G)
    (MultilinearMap.toFun.{u_1, 0, u_2, u_4} (R := 𝕜) (M₁ := fun (i : Fin n) ↦ E)
      (MultilinearMap.mk' (M₁ := fun (i : Fin n) ↦ E)
        (fun (v : (i : Fin n) → E) ↦ (f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v)) ⋯ ⋯))

Tactic:
apply f.cont.comp

Premises used: Continuous.comp, ContinuousMultilinearMap.cont
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
change :
  Continuous.{u_2, u_3} (Y := (m : Fin c.length) → F) fun (v : Fin n → E) (m : Fin c.length) ↦
    (p m : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)
⊢ Continuous (c.applyOrderedFinpartition p)

Tactic:
change Continuous (fun v m ↦ p m (v ∘ c.emb m))

Premises used: Continuous, OrderedFinpartition.emb, Function.comp, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p_1 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
⊢ Continuous.{u_2, u_3} (Y := (m : Fin c.length) → F) fun (v : Fin n → E) (m : Fin c.length) ↦
    (p m : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
v : Fin n → E
⊢ Eq.{u_4 + 1} (α := G) ((c.compAlongOrderedFinpartition f p : (a : (i : Fin n) → E) → G) v : G)
    ((f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
⊢ 0 ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
refine :
  ∀ (v : (i : Fin n) → E),
    norm.{u_4} (E := G) ((c.compAlongOrderedFinpartition f p : (a : (i : Fin n) → E) → G) v : G) ≤
      (‖f‖ * ∏ i : Fin c.length, ‖p i‖) * ∏ i : Fin n, ‖v i‖
⊢ ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖

Tactic:
refine ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun v ↦ ?_

Premises used: ContinuousMultilinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
v : (i : Fin n) → E
rw :
  norm.{u_4} (E := G) ((f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v) : G) ≤
    ‖f‖ * ∏ x : Fin c.length, ‖p x‖ * ∏ r : Fin (c.partSize x), ‖v (c.emb x r)‖
⊢ norm.{u_4} (E := G) ((c.compAlongOrderedFinpartition f p : (a : (i : Fin n) → E) → G) v : G) ≤
    (‖f‖ * ∏ i : Fin c.length, ‖p i‖) * ∏ i : Fin n, ‖v i‖

Tactic:
rw [compAlongOrderFinpartition_apply, mul_assoc, ← c.prod_sigma_eq_prod,
    ← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, mul_assoc, OrderedFinpartition.prod_sigma_eq_prod, OrderedFinpartition.compAlongOrderFinpartition_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
v : (i : Fin n) → E
⊢ norm.{u_4} (E := G) ((f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v) : G) ≤
    ‖f‖ * ∏ x : Fin c.length, ‖p x‖ * ∏ r : Fin (c.partSize x), ‖v (c.emb x r)‖

Tactic:
f.le_opNorm_mul_prod_of_le <| c.norm_applyOrderedFinpartition_le _ _

Premises used: OrderedFinpartition.norm_applyOrderedFinpartition_le, ContinuousMultilinearMap.le_opNorm_mul_prod_of_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ
c : OrderedFinpartition n
f : ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G
p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F
v : (i : Fin n) → E
⊢ norm.{u_4} (E := G) ((f : (a : (i : Fin c.length) → F) → G) (c.applyOrderedFinpartition p v) : G) ≤
    ‖f‖ * ∏ x : Fin c.length, ‖p x‖ * ∏ r : Fin (c.partSize x), ‖v (c.emb x r)‖

Tactic:
exact f.le_opNorm_mul_prod_of_le <| c.norm_applyOrderedFinpartition_le _ _

Premises used: OrderedFinpartition.norm_applyOrderedFinpartition_le, ContinuousMultilinearMap.le_opNorm_mul_prod_of_le