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
A : Type u_3
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin n) ↦ E) A)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ f y * g y) univ x) ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      (↑(n.choose x_1) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin x_1) ↦ E) A)
            (iteratedFDerivWithin 𝕜 x_1 f univ x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin (n - x_1)) ↦ E) A)
          (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)

Tactic:
norm_iteratedFDerivWithin_mul_le
    hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn

Premises used: ContDiff.contDiffOn, uniqueDiffOn_univ, Set.mem_univ, norm_iteratedFDerivWithin_mul_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_3
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin n) ↦ E) A)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ f y * g y) univ x) ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      (↑(n.choose x_1) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin x_1) ↦ E) A)
            (iteratedFDerivWithin 𝕜 x_1 f univ x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin (n - x_1)) ↦ E) A)
          (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)

Tactic:
exact norm_iteratedFDerivWithin_mul_le
    hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn

Premises used: ContDiff.contDiffOn, uniqueDiffOn_univ, Set.mem_univ, norm_iteratedFDerivWithin_mul_le
-- 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
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffOn 𝕜 N (f i) s
hn : (↑0 : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin 0) ↦ E) A')
      (iteratedFDerivWithin 𝕜 0 (fun (x : E) ↦ ∏ j ∈ ∅, f j x) s x) ≤
    ∑ p ∈ Finset.sym ∅ 0,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ ∅,
          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:
simp [Sym.eq_nil_of_card_zero]

Premises used: Sym.eq_nil_of_card_zero
-- 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
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffOn 𝕜 N (f i) s
n : ℕ
hn : (↑(n + 1) : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n + 1)) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ ∏ j ∈ ∅, f j x) s x) ≤
    ∑ p ∈ Finset.sym ∅ (n + 1),
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ ∅,
          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:
simp [iteratedFDerivWithin_succ_const]

Premises used: iteratedFDerivWithin_succ_const
-- 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
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffOn 𝕜 N (f i) s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
empty :
  ∀ (hn : (↑0 : ℕ∞ω) ≤ N),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin 0) ↦ E) A')
        (iteratedFDerivWithin 𝕜 0 (fun (x : E) ↦ ∏ j ∈ ∅, f j x) s x) ≤
      ∑ p ∈ Finset.sym ∅ 0,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ ∅,
            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))
empty₁ :
  ∀ (n : ℕ) (hn : (↑(n + 1) : ℕ∞ω) ≤ N),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n + 1)) ↦ E) A')
        (iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) ↦ ∏ j ∈ ∅, f j x) s x) ≤
      ∑ p ∈ Finset.sym ∅ (n + 1),
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ ∅,
            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))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
      (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ ∅, f j x) s x) ≤
    ∑ p ∈ Finset.sym ∅ n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ ∅,
          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:
cases n with
    | zero => simp [Sym.eq_nil_of_card_zero]
    | succ n => simp [iteratedFDerivWithin_succ_const]

Premises used: Fin.succ, iteratedFDerivWithin_succ_const, Sym.eq_nil_of_card_zero
-- 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))
hf : ∀ i_1 ∈ insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
lhs :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
    (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ insert i u, f j x) s x)
| norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
      (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ insert i u, f j x) s x) ≤
    ∑ p ∈ (insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ insert i 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:
lhs
-- 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))
hf : ∀ i_1 ∈ insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
simp :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
    (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ f i x * ∏ j ∈ u, f j x) s x)
| norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
    (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ insert i u, f j x) s x)

Tactic:
simp only [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
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))
hf : ∀ i_1 ∈ insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
simp :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
    (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ f i x * ∏ j ∈ u, f j x) s x)
| norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
      (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ insert i u, f j x) s x) ≤
    ∑ p ∈ (insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ insert i 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:
lhs; simp only [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
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))
hf : ∀ i_1 ∈ Insert.insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
insert :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
      (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ f i x * ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ (Insert.insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ Insert.insert i 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))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
      (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ Insert.insert i u, f j x) s x) ≤
    ∑ p ∈ (Insert.insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ Insert.insert i 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:
conv => lhs; simp only [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
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))
hf : ∀ i_1 ∈ insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hf

Premises used: Finset.mem_insert, forall_eq_or_imp
-- 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
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
      (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ f i x * ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ (insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ insert i 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:
le_trans (norm_iteratedFDerivWithin_mul_le hf.1 (contDiffOn_prod hf.2) hs hx hn) ?_

Premises used: contDiffOn_prod, And.right, And.left, norm_iteratedFDerivWithin_mul_le, 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
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 :
  LE.le (α := ℝ)
    (∑ i_1 ∈ Finset.range (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))
    (∑ p ∈ (Insert.insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ Insert.insert i 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)))
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
      (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ f i x * ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ (Insert.insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ Insert.insert i 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:
refine le_trans (norm_iteratedFDerivWithin_mul_le hf.1 (contDiffOn_prod hf.2) hs hx hn) ?_

Premises used: contDiffOn_prod, And.right, And.left, norm_iteratedFDerivWithin_mul_le, 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
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 :
  LE.le (α := ℝ)
    (∑ i_1 ∈ Finset.range (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))
    (∑ i_1 : ↥((Insert.insert i u).sym n),
      HMul.hMul (α := ℝ) (↑(↑(↑i_1 : Sym ι n) : Multiset ι).countPerms : ℝ)
        (∏ j ∈ Insert.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)))
⊢ LE.le (α := ℝ)
    (∑ i_1 ∈ Finset.range (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))
    (∑ p ∈ (Insert.insert i u).sym n,
      HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ j ∈ Insert.insert i 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:
rw [← Finset.sum_coe_sort (Finset.sym _ _)]

Premises used: Finset.sym, Finset.sum_coe_sort
-- 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 ↔
      Membership.mem (α := (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ)))) (γ :=
        Finset ((i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ))))) Finset.univ
        ((Finset.symInsertEquiv hi : (a : ↥((insert i u).sym n)) → (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ)))) i_1 :
          (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ))))

Tactic:
simp