awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (hypothesis)
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
⊢ 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
have 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)
Tactic: have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
      mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxu
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
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 (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
have 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
Tactic: convert! HasDerivAt.of_notMem_tsupport hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
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)
⊢ 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
have 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
Tactic: by_cases hxv : x ∈ tsupport v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
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
⊢ 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
have 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
Tactic: by_cases hxv : x ∈ tsupport v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
hf : HasDerivAt f f' x
⊢ HasDerivAt (c • f) (c x • f' + c' • f x) x
have rw : ∀ (hc : HasDerivWithinAt c c' univ x) (hf : HasDerivWithinAt f f' univ x),
  HasDerivWithinAt (c • f) (c x • f' + c' • f x) univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hc, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
have this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) x
Tactic: have := hc.smul (hasStrictDerivAt_const x f)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) x
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
have rwa : ∀ (this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (0 + c' • f) x),
  HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
Tactic: rwa [smul_zero, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) x
rwa :
  ∀ (this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (0 + c' • f) x),
    HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
have rwa₁ : ∀ (this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (c' • f) x),
  HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
Tactic: rwa [smul_zero, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
have this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) s x
Tactic: have := hc.smul (hasDerivWithinAt_const x s f)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) s x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
have rwa : ∀ (this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (0 + c' • f) s x),
  HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
Tactic: rwa [smul_zero, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) s x
rwa :
  ∀ (this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (0 + c' • f) s x),
    HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
have rwa₁ : ∀ (this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (c' • f) s x),
  HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
Tactic: rwa [smul_zero, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
f : F
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
have rw : ∀ (hc : HasDerivWithinAt c c' univ x) (f : F), HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hc, f
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
⊢ HasDerivAt (c * d) (c' * d x + c x * d') x
have rw : ∀ (hc : HasDerivWithinAt c c' univ x) (hd : HasDerivWithinAt d d' univ x),
  HasDerivWithinAt (c * d) (c' * d x + c x * d') univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hc, hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y * d) (c' * d) s x
have h : c' * d = c' * d + c x * 0
Tactic: convert! hc.mul (hasDerivWithinAt_const x s d) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
⊢ c' * d = c' * d + c x * 0
have h : c' * d = c' * d + 0
Tactic: rw [mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
h : c' * d = c' * d + 0
⊢ c' * d = c' * d + c x * 0
have h₁ : c' * d = c' * d
Tactic: rw [mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivAt c c' x
d : 𝔸
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y * d) (c' * d) x
have rw : ∀ (hc : HasDerivWithinAt c c' univ x) (d : 𝔸), HasDerivWithinAt (fun (y : 𝕜) ↦ c y * d) (c' * d) univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hc, d
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y * d) (c' * d) x
have h : c' * d = c' * d + c x * 0
Tactic: convert! hc.mul (hasStrictDerivAt_const x d) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
⊢ c' * d = c' * d + c x * 0
have h : c' * d = c' * d + 0
Tactic: rw [mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
h : c' * d = c' * d + 0
⊢ c' * d = c' * d + c x * 0
have h₁ : c' * d = c' * d
Tactic: rw [mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x