awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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
have pos : c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) (c.index j) =
  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))
    (c.index j)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) (c.index j) =
    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))
      (c.index j)
have pos : Eq.{u_3 + 1} (α := F)
  ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
      (update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb (c.index j)) :
    F)
  ((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) :
    F)
Tactic: simp only [applyOrderedFinpartition, update_self]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ Eq.{u_3 + 1} (α := F)
    ((p (c.index j) : (a : (i : Fin (c.partSize (c.index j))) → E) → F)
        (update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb (c.index j)) :
      F)
    ((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) :
      F)
have pos : update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb (c.index j) =
  update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb (c.index j) =
    update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z
have pos : Eq (α := (i : Fin (c.partSize (c.index j))) → E) (update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb (c.index j))
  (update (β := fun (a : Fin n) ↦ E) v (c.emb (c.index j) (c.invEmbedding j)) z ∘ c.emb (c.index j))
Tactic: rw [← Function.update_comp_eq_of_injective]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
pos :
  Eq (α := (i : Fin (c.partSize (c.index j))) → E) (update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb (c.index j))
    (update (β := fun (a : Fin n) ↦ E) v (c.emb (c.index j) (c.invEmbedding j)) z ∘ c.emb (c.index j))
⊢ update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb (c.index j) =
    update (β := fun (i : Fin (c.partSize (c.index j))) ↦ E) (v ∘ c.emb (c.index j)) (c.invEmbedding j) z
have pos₁ : Injective (α := Fin (c.partSize (c.index j))) (c.emb (c.index j))
Tactic: rw [← Function.update_comp_eq_of_injective]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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
have 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)
Tactic: simp only [applyOrderedFinpartition, ne_eq, h, not_false_eq_true,
      update_of_ne]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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)
have neg : update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb m = v ∘ c.emb m
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ update (β := fun (a : Fin n) ↦ E) v j z ∘ c.emb m = v ∘ c.emb m
have neg : j ∉ range (c.emb m)
Tactic: apply Function.update_comp_eq_of_notMem_range
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
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
⊢ j ∉ range (c.emb m)
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
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 (c.emb m)
have this : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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))
have 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
Tactic: ext d
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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
have 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
Tactic: by_cases h : d = m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ 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
have 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
Tactic: by_cases h : d = m
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
have 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
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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_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)) ⋯ ⋯))
have apply : Continuous (c.applyOrderedFinpartition p)
Tactic: apply f.cont.comp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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 (c.applyOrderedFinpartition p)
have 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)
Tactic: change Continuous (fun v m ↦ p m (v ∘ c.emb m))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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
⊢ ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖
have 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‖
Tactic: refine ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun v ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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) ((c.compAlongOrderedFinpartition f p : (a : (i : Fin n) → E) → G) v : G) ≤
    (‖f‖ * ∏ i : Fin c.length, ‖p i‖) * ∏ i : Fin n, ‖v i‖
have 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)‖
Tactic: rw [compAlongOrderFinpartition_apply, mul_assoc, ← c.prod_sigma_eq_prod,
    ← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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_1 : 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
m : Fin c.length
a : 𝕜
q : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize m)) ↦ E) F
⊢ (fun (p : (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
        c.compAlongOrderedFinpartition f p)
      (update (β := fun (i : Fin c.length) ↦
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (a • q)) =
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) a
      ((fun
            (p :
              (i : Fin c.length) → ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
          c.compAlongOrderedFinpartition f p)
        (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))
have H : ∀ (v : (i : Fin n) → E),
  Eq.{u_4 + 1} (α := G)
    (((fun
                (p :
                  (i : Fin c.length) →
                    ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
              c.compAlongOrderedFinpartition f p)
            (update (β := fun (i : Fin c.length) ↦
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) p m (a • q)) :
          (a : (i : Fin n) → E) → G)
        v :
      G)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) a
            ((fun
                  (p :
                    (i : Fin c.length) →
                      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) ↦
                c.compAlongOrderedFinpartition f p)
              (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)) :
          (a : (i : Fin n) → E) → G)
        v :
      G)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
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 : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
⊢ ContinuousMultilinearMap.{u_1, 0, u_3, u_4} 𝕜 (fun (i : Fin c.length) ↦ F) G →L[𝕜]
    ContinuousMultilinearMap 𝕜
      (fun (i : Fin c.length) ↦ ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
have refine : ∀ (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),
  norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
      ((((c.compAlongOrderedFinpartitionₗ :
                  (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) ↦ F) G) →
                    MultilinearMap 𝕜
                      (fun (i : Fin c.length) ↦ ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) G))
                f :
              MultilinearMap 𝕜
                (fun (i : Fin c.length) ↦
                  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F)
                (ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)) :
            (a : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) ↦ E) F) →
              ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) G)
          p :
        ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G) ≤
    1 * ‖f‖ * ∏ i : Fin c.length, ‖p i‖
Tactic: refine MultilinearMap.mkContinuousLinear c.compAlongOrderedFinpartitionₗ 1 fun f p ↦ ?_