awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
have pos : ∀ (hv : DifferentiableWithinAt 𝕜 v s x), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
Tactic: by_cases hv : DifferentiableWithinAt 𝕜 v s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
pos : ∀ (hv : DifferentiableWithinAt 𝕜 v s x), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
have neg : ∀ (hv : ¬DifferentiableWithinAt 𝕜 v s x), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
Tactic: by_cases hv : DifferentiableWithinAt 𝕜 v s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
have pos : derivWithin v s x * u = derivWithin v s x * u
Tactic: rw [derivWithin_mul_const hv u]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
have pos : ∀ (hu : u = 0), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
Tactic: by_cases hu : u = 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
pos : ∀ (hu : u = 0), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
have neg : ∀ (hu : ¬u = 0), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
Tactic: by_cases hu : u = 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
have neg : ¬DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ v y * u) s x
Tactic: rw [derivWithin_zero_of_not_differentiableWithinAt hv, zero_mul,
      derivWithin_zero_of_not_differentiableWithinAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ v = fun (x : 𝕜) ↦ v x * u * u⁻¹
have h : ∀ (x : 𝕜), v x = v x * u * u⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ ¬DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ v y * u) s x
have this : v = fun (x : 𝕜) ↦ v x * u * u⁻¹
Tactic: have : v = fun x ↦ (v x * u) * u⁻¹ := by ext; simp [hu]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
⊢ deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
have pos : ∀ (hu : DifferentiableAt 𝕜 u x), deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
Tactic: by_cases hu : DifferentiableAt 𝕜 u x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
pos : ∀ (hu : DifferentiableAt 𝕜 u x), deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
⊢ deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
have neg : ∀ (hu : ¬DifferentiableAt 𝕜 u x), deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
Tactic: by_cases hu : DifferentiableAt 𝕜 u x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
⊢ deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
have neg : Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0
Tactic: rw [deriv_zero_of_not_differentiableAt hu, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
⊢ Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0
have neg : Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * 0) x) 0
Tactic: rcases eq_or_ne v 0 with (rfl | hd)
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
neg : Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * 0) x) 0
⊢ Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0
have neg₁ : ∀ (hd : v ≠ 0), Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0
Tactic: rcases eq_or_ne v 0 with (rfl | hd)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
hd : v ≠ 0
⊢ Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0
have neg : ∀ (H : DifferentiableAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ u y * v) x), DifferentiableAt 𝕜 u x
Tactic: refine deriv_zero_of_not_differentiableAt (mt (fun H => ?_) hu)
-- 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 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c * d y) (c * d') s x
have h : c * d' = 0 * d x + c * d'
Tactic: convert! (hasDerivWithinAt_const x s c).mul hd 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 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
⊢ c * d' = 0 * d x + c * d'
have h : c * d' = 0 + c * d'
Tactic: rw [zero_mul, zero_add]
-- 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 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
h : c * d' = 0 + c * d'
⊢ c * d' = 0 * d x + c * d'
have h₁ : c * d' = c * d'
Tactic: rw [zero_mul, zero_add]
-- 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 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivAt d d' x
⊢ HasDerivAt (fun (y : 𝕜) ↦ c * d y) (c * d') x
have rw : ∀ (hd : HasDerivWithinAt d d' univ x), HasDerivWithinAt (fun (y : 𝕜) ↦ c * d y) (c * d') univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hd
-- 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 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c * d y) (c * d') x
have h : c * d' = 0 * d x + c * d'
Tactic: convert! (hasStrictDerivAt_const _ _).mul hd 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 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ c * d' = 0 * d x + c * d'
have h : c * d' = 0 + c * d'
Tactic: rw [zero_mul, zero_add]
-- 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 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
h : c * d' = 0 + c * d'
⊢ c * d' = 0 * d x + c * d'
have h₁ : c * d' = c * d'
Tactic: rw [zero_mul, zero_add]
-- 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 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * derivWithin d s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * 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 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * derivWithin d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * derivWithin d s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * 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 : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
⊢ HasDerivAt.{u, u_3} (F := 𝔸') (∏ i ∈ u, f i) (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x
have h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
Tactic: convert! HasDerivAt.fun_finsetProd hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
⊢ HasDerivWithinAt.{u, u_3} (F := 𝔸') (∏ i ∈ u, f i) (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) s
    x
have h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
Tactic: convert! HasDerivWithinAt.fun_finsetProd hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x
⊢ HasStrictDerivAt.{u, u_3} (F := 𝔸') (∏ i ∈ u, f i) (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x
have h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
Tactic: convert! HasStrictDerivAt.fun_finsetProd hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) 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_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
      (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) 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_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (∏ i ∈ u, f i) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))
have h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
Tactic: convert! derivWithin_fun_finsetProd hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt.{u, u, u_3} 𝕜 (F := 𝔸') (∏ i ∈ u, f i) x
have h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
Tactic: convert! DifferentiableAt.fun_finsetProd hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Mul (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt.{u, u, u_3} 𝕜 (F := 𝔸') (∏ i ∈ u, f i) s x
have h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
Tactic: convert! DifferentiableWithinAt.fun_finsetProd hd
-- 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
x : 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') x
have rw : ∀ (hc : HasDerivWithinAt c c' univ x) (hd : HasDerivWithinAt d d' univ x),
  HasDerivWithinAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL 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 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL 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 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL 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 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
⊢ derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s x) : G)
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s 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
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
      HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
        ((c x : (a : F) → G) (derivWithin u s x) : G)
⊢ derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s x) : G)
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s x) : G)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
⊢ HasDerivAt (Function.update (β := fun (a : ι) ↦ 𝕜) x i) (Pi.single (M := fun (a : ι) ↦ 𝕜) i 1) y
have h : Eq (α := (x : 𝕜) → (j : ι) → 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i : (x : 𝕜) → (j : ι) → 𝕜)
  ((⇑(ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜))) :
      (a : 𝕜) → (a : ι) → 𝕜) :
    (a : 𝕜) → (a : ι) → 𝕜)
