awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  ∀ (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) {n : ℕ} (hn : (↑n : ℕ∞ω) ≤ N),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
        (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
      ∑ p ∈ u.sym n,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∀ (i_1 : ↥((insert i u).sym n)),
    Membership.mem (γ := Finset ↥((insert i u).sym n)) Finset.univ i_1 →
      HMul.hMul (α := ℝ) (↑(↑(↑i_1 : Sym ι n) : Multiset ι).countPerms : ℝ)
          (∏ j ∈ insert i u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
                (fun (i : Fin (Multiset.count j (↑(↑i_1 : Sym ι n) : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(↑i_1 : Sym ι n) : Multiset ι)) (f j) s x)) =
        ((fun (v : Multiset ι) ↦
              HMul.hMul (α := ℝ) (↑v.countPerms : ℝ)
                (∏ j ∈ insert i u,
                  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j v)) ↦ E) A')
                    (iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x))) ∘
            comp (β := Sym ι n) Sym.toMultiset
              (comp (β := ↥((insert i u).sym n)) (Subtype.val (p := fun (x : Sym ι n) ↦ x ∈ (insert i u).sym n))
                (comp (β := (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ))))
                  (⇑(Equiv.symm (Finset.symInsertEquiv hi)) :
                    (a : (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ)))) → ↥((insert i u).sym n))
                  (⇑(Finset.symInsertEquiv hi) :
                    (a : ↥((insert i u).sym n)) → (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ)))))))
          i_1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  ∀ (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) {n : ℕ} (hn : (↑n : ℕ∞ω) ≤ N),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
        (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
      ∑ p ∈ u.sym n,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
insert :
  ∀ (m : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m →
      (↑(n.choose (↑m : ℕ)) : ℝ) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (y : E) ↦ ∏ i ∈ u, f i y) s x) ≤
        ∑ x_1 : ↥(u.sym (n - (↑m : ℕ))),
          HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι).countPerms : ℝ)
            (∏ x_2 ∈ Insert.insert i u,
              norm (E :=
                ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
                  (fun (i : Fin (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))) ↦ E)
                  A')
                (iteratedFDerivWithin 𝕜
                  (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι)) (f x_2) s x))
⊢ LE.le (α := ℝ)
    (∑ i_1 : Fin (n + 1),
      (↑(n.choose (↑i_1 : ℕ)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑i_1 : ℕ)) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (↑i_1 : ℕ) (f i) s x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑i_1 : ℕ))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (n - (↑i_1 : ℕ)) (fun (y : E) ↦ ∏ i ∈ u, f i y) s x))
    (∑ x_1 : Fin (n + 1),
      ∑ x_2 : ↥(u.sym (n - (↑x_1 : ℕ))),
        HMul.hMul (α := ℝ) (↑(↑(Sym.fill i x_1 (↑x_2 : Sym ι (n - (↑x_1 : ℕ)))) : Multiset ι).countPerms : ℝ)
          (∏ x_3 ∈ Insert.insert i u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
                (fun (i : Fin (Multiset.count x_3 (↑(Sym.fill i x_1 (↑x_2 : Sym ι (n - (↑x_1 : ℕ)))) : Multiset ι))) ↦
                  E)
                A')
              (iteratedFDerivWithin 𝕜
                (Multiset.count x_3 (↑(Sym.fill i x_1 (↑x_2 : Sym ι (n - (↑x_1 : ℕ)))) : Multiset ι)) (f x_3) s x)))

Tactic:
gcongr with m _
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  ∀ (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) {n : ℕ} (hn : (↑n : ℕ∞ω) ≤ N),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
        (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
      ∑ p ∈ u.sym n,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
⊢ LE.le (α := ℕ∞ω) (↑(n - (↑m : ℕ)) : ℕ∞ω) (↑n : ℕ∞ω)

Tactic:
exact_mod_cast n.sub_le m

Premises used: Nat.sub_le, Fin.val
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  ∀ (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) {n : ℕ} (hn : (↑n : ℕ∞ω) ≤ N),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
        (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
      ∑ p ∈ u.sym n,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))

