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
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_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
⊢ HEq (α :=
    Fin
        (update (β := fun (a : Fin c.length) ↦ ℕ)
          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) + 1)
          i) →
      Fin (n + 1))
    (if h_1 : i = c.index 0 then
      (fun
            (i :
              Fin
                (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                    (c.index 0) +
                  1)) ↦
          cases (motive :=
            fun
              (x :
                Fin
                  (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0) +
                    1)) ↦
            Fin (n + 1)) 0
            (succ ∘
              fun
                (j :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0))) ↦
              (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
            i) ∘
        Fin.cast ⋯
    else
      succ ∘
        (fun
              (j :
                Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
            if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) ∘
          Fin.cast ⋯)
    (c.emb i)

Tactic:
((Fin.heq_fun_iff ?_).mpr ?_).symm

Premises used: Iff.mpr, HEq.symm, Fin.heq_fun_iff
-- 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 : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
⊢ c.partSize i =
    update (β := fun (a : Fin c.length) ↦ ℕ)
      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) + 1) i

Tactic:
simp only [update_self, B, update_idem, update_eq_self]

Premises used: Function.update_eq_self, Function.update_idem, Function.update_self
-- 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 : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
neg :
  c.emb (c.index 0) j =
    cases (motive :=
      fun
        (x :
          Fin
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) +
              1)) ↦
      Fin (n + 1)) 0
      (succ ∘
        fun
          (j :
            Fin
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                (c.index 0))) ↦
        (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
      (Fin.cast ⋯
        (⟨(↑j : ℕ), ⋯⟩ :
          Fin
            (update (β := fun (a : Fin c.length) ↦ ℕ)
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                  (c.index 0) +
                1)
              (c.index 0))))
⊢ c.emb (c.index 0) j =
    (if h_1 : c.index 0 = c.index 0 then
        (fun
              (i :
                Fin
                  (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0) +
                    1)) ↦
            cases (motive :=
              fun
                (x :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0) +
                      1)) ↦
              Fin (n + 1)) 0
              (succ ∘
                fun
                  (j :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0))) ↦
                (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
              i) ∘
          Fin.cast ⋯
      else
        succ ∘
          (fun
                (j :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0))) ↦
              if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
              else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯)
      ⟨(↑j : ℕ), ⋯⟩

Tactic:
simp only [↓reduceDIte, comp_apply]

Premises used: reduceDIte, Function.comp_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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ c.emb (c.index 0) 0 =
    cases (motive :=
      fun
        (x :
          Fin
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) +
              1)) ↦
      Fin (n + 1)) 0
      (succ ∘
        fun
          (j :
            Fin
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                (c.index 0))) ↦
        (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
      (Fin.cast ⋯
        (⟨(↑0 : ℕ), ⋯⟩ :
          Fin
            (update (β := fun (a : Fin c.length) ↦ ℕ)
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                  (c.index 0) +
                1)
              (c.index 0))))

Tactic:
simpa using c.emb_zero

Premises used: OrderedFinpartition.emb_zero
-- 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 : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
⊢ Fin.cast ⋯ j ≠ 0

Tactic:
simpa using hj
-- 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 : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
j' : Fin (c.partSize (c.index 0) - 1) := (Fin.cast ⋯ j).pred ⋯
⊢ j = Fin.cast B j'.succ

Tactic:
simp [j']
-- 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 : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
j' : Fin (c.partSize (c.index 0) - 1) := (Fin.cast ⋯ j).pred ⋯
⊢ j = Fin.cast B j'.succ

Tactic:
have : j = (succ j').cast B := by simp [j']
-- 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 : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
j' : Fin (c.partSize (c.index 0) - 1) := (Fin.cast ⋯ j).pred ⋯
this : j = Fin.cast B j'.succ
neg : c.emb (c.index 0) (Fin.cast B j'.succ) = c.emb (c.index 0) ⟨(↑j' : ℕ) + 1, ⋯⟩
⊢ c.emb (c.index 0) j =
    cases (motive :=
      fun
        (x :
          Fin
            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) +
              1)) ↦
      Fin (n + 1)) 0
      (succ ∘
        fun
          (j :
            Fin
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                (c.index 0))) ↦
        (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
      (Fin.cast ⋯
        (⟨(↑j : ℕ), ⋯⟩ :
          Fin
            (update (β := fun (a : Fin c.length) ↦ ℕ)
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                  (c.index 0) +
                1)
              (c.index 0))))

Tactic:
simp only [this, val_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk,
                succ_pred]

Premises used: Fin.val_succ, Fin.succ_mk, Fin.val_cast, Fin.cast_mk, Function.comp_apply, Fin.cases_succ', Fin.succ_pred
-- 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 : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
j' : Fin (c.partSize (c.index 0) - 1) := (Fin.cast ⋯ j).pred ⋯
this : j = Fin.cast B j'.succ
⊢ c.emb (c.index 0) (Fin.cast B j'.succ) = c.emb (c.index 0) ⟨(↑j' : ℕ) + 1, ⋯⟩

Tactic:
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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n_1 : ℕ
c_1 : OrderedFinpartition n_1
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (ι := Fin (c.partSize 0)) (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
i : Fin c.length
j : Fin (c.partSize i)
hi : i ≠ c.index 0
⊢ c.emb i j =
    (if h_1 : i = c.index 0 then
        (fun
              (i :
                Fin
                  (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                      (c.index 0) +
                    1)) ↦
            cases (motive :=
              fun
                (x :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0) +
                      1)) ↦
              Fin (n + 1)) 0
              (succ ∘
                fun
                  (j :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0))) ↦
                (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
              i) ∘
          Fin.cast ⋯
      else
        succ ∘
          (fun
                (j :
                  Fin
                    (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
              if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) ∘
            Fin.cast ⋯)
      ⟨(↑j : ℕ), ⋯⟩

Tactic:
simp [hi]
-- 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
v : Fin n → E
⊢ c.applyOrderedFinpartition p v = fun (m : Fin c.length) ↦ (p m : (a : (i : Fin (c.partSize m)) → E) → F) (v ∘ c.emb m)

Tactic:
rfl

Premises used: OrderedFinpartition.applyOrderedFinpartition, 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
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
v : Fin n → E
m : Fin c.length
⊢ ‖c.applyOrderedFinpartition p v m‖ ≤ ‖p m‖ * ∏ i : Fin (c.partSize m), ‖v (c.emb m i)‖

Tactic:
(p m).le_opNorm _

Premises used: ContinuousMultilinearMap.le_opNorm, 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
j : Fin n
v : Fin n → E
z : E
h :
  ∀ (m : Fin c.length),
    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
⊢ c.applyOrderedFinpartition p (update (β := fun (a : Fin n) ↦ E) v j z) =
    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))

Tactic:
ext 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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
pos :
  ∀ (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
neg :
  ∀ (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
⊢ 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:
by_cases h : m = c.index j

Premises used: OrderedFinpartition.index
-- 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
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)
⊢ 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:
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
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
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)
⊢ 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:
simp only [applyOrderedFinpartition, update_self]

Premises used: OrderedFinpartition.applyOrderedFinpartition, Function.update_self
-- 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
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
⊢ 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:
congr
-- 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
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))
pos₁ : Injective (α := Fin (c.partSize (c.index j))) (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

Tactic:
rw [← Function.update_comp_eq_of_injective]

Premises used: Function.update_comp_eq_of_injective
-- 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
⊢ 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:
simp