awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hf' : ContDiffOn 𝕜 n f t
hst : s ∪ t = univ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
rw : ContDiffOn 𝕜 n f (s ∪ t)
⊢ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ, ← hst]

Premises used: contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hf' : ContDiffOn 𝕜 n f t
hst : s ∪ t = univ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiffOn 𝕜 n f (s ∪ t)

Tactic:
hf.union_of_isOpen hf' hs ht

Premises used: ContDiffOn.union_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hf' : ContDiffOn 𝕜 n f t
hst : s ∪ t = univ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiffOn 𝕜 n f (s ∪ t)

Tactic:
exact hf.union_of_isOpen hf' hs ht

Premises used: ContDiffOn.union_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
x : E
i : ι
hxsi : Membership.mem (γ := Set E) ((fun (i : ι) ↦ s i) i) x
⊢ ContDiffWithinAt 𝕜 n f (⋃ (i : ι), s i) x

Tactic:
(hf i).contDiffAt ((hs i).mem_nhds hxsi) |>.contDiffWithinAt

Premises used: IsOpen.mem_nhds, ContDiffOn.contDiffAt, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
x : E
i : ι
hxsi : Membership.mem (γ := Set E) ((fun (i : ι) ↦ s i) i) x
⊢ ContDiffWithinAt 𝕜 n f (⋃ (i : ι), s i) x

Tactic:
exact (hf i).contDiffAt ((hs i).mem_nhds hxsi) |>.contDiffWithinAt

Premises used: IsOpen.mem_nhds, ContDiffOn.contDiffAt, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
⊢ ContDiffOn 𝕜 n f (⋃ (i : ι), s i) ↔ ∀ (i : ι), ContDiffOn 𝕜 n f (s i)

Tactic:
⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a,
   fun h ↦ ContDiffOn.iUnion_of_isOpen h hs⟩

Premises used: Set.subset_iUnion_of_subset, ContDiffOn.mono, ContDiffOn.iUnion_of_isOpen, Iff.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
rw : ContDiffOn 𝕜 n f (⋃ (i : ι), s i)
⊢ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ, ← hs']

Premises used: contDiffOn_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
⊢ ContDiffOn 𝕜 n f (⋃ (i : ι), s i)

Tactic:
ContDiffOn.iUnion_of_isOpen hf hs

Premises used: ContDiffOn.iUnion_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
ι : Type u_5
s : ι → Set E
hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
hs : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
⊢ ContDiffOn 𝕜 n f (⋃ (i : ι), s i)

Tactic:
exact ContDiffOn.iUnion_of_isOpen hf hs

Premises used: ContDiffOn.iUnion_of_isOpen
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
⊢ ContDiff 𝕜 (E := (E × F) × G) (F := E × F × G) n (⇑(Equiv.prodAssoc E F G) : (a : (E × F) × G) → E × F × G)

Tactic:
(LinearIsometryEquiv.prodAssoc 𝕜 E F G).contDiff

Premises used: LinearIsometryEquiv.contDiff, LinearIsometryEquiv.prodAssoc
-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
⊢ ContDiff 𝕜 (E := E × F × G) (F := (E × F) × G) n (⇑(Equiv.prodAssoc E F G).symm : (a : E × F × G) → (E × F) × G)

Tactic:
(LinearIsometryEquiv.prodAssoc 𝕜 E F G).symm.contDiff

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.contDiff, LinearIsometryEquiv.prodAssoc
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑0 : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑0 : ℕ∞ω) g s
zero :
  norm (E := Gu) ((((B : (a : Eu) → Fu →L[𝕜] Gu) (f x) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g x) : Gu) ≤ ‖B‖ * ‖f x‖ * ‖g x‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ Du) Gu)
      (iteratedFDerivWithin 𝕜 0
        (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
        (↑(Nat.choose 0 i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (0 - i)) ↦ Du) Fu) (iteratedFDerivWithin 𝕜 (0 - i) g s x)

Tactic:
simp only [norm_iteratedFDerivWithin_zero, zero_add, Finset.range_one,
      Finset.sum_singleton, Nat.choose_self, Nat.cast_one, one_mul, Nat.sub_zero, ← mul_assoc]

Premises used: norm_iteratedFDerivWithin_zero, mul_assoc, zero_add, Finset.sum_singleton, Nat.sub_zero, Finset.range_one, Nat.cast_one, Nat.choose_self, one_mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑0 : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑0 : ℕ∞ω) g s
⊢ norm (E := Gu) ((((B : (a : Eu) → Fu →L[𝕜] Gu) (f x) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g x) : Gu) ≤ ‖B‖ * ‖f x‖ * ‖g x‖

Tactic:
apply B.le_opNorm₂

Premises used: ContinuousLinearMap.le_opNorm₂
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
⊢ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)