Tactic:
specialize IH hf.2 (n := n - m) (le_trans (by exact_mod_cast n.sub_le m) hn)

Premises used: And.right, le_trans
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
IH :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
insert :
  (↑(n.choose (↑m : ℕ)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      ∑ p ∈ u.sym (n - (↑m : ℕ)),
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x)) ≤
    ∑ x_1 : ↥(u.sym (n - (↑m : ℕ))),
      HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι).countPerms : ℝ)
        (∏ x_2 ∈ Insert.insert i u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
              (fun (i : Fin (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))
              (f x_2) s x))
⊢ (↑(n.choose (↑m : ℕ)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
        (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (y : E) ↦ ∏ i ∈ u, f i y) s x) ≤
    ∑ x_1 : ↥(u.sym (n - (↑m : ℕ))),
      HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι).countPerms : ℝ)
        (∏ x_2 ∈ Insert.insert i u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
              (fun (i : Fin (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))
              (f x_2) s x))

Tactic:
grw [IH]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
IH :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
⊢ LE.le (α := ℝ)
    (∑ i_1 : ↥(u.sym (n - (↑m : ℕ))),
      (↑(n.choose (↑m : ℕ)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
        HMul.hMul (α := ℝ) (↑(↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
                (fun (i : Fin (Multiset.count j (↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι)) (f j) s x)))
    (∑ x_1 : ↥(u.sym (n - (↑m : ℕ))),
      HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι).countPerms : ℝ)
        (∏ x_2 ∈ insert i u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
              (fun (i : Fin (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))
              (f x_2) s x)))

Tactic:
Finset.sum_le_sum ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
IH :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
p : Sym ι (n - (↑m : ℕ))
hp : ∀ a ∈ p, a ∈ u
⊢ (↑(n.choose (↑m : ℕ)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑p : Multiset ι)) (f x_1) s x)) ≤
    HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m p) : Multiset ι).countPerms : ℝ)
      (∏ x_1 ∈ insert i u,
        norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
            (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι)) (f x_1) s x))

Tactic:
le_of_eq ?_

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
IH :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
p : Sym ι (n - (↑m : ℕ))
hp : ∀ a ∈ p, a ∈ u
insert :
  (↑(n.choose (↑m : ℕ)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑p : Multiset ι)) (f x_1) s x)) =
    HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m p) : Multiset ι).countPerms : ℝ)
      (∏ x_1 ∈ Insert.insert i u,
        norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
            (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι)) (f x_1) s x))
⊢ (↑(n.choose (↑m : ℕ)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑p : Multiset ι)) (f x_1) s x)) ≤
    HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m p) : Multiset ι).countPerms : ℝ)
      (∏ x_1 ∈ Insert.insert i u,
        norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
            (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι)) (f x_1) s x))

Tactic:
refine le_of_eq ?_

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
IH :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
p : Sym ι (n - (↑m : ℕ))
hp : ∀ a ∈ p, a ∈ u
insert :
  (↑(n.choose (↑m : ℕ)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑p : Multiset ι)) (f x_1) s x)) =
    (↑(↑(Sym.fill i m p) : Multiset ι).countPerms : ℝ) *
      (norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
            (fun (i : Fin (Multiset.count i (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count i (↑(Sym.fill i m p) : Multiset ι)) (f i) s x) *
        ∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
              (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι)) (f x_1) s x))
⊢ (↑(n.choose (↑m : ℕ)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑p : Multiset ι)) (f x_1) s x)) =
    HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m p) : Multiset ι).countPerms : ℝ)
      (∏ x_1 ∈ Insert.insert i u,
        norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
            (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι)) (f x_1) s x))

Tactic:
rw [Finset.prod_insert hi]

Premises used: Finset.prod_insert
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
IH :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
p : Sym ι (n - (↑m : ℕ))
hp : ∀ a ∈ p, a ∈ u
⊢ i ∉ p

Tactic:
have hip : i ∉ p := mt (hp i) hi