awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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))
have 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 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 ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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))
have 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))
Tactic: rw [Finset.prod_insert hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
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)) =
    (↑(↑(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))
have hip : i ∉ p
Tactic: have hip : i ∉ p := mt (hp i) hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
hip : i ∉ p
⊢ (↑(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)) =
    (↑(n.choose (↑m : ℕ) * (↑p : Multiset ι).countPerms) : ℝ) *
      (norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (↑m : ℕ) (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))
have insert : Eq (α := ℝ)
  (∏ 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))
  (∏ j ∈ u,
    norm (E :=
      ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
        (fun (i : Fin (Multiset.count j (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(Sym.fill i m p) : Multiset ι)) (f j) s x))
Tactic: suffices ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖ =
        ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j (Sym.fill i m p)) (f j) s x‖ by
      rw [this, Nat.cast_mul]
      ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
hip : i ∉ p
⊢ Eq (α := ℝ)
    (∏ 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))
    (∏ j ∈ u,
      norm (E :=
        ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
          (fun (i : Fin (Multiset.count j (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
        (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(Sym.fill i m p) : Multiset ι)) (f j) s x))
have insert : ∀ 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) =
    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 Finset.prod_congr rfl ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
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
hip : i ∉ p
j : ι
hj : 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) =
    norm (E :=
      ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
        (fun (i : Fin (Multiset.count j (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(Sym.fill i m p) : Multiset ι)) (f j) s x)
have hji : j ≠ i
Tactic: have hji : j ≠ i := mt (· ▸ hj) hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
hip : i ∉ p
j : ι
hj : j ∈ u
hji : j ≠ i
⊢ 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 (Multiset.count j (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(Sym.fill i m p) : Multiset ι)) (f j) s x)
have insert : 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 (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
    (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x)
Tactic: rw [Sym.count_coe_fill_of_ne hji]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x) ≤
    (↑(n + 1)! : ℝ) * C * D ^ (n + 1)
have M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Tactic: have M : (n : ℕ∞ω) < n.succ := Nat.cast_lt.2 n.lt_succ_self
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin (n + 1)) ↦ E) Gu)
      (iteratedFDerivWithin 𝕜 (n + 1) (g ∘ f) s x) ≤
    (↑(n + 1)! : ℝ) * C * D ^ (n + 1)
have Cnonneg : 0 ≤ C
Tactic: have Cnonneg : 0 ≤ C := (norm_nonneg _).trans (hC 0 bot_le)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
Fu : Type u
inst_3 : NormedAddCommGroup Fu
inst_4 : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst_7 : NormedAddCommGroup Gu] [inst_8 : NormedSpace 𝕜 Gu] {g : Fu → Gu}
      (hg : ContDiffOn 𝕜 (↑m : ℕ∞ω) g t) (hf : ContDiffOn 𝕜 (↑m : ℕ∞ω) f s)
      (hC :
        ∀ i ≤ m,
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C)
      (hD :
        ∀ (i : ℕ),
          1 ≤ i →
            i ≤ m →
              norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
                  (iteratedFDerivWithin 𝕜 i f s x) ≤
                D ^ i),
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin m) ↦ E) Gu)
          (iteratedFDerivWithin 𝕜 m (g ∘ f) s x) ≤
        (↑m ! : ℝ) * C * D ^ m
Gu : Type u
inst_5 : NormedAddCommGroup Gu
inst_6 : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g t
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hC :
  ∀ i ≤ n + 1, norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Fu) Gu) (iteratedFDerivWithin 𝕜 i g t (f x)) ≤ C
hD :
  ∀ (i : ℕ),
    1 ≤ i →
      i ≤ n + 1 →
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u} 𝕜 (fun (i : Fin i) ↦ E) Fu)
            (iteratedFDerivWithin 𝕜 i f s x) ≤
          D ^ i
M : LT.lt (α := ℕ∞ω) (↑n : ℕ∞ω) (↑n.succ : ℕ∞ω)
Cnonneg : 0 ≤ C
⊢ 0 ≤ D
have this : 1 ≤ n + 1
Tactic: have : 1 ≤ n + 1 := by simp only [le_add_iff_nonneg_left, zero_le']