Tactic:
simp only [Nat.cast_succ, le_refl]

Premises used: Nat.cast_succ, le_refl
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
⊢ HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)

Tactic:
have In : (n : ℕ∞ω) + 1 ≤ n.succ := by simp only [Nat.cast_succ, le_refl]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) (Du →L[𝕜] Gu))
      (iteratedFDerivWithin 𝕜 n
        (fun (y : Du) ↦
          (((precompR Du B : (a : Eu) → (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) (f y) : (Du →L[𝕜] Fu) →L[𝕜] Du →L[𝕜] Gu) :
              (a : Du →L[𝕜] Fu) → Du →L[𝕜] Gu)
            (fderivWithin 𝕜 g s y))
        s x) ≤
    HMul.hMul (α := ℝ) sorry
      (∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) (Du →L[𝕜] Fu))
            (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x))

Tactic:
IH _ (hf.of_le (Nat.cast_le.2 (Nat.le_succ n))) (hg.fderivWithin hs In)

Premises used: Iff.mpr, Nat.le_succ, ContDiffOn.of_le, ContDiffOn.fderivWithin, Nat.cast_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
hbc : sorry ≤ ‖B‖
⊢ HMul.hMul (α := ℝ) sorry
      (∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) (Du →L[𝕜] Fu))
            (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x)) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) (Du →L[𝕜] Fu))
            (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
⊢ sorry ≤ ‖B‖

Tactic:
B.norm_precompR_le Du

Premises used: ContinuousLinearMap.norm_precompR_le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
e_a :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) (Du →L[𝕜] Fu))
          (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x))
    (∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
          (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x))
⊢ ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) (Du →L[𝕜] Fu))
            (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x) =
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
            (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
Du : Type u
inst_1 : NormedAddCommGroup Du
inst_2 : NormedSpace 𝕜 Du
s : Set Du
x : Du
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
IH :
  ∀ {Eu Fu Gu : Type u} [inst_9 : NormedAddCommGroup Eu] [inst_10 : NormedSpace 𝕜 Eu] [inst_11 : NormedAddCommGroup Fu]
    [inst_12 : NormedSpace 𝕜 Fu] [inst_13 : NormedAddCommGroup Gu] [inst_14 : NormedSpace 𝕜 Gu]
    (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} (hf : ContDiffOn 𝕜 (↑n : ℕ∞ω) f s)
    (hg : ContDiffOn 𝕜 (↑n : ℕ∞ω) g s),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Du) Gu)
        (iteratedFDerivWithin 𝕜 n
          (fun (y : Du) ↦ (((B : (a : Eu) → Fu →L[𝕜] Gu) (f y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (g y)) s x) ≤
      ‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
            norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) Fu)
              (iteratedFDerivWithin 𝕜 (n - i) g s x)
Eu Fu Gu : Type u
inst_3 : NormedAddCommGroup Eu
inst_4 : NormedSpace 𝕜 Eu
inst_5 : NormedAddCommGroup Fu
inst_6 : NormedSpace 𝕜 Fu
inst_7 : NormedAddCommGroup Gu
inst_8 : NormedSpace 𝕜 Gu
B : Eu →L[𝕜] Fu →L[𝕜] Gu
f : Du → Eu
g : Du → Fu
hf : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) f s
hg : ContDiffOn 𝕜 (↑(n + 1) : ℕ∞ω) g s
In : HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1 ≤ (↑n.succ : ℕ∞ω)
apply :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (n + 1)),
    (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) (Du →L[𝕜] Fu))
          (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x) =
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
          (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x)
⊢ Eq (α := ℝ)
    (∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n - i)) ↦ Du) (Du →L[𝕜] Fu))
          (iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 g s) s x))
    (∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1 - i)) ↦ Du) Fu)
          (iteratedFDerivWithin 𝕜 (n + 1 - i) g s x))

Tactic:
apply Finset.sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl