awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
t : ℝ
Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
⊢ ∃ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) x_1 ∧
      f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) x_1) : (a : E) → ℝ) (y - x)

Tactic:
⟨t, hsub Ht, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
t : ℝ
Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
refine : f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) t) : (a : E) → ℝ) (y - x)
⊢ ∃ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) x_1 ∧
      f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) x_1) : (a : E) → ℝ) (y - x)

Tactic:
refine ⟨t, hsub Ht, ?_⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
t : ℝ
Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
⊢ f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) t) : (a : E) → ℝ) (y - x)

Tactic:
simpa [g] using hMVT'.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : HasDerivWithinAt u u' s x
hv : HasDerivWithinAt v v' s x
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    s x

Tactic:
simpa using (B.hasFDerivWithinAt_of_bilinear
    hu.hasFDerivWithinAt hv.hasFDerivWithinAt).hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, ContinuousLinearMap.hasFDerivWithinAt_of_bilinear, HasFDerivWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
pos :
  ∀ (hxu : x ∈ tsupport u),
    HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
      (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
      x
neg :
  ∀ (hxu : x ∉ tsupport u),
    HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
      (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
      x
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x

Tactic:
by_cases hxu : x ∈ tsupport u

Premises used: tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
pos :
  ∀ (hxv : x ∈ tsupport v),
    HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
      (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
      x
neg :
  ∀ (hxv : x ∉ tsupport v),
    HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
      (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
      x
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x

Tactic:
by_cases hxv : x ∈ tsupport v

Premises used: tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∈ tsupport v
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x

Tactic:
simpa using (B.hasFDerivAt_of_bilinear (hu hxv).hasFDerivAt (hv hxu).hasFDerivAt).hasDerivAt

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.hasDerivAt, ContinuousLinearMap.hasFDerivAt_of_bilinear
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x_1 : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x_1 ∈ tsupport v → HasDerivAt u u' x_1
hv : x_1 ∈ tsupport u → HasDerivAt v v' x_1
hxu : x_1 ∈ tsupport u
hxv : x_1 ∉ tsupport v
h_1 :
  Membership.mem (γ := Set 𝕜)
    (tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)) x_1
x : 𝕜
h : v x = 0
⊢ Eq.{u_1 + 1} (α := G) ((fun (x : 𝕜) ↦ ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)) x) 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
⊢ x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)

Tactic:
have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
        mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxv
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
⊢ HasDerivAt.{u, u_1} (F := G) (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)) 0 x

Tactic:
HasDerivAt.of_notMem_tsupport hx

Premises used: HasDerivAt.of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
h :
  HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
    0
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x

Tactic:
convert! HasDerivAt.of_notMem_tsupport hx

Premises used: HasDerivAt.of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∈ tsupport u
hxv : x ∉ tsupport v
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
⊢ HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
    0

Tactic:
simp [(hv hxu).unique <| .of_notMem_tsupport hxv, image_eq_zero_of_notMem_tsupport hxv]

Premises used: image_eq_zero_of_notMem_tsupport, HasDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x_1 : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x_1 ∈ tsupport v → HasDerivAt u u' x_1
hv : x_1 ∈ tsupport u → HasDerivAt v v' x_1
hxu : x_1 ∉ tsupport u
h_1 :
  Membership.mem (γ := Set 𝕜)
    (tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)) x_1
x : 𝕜
h : u x = 0
⊢ Eq.{u_1 + 1} (α := G) ((fun (x : 𝕜) ↦ ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)) x) 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
⊢ x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)

Tactic:
have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
      mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxu
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
⊢ HasDerivAt.{u, u_1} (F := G) (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)) 0 x

Tactic:
HasDerivAt.of_notMem_tsupport hx

Premises used: HasDerivAt.of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
h :
  HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
    0
⊢ HasDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x

Tactic:
convert! HasDerivAt.of_notMem_tsupport hx

Premises used: HasDerivAt.of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
pos :
  ∀ (hxv : x ∈ tsupport v),
    HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
      0
neg :
  ∀ (hxv : x ∉ tsupport v),
    HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
        ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
      0
⊢ HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
    0

Tactic:
by_cases hxv : x ∈ tsupport v

Premises used: tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
hxv : x ∈ tsupport v
⊢ HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
    0

Tactic:
simp [image_eq_zero_of_notMem_tsupport hxu, (hu hxv).unique <| .of_notMem_tsupport hxu]

Premises used: image_eq_zero_of_notMem_tsupport, HasDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport.{u, u_1} (α := G) fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x)
hxv : x ∉ tsupport v
⊢ HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G) =
    0

Tactic:
simp [image_eq_zero_of_notMem_tsupport hxu, image_eq_zero_of_notMem_tsupport hxv]

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : HasStrictDerivAt u u' x
hv : HasStrictDerivAt v v' x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (v x))
    (HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) v' : G)
      ((((B : (a : E) → F →L[𝕜] G) u' : F →L[𝕜] G) : (a : F) → G) (v x) : G))
    x

Tactic:
simpa using
    (B.hasStrictFDerivAt_of_bilinear hu.hasStrictFDerivAt hv.hasStrictFDerivAt).hasStrictDerivAt

Premises used: ContinuousLinearMap.hasStrictFDerivAt_of_bilinear, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u y) : F →L[𝕜] G) : (a : F) → G) (v y)) s x =
      HAdd.hAdd (α := G) (β := G)
        ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (derivWithin v s x) : G)
        ((((B : (a : E) → F →L[𝕜] G) (derivWithin u s x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u y) : F →L[𝕜] G) : (a : F) → G) (v y)) s x =
      HAdd.hAdd (α := G) (β := G)
        ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (derivWithin v s x) : G)
        ((((B : (a : E) → F →L[𝕜] G) (derivWithin u s x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)
⊢ derivWithin (fun (y : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u y) : F →L[𝕜] G) : (a : F) → G) (v y)) s x =
    HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (derivWithin v s x) : G)
      ((((B : (a : E) → F →L[𝕜] G) (derivWithin u s x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u y) : F →L[𝕜] G) : (a : F) → G) (v y)) s x =
    HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (derivWithin v s x) : G)
      ((((B : (a : E) → F →L[𝕜] G) (derivWithin u s x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)

Tactic:
(B.hasDerivWithinAt_of_bilinear hu.hasDerivWithinAt hv.hasDerivWithinAt).derivWithin hsx

Premises used: ContinuousLinearMap.hasDerivWithinAt_of_bilinear, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u y) : F →L[𝕜] G) : (a : F) → G) (v y)) s x =
    HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (derivWithin v s x) : G)
      ((((B : (a : E) → F →L[𝕜] G) (derivWithin u s x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)

Tactic:
exact (B.hasDerivWithinAt_of_bilinear hu.hasDerivWithinAt hv.hasDerivWithinAt).derivWithin hsx

Premises used: ContinuousLinearMap.hasDerivWithinAt_of_bilinear, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : DifferentiableWithinAt 𝕜 u s x
hv : DifferentiableWithinAt 𝕜 v s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u y) : F →L[𝕜] G) : (a : F) → G) (v y)) s x =
    HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (derivWithin v s x) : G)
      ((((B : (a : E) → F →L[𝕜] G) (derivWithin u s x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt