awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
h : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x
cons :
  iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ f a x + ∑ j ∈ u, f j x) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ Finset.cons a u ha, f j x) s x)
    (∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x)

Tactic:
simp only [Finset.sum_cons]

Premises used: Finset.sum_cons
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
h : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f a) s x
cons :
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ i ∈ u, f i x) s x) =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
cons₁ cons₂ :
  HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x) =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)
⊢ iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ f a x + ∑ j ∈ u, f j x) s x =
    HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (f a) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)

Tactic:
rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]

Premises used: fun_iteratedFDerivWithin_add_apply, ContDiffWithinAt.sum, And.right, And.left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
empty :
  ∀ (h : ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ ∅, f j x) s x) (∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x)
cons :
  ∀ (a : ι) (u : Finset ι) (ha : a ∉ u)
    (IH :
      ∀ (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
        Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
          (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x))
    (h : ∀ j ∈ Finset.cons a u ha, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ Finset.cons a u ha, f j x) s x)
      (∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)

Tactic:
induction u using Finset.cons_induction with
  | empty => simp
  | cons a u ha IH =>
    simp only [Finset.mem_cons, forall_eq_or_imp] at h
    simp only [Finset.sum_cons]
    rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]

Premises used: Finset.sum_cons, Fin.cons, forall_eq_or_imp, Finset.mem_cons
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)

Tactic:
iteratedFDerivWithin_sum_apply hs hx h

Premises used: iteratedFDerivWithin_sum_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
h₁ : ∀ (x : E), Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x) ((∑ j ∈ u, f j) x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (z : E) ↦ ∑ j ∈ u, f j z) s x) (∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x)

Tactic:
convert! iteratedFDerivWithin_sum_apply hs hx h

Premises used: iteratedFDerivWithin_sum_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) (f j) s x
x_1 : E
h₁ h₂ : Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) (∑ c ∈ u, f c x_1)
⊢ Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) ((∑ j ∈ u, f j) x_1)

Tactic:
rw [Finset.sum_apply]

Premises used: Finset.sum_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
simp :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (∑ j ∈ u, f j) univ x) (∑ x_1 ∈ u, iteratedFDerivWithin 𝕜 n (f x_1) univ x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n (∑ j ∈ u, f j) x)
    (∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x)

Tactic:
simp only [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDerivWithin 𝕜 n (∑ j ∈ u, f j) univ x) (∑ x_1 ∈ u, iteratedFDerivWithin 𝕜 n (f x_1) univ x)

Tactic:
apply iteratedFDerivWithin_sum_apply uniqueDiffOn_univ (Set.mem_univ x)
    (h · · |>.contDiffWithinAt)

Premises used: uniqueDiffOn_univ, Set.mem_univ, iteratedFDerivWithin_sum_apply, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n (∑ j ∈ u, f j) x)
    (∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x)

Tactic:
iteratedFDeriv_sum_apply h

Premises used: iteratedFDeriv_sum_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
h₁ : ∀ (x : E), Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x) ((∑ j ∈ u, f j) x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv 𝕜 n (fun (z : E) ↦ ∑ j ∈ u, f j z) x) (∑ j ∈ u, iteratedFDeriv 𝕜 n (f j) x)

Tactic:
convert! iteratedFDeriv_sum_apply h

Premises used: iteratedFDeriv_sum_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n : ℕ∞ω) (f j) x
x_1 : E
h₁ h₂ : Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) (∑ c ∈ u, f c x_1)
⊢ Eq.{uF + 1} (α := F) (∑ j ∈ u, f j x_1) ((∑ j ∈ u, f j) x_1)

Tactic:
rw [Finset.sum_apply]

Premises used: Finset.sum_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
h : ∀ j ∈ u, ContDiff 𝕜 (↑i : ℕ∞ω) (f j)
x : E
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv 𝕜 i (fun (x : E) ↦ ∑ j ∈ u, f j x) x) ((∑ j ∈ u, iteratedFDeriv 𝕜 i (f j)) x)

Tactic:
simpa [iteratedFDerivWithin_univ] using
    iteratedFDerivWithin_fun_sum_apply uniqueDiffOn_univ (mem_univ x) (h · · |>.contDiffWithinAt)