Tactic: convert! (hasFDerivAt_update x y).hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
⊢ Eq (α := (x : 𝕜) → (j : ι) → 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i : (x : 𝕜) → (j : ι) → 𝕜)
    ((⇑(ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜))) :
        (a : 𝕜) → (a : ι) → 𝕜) :
      (a : 𝕜) → (a : ι) → 𝕜)
have h : ∀ (z : 𝕜) (j : ι),
  Eq.{u_1 + 1} (α := 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i z j : 𝕜)
    ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
          (a : 𝕜) → (a : ι) → 𝕜)
        z j :
      𝕜)
Tactic: ext z j
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
⊢ Eq.{u_1 + 1} (α := 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i z j : 𝕜)
    ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
          (a : 𝕜) → (a : ι) → 𝕜)
        z j :
      𝕜)
have h : (if j = i then z else 0 j) =
  (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
        (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
      (a : 𝕜) → (a : ι) → 𝕜)
    z j
Tactic: rw [Pi.single, Function.update_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
⊢ (if j = i then z else 0 j) =
    (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
        (a : 𝕜) → (a : ι) → 𝕜)
      z j
have pos : ∀ (h : j = i),
  z =
    (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
        (a : 𝕜) → (a : ι) → 𝕜)
      z j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
pos :
  ∀ (h : j = i),
    z =
      (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
          (a : 𝕜) → (a : ι) → 𝕜)
        z j
⊢ (if j = i then z else 0 j) =
    (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
        (a : 𝕜) → (a : ι) → 𝕜)
      z j
have neg : ∀ (h : ¬j = i),
  Eq.{u_1 + 1} (α := 𝕜) (0 j : 𝕜)
    ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
          (a : 𝕜) → (a : ι) → 𝕜)
        z j :
      𝕜)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Polynomial (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x
have add : ∀ (p q : 𝕜[X]) (hp : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x)
  (hq : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x q) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) q)) x),
  HasStrictDerivAt (fun (x : 𝕜) ↦ eval x (p + q)) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) (p + q))) x
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simpa using hp.add hq
  | monomial n a => simpa [mul_assoc, derivative_monomial]
                      using (hasStrictDerivAt_pow n x).const_mul a