Premises used: uniqueDiffOn_univ, ContDiff.contDiffWithinAt, iteratedFDerivWithin_fun_sum_apply, Set.mem_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
⊢ ContDiff 𝕜 (F := 𝔸) n fun (p : 𝔸 × 𝔸) ↦ p.1 * p.2

Tactic:
(ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.contDiff

Premises used: IsBoundedBilinearMap.contDiff, ContinuousLinearMap.isBoundedBilinearMap, ContinuousLinearMap.mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
s : Set E
f g : E → 𝔸
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt.{u_1, uE, u_3} 𝕜 (F := 𝔸) n (fun (x : E) ↦ f x * g x) s x

Tactic:
contDiff_mul.comp_contDiffWithinAt (hf.prodMk hg)

Premises used: ContDiff.comp_contDiffWithinAt, contDiff_mul, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f g : E → 𝔸
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt.{u_1, uE, u_3} 𝕜 (F := 𝔸) n (fun (x : E) ↦ f x * g x) x

Tactic:
hf.mul hg

Premises used: ContDiffAt, ContDiffWithinAt.mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f g : E → 𝔸
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn.{u_1, uE, u_3} 𝕜 (F := 𝔸) n (fun (x : E) ↦ f x * g x) s

Tactic:
fun x hx => (hf x hx).mul (hg x hx)

Premises used: ContDiffOn, ContDiffWithinAt.mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f g : E → 𝔸
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff.{u_1, uE, u_3} 𝕜 (F := 𝔸) n fun (x : E) ↦ f x * g x

Tactic:
contDiff_mul.comp (hf.prodMk hg)

Premises used: ContDiff.prodMk, ContDiff.comp, contDiff_mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x
⊢ ContDiffWithinAt.{u_1, uE, u_4} 𝕜 (F := 𝔸') n (∏ i ∈ t, f i) s x

Tactic:
Finset.prod_induction f (fun f => ContDiffWithinAt 𝕜 n f s x) (fun _ _ => ContDiffWithinAt.mul)
    (contDiffWithinAt_const (c := 1)) h

Premises used: contDiffWithinAt_const, ContDiffWithinAt.mul, Finset.prod_induction, ContDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x
⊢ ContDiffWithinAt.{u_1, uE, u_4} 𝕜 (F := 𝔸') n (fun (y : E) ↦ ∏ i ∈ t, f i y) s x

Tactic:
simpa only [← Finset.prod_apply] using contDiffWithinAt_prod' h

Premises used: Finset.prod_apply, contDiffWithinAt_prod'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x
⊢ ContDiffAt.{u_1, uE, u_4} 𝕜 (F := 𝔸') n (∏ i ∈ t, f i) x

Tactic:
contDiffWithinAt_prod' h

Premises used: ContDiffAt, contDiffWithinAt_prod'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x
⊢ ContDiffAt.{u_1, uE, u_4} 𝕜 (F := 𝔸') n (fun (y : E) ↦ ∏ i ∈ t, f i y) x

Tactic:
contDiffWithinAt_prod h

Premises used: ContDiffAt, contDiffWithinAt_prod
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s
⊢ ContDiffOn.{u_1, uE, u_4} 𝕜 (F := 𝔸') n (∏ i ∈ t, f i) s

Tactic:
fun x hx => contDiffWithinAt_prod' fun i hi => h i hi x hx

Premises used: ContDiffOn, contDiffWithinAt_prod'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s
⊢ ContDiffOn.{u_1, uE, u_4} 𝕜 (F := 𝔸') n (fun (y : E) ↦ ∏ i ∈ t, f i y) s

Tactic:
fun x hx =>
  contDiffWithinAt_prod fun i hi => h i hi x hx

Premises used: ContDiffOn, contDiffWithinAt_prod
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiff 𝕜 n (f i)
⊢ ContDiff.{u_1, uE, u_4} 𝕜 (E := E) (F := 𝔸') n (∏ i ∈ t, f i)

Tactic:
contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod' fun i hi => (h i hi).contDiffAt

Premises used: Iff.mpr, contDiffAt_prod', contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝔸' : Type u_4
ι : Type u_5
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
t : Finset ι
f : ι → E → 𝔸'
h : ∀ i ∈ t, ContDiff 𝕜 n (f i)
⊢ ContDiff.{u_1, uE, u_4} 𝕜 (F := 𝔸') n fun (y : E) ↦ ∏ i ∈ t, f i y

Tactic:
contDiff_iff_contDiffAt.mpr fun _ => contDiffAt_prod fun i hi => (h i hi).contDiffAt

Premises used: Iff.mpr, contDiffAt_prod, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiff 𝕜 n f
⊢ ContDiff.{u_1, uE, u_3} 𝕜 (F := 𝔸) n fun (x : E) ↦ HPow.hPow (β := ℕ) (f x) 0

Tactic:
simpa using contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiff 𝕜 n f
m : ℕ
⊢ ContDiff.{u_1, uE, u_3} 𝕜 (F := 𝔸) n fun (x : E) ↦ f x ^ (m + 1)

Tactic:
simpa [pow_succ] using (hf.pow m).mul hf

Premises used: pow_succ, ContDiff.mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiffWithinAt 𝕜 n f s x
m : ℕ
⊢ ContDiffWithinAt.{u_1, uE, u_3} 𝕜 (F := 𝔸) n (fun (y : E) ↦ f y ^ m) s x

Tactic:
(contDiff_id.pow m).comp_contDiffWithinAt hf

Premises used: ContDiff.comp_contDiffWithinAt, ContDiff.pow, contDiff_id
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiffAt 𝕜 n f x
m : ℕ
⊢ ContDiffAt.{u_1, uE, u_3} 𝕜 (F := 𝔸) n (fun (y : E) ↦ f y ^ m) x

Tactic:
hf.pow m

Premises used: ContDiffAt, ContDiffWithinAt.pow
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
n : ℕ∞ω
𝔸 : Type u_3
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiffOn 𝕜 n f s
m : ℕ
⊢ ContDiffOn.{u_1, uE, u_3} 𝕜 (F := 𝔸) n (fun (y : E) ↦ f y ^ m) s

Tactic:
fun y hy => (hf y hy).pow m

Premises used: ContDiffOn, ContDiffWithinAt.pow
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
𝕜' : Type u_6
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
n : ℕ∞ω
hf : ContDiffWithinAt 𝕜 n f s x
c : 𝕜'
⊢ ContDiffWithinAt.{u_1, uE, u_6} 𝕜 (F := 𝕜') n (fun (x : E) ↦ f x / c) s x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul contDiffWithinAt_const

Premises used: contDiffWithinAt_const, ContDiffWithinAt.mul, div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝕜' : Type u_6
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
c : 𝕜'
⊢ ContDiffAt.{u_1, uE, u_6} 𝕜 (F := 𝕜') n (fun (x : E) ↦ f x / c) x

Tactic:
hf.div_const c

Premises used: ContDiffAt, ContDiffWithinAt.div_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
𝕜' : Type u_6
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
c : 𝕜'
⊢ ContDiffOn.{u_1, uE, u_6} 𝕜 (F := 𝕜') n (fun (x : E) ↦ f x / c) s

Tactic:
fun x hx => (hf x hx).div_const c

Premises used: ContDiffOn, ContDiffWithinAt.div_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_6
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
n : ℕ∞ω
hf : ContDiff 𝕜 n f
c : 𝕜'
⊢ ContDiff.{u_1, uE, u_6} 𝕜 (F := 𝕜') n fun (x : E) ↦ f x / c

Tactic:
simpa only [div_eq_mul_inv] using hf.mul contDiff_const

Premises used: contDiff_const, div_eq_mul_inv, ContDiff.mul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
𝕜' : Type u_3
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
⊢ ContDiff 𝕜 (F := F) n fun (p : 𝕜' × F) ↦ p.1 • p.2

Tactic:
isBoundedBilinearMap_smul.contDiff

Premises used: IsBoundedBilinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
s : Set E
f : E → 𝕜'
g : E → F
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt 𝕜 n (f • g) s x

Tactic:
contDiff_smul.contDiffWithinAt.comp x (hf.prodMk hg) subset_preimage_univ

Premises used: ContDiffWithinAt.comp, Set.subset_preimage_univ, ContDiff.contDiffWithinAt, contDiff_smul, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