awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (hypothesis)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n_1 n : ℕ
⊢ HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
have this : HasStrictFDerivAt (f * f ^ (n + 1))
  (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
Tactic: have := h.mul' (h.pow' (n + 1))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n_1 n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
have simp_rw : HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
  (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
Tactic: simp_rw [pow_succ' _ (n + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (hypothesis)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n_1 n : ℕ
⊢ HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s x
have this : HasFDerivWithinAt (f * f ^ (n + 1))
  (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x
Tactic: have := h.mul' (h.pow' (n + 1))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n_1 n : ℕ
this :
  HasFDerivWithinAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x
⊢ HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s x
have simp_rw : HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
  (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s x
Tactic: simp_rw [pow_succ' _ (n + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (hypothesis)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n_1 n : ℕ
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
have this : HasFDerivAt (f * f ^ (n + 1))
  (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
Tactic: have := h.mul' (h.pow' (n + 1))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n_1 n : ℕ
this :
  HasFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
have simp_rw : HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
  (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
Tactic: simp_rw [pow_succ' _ (n + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
x : 𝔸
n : ℕ
⊢ Eq (α := 𝔸 →L[𝕜] 𝔸) (fderiv 𝕜 (fun (x : 𝔸) ↦ x ^ n) x)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
have rw : Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> fderiv 𝕜 (fun (x : 𝔸) ↦ x) x <• x ^ i)
  (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
Tactic: rw [fderiv_fun_pow' n differentiableAt_fun_id, fderiv_fun_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
x : 𝔸
n : ℕ
rw :
  Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> fderiv 𝕜 (fun (x : 𝔸) ↦ x) x <• x ^ i)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
⊢ Eq (α := 𝔸 →L[𝕜] 𝔸) (fderiv 𝕜 (fun (x : 𝔸) ↦ x ^ n) x)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
have rw₁ : Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
  (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
Tactic: rw [fderiv_fun_pow' n differentiableAt_fun_id, fderiv_fun_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
s : Set 𝔸
x : 𝔸
n : ℕ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝔸 →L[𝕜] 𝔸) (fderivWithin 𝕜 (fun (x : 𝔸) ↦ x ^ n) s x)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
have rw : Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> fderivWithin 𝕜 (fun (x : 𝔸) ↦ x) s x <• x ^ i)
  (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
Tactic: rw [fderivWithin_fun_pow' hxs n differentiableAt_fun_id.differentiableWithinAt,
    fderivWithin_fun_id hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
s : Set 𝔸
x : 𝔸
n : ℕ
hxs : UniqueDiffWithinAt 𝕜 s x
rw :
  Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> fderivWithin 𝕜 (fun (x : 𝔸) ↦ x) s x <• x ^ i)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
⊢ Eq (α := 𝔸 →L[𝕜] 𝔸) (fderivWithin 𝕜 (fun (x : 𝔸) ↦ x ^ n) s x)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
have rw₁ : Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
  (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
Tactic: rw [fderivWithin_fun_pow' hxs n differentiableAt_fun_id.differentiableWithinAt,
    fderivWithin_fun_id hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f' = (n • f x ^ (n - 1)) • f'
have simp_rw : HSMul.hSMul (α := 𝔸) (∑ i ∈ Finset.range n, f x ^ (i + (n.pred - i))) f' = (n • f x ^ (n - 1)) • f'
Tactic: simp_rw [op_smul_eq_smul, smul_smul, ← pow_add, ← Finset.sum_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ HSMul.hSMul (α := 𝔸) (∑ i ∈ Finset.range n, f x ^ (i + (n.pred - i))) f' = (n • f x ^ (n - 1)) • f'
have rw : ∀ a ∈ Finset.range n, f x ^ (a + (n.pred - a)) = f x ^ (n - 1)
Tactic: rw [Finset.sum_eq_card_nsmul, Finset.card_range, smul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n a : ℕ
ha : a ∈ Finset.range n
⊢ f x ^ (a + (n.pred - a)) = f x ^ (n - 1)
have e_a : a + (n.pred - a) = n - 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
x : 𝔸
n : ℕ
⊢ fderiv 𝕜 (fun (x : 𝔸) ↦ x ^ n) x = HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
have rw : HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (fderiv 𝕜 (fun (x : 𝔸) ↦ x) x) =
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
Tactic: rw [fderiv_fun_pow n differentiableAt_fun_id, fderiv_fun_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
x : 𝔸
n : ℕ
rw :
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (fderiv 𝕜 (fun (x : 𝔸) ↦ x) x) =
    HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
⊢ fderiv 𝕜 (fun (x : 𝔸) ↦ x ^ n) x = HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
have rw₁ : HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸) =
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
Tactic: rw [fderiv_fun_pow n differentiableAt_fun_id, fderiv_fun_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
s : Set 𝔸
x : 𝔸
n : ℕ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun (x : 𝔸) ↦ x ^ n) s x = HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
have rw : HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (fderivWithin 𝕜 (fun (x : 𝔸) ↦ x) s x) =
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
Tactic: rw [fderivWithin_fun_pow hxs n differentiableAt_fun_id.differentiableWithinAt,
    fderivWithin_fun_id hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
s : Set 𝔸
x : 𝔸
n : ℕ
hxs : UniqueDiffWithinAt 𝕜 s x
rw :
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (fderivWithin 𝕜 (fun (x : 𝔸) ↦ x) s x) =
    HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
⊢ fderivWithin 𝕜 (fun (x : 𝔸) ↦ x ^ n) s x = HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
have rw₁ : HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸) =
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
Tactic: rw [fderivWithin_fun_pow hxs n differentiableAt_fun_id.differentiableWithinAt,
    fderivWithin_fun_id hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (F' i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
⊢ DifferentiableWithinAt 𝕜 (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) s' f
have h : HasFDerivWithinAt (𝕜 := 𝕜) (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) (proj (φ := F') i) s' f
Tactic: apply HasFDerivWithinAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (F' i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
h : HasFDerivWithinAt (𝕜 := 𝕜) (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) (proj (φ := F') i) s' f
⊢ DifferentiableWithinAt 𝕜 (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) s' f
have f' : ((i : ι) → F' i) →L[𝕜] F' i
Tactic: apply HasFDerivWithinAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
l : Filter (E × E)
⊢ HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' l ↔
    HasFDerivAtFilter φ (proj (φ := F') 0 ∘SL φ') l ∧
      HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l
have rw : (HasFDerivAtFilter (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) (proj (φ := F') 0 ∘SL φ') l ∧
    ∀ (i : Fin n),
      HasFDerivAtFilter (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) (proj (φ := F') i.succ ∘SL φ') l) ↔
  HasFDerivAtFilter φ (proj (φ := F') 0 ∘SL φ') l ∧
    ∀ (i : Fin n),
      HasFDerivAtFilter (fun (x : E) ↦ φs x i)
        (comp (σ₂₃ := RingHom.id 𝕜) (proj (φ := fun (i : Fin n) ↦ F' i.succ) i) (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ')) l
Tactic: rw [hasFDerivAtFilter_pi', Fin.forall_fin_succ, hasFDerivAtFilter_pi']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
l : Filter (E × E)
⊢ (HasFDerivAtFilter (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) (proj (φ := F') 0 ∘SL φ') l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) (proj (φ := F') i.succ ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj (φ := F') 0 ∘SL φ') l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun (x : E) ↦ φs x i)
          (comp (σ₂₃ := RingHom.id 𝕜) (proj (φ := fun (i : Fin n) ↦ F' i.succ) i) (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ'))
          l
have dsimp : (HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0)
      { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x 0, map_add' := sorry, map_smul' := sorry, cont := sorry }
      l ∧
    ∀ (i : Fin n),
      HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' i.succ) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ)
        { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x i.succ, map_add' := sorry, map_smul' := sorry,
          cont := sorry }
        l) ↔
  HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) φ
      { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x 0, map_add' := sorry, map_smul' := sorry, cont := sorry }
      l ∧
    ∀ (i : Fin n),
      HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' i.succ) (fun (x : E) ↦ φs x i)
        { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x i.succ, map_add' := sorry, map_smul' := sorry,
          cont := sorry }
        l
Tactic: dsimp [ContinuousLinearMap.comp, LinearMap.comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableWithinAt.{u_1, u_2, u_6} 𝕜 (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) s x ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x
have rw : (DifferentiableWithinAt.{u_1, u_2, u_6} 𝕜 (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) s x ∧
    ∀ (i : Fin n),
      DifferentiableWithinAt.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) s
        x) ↔
  DifferentiableWithinAt 𝕜 φ s x ∧
    ∀ (i : Fin n), DifferentiableWithinAt.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) (fun (x : E) ↦ φs x i) s x
Tactic: rw [differentiableWithinAt_pi, Fin.forall_fin_succ, differentiableWithinAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableAt.{u_1, u_2, u_6} 𝕜 (F := (i : Fin (n + 1)) → F' i) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) x ↔
    DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x
have rw : (DifferentiableAt.{u_1, u_2, u_6} 𝕜 (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) x ∧
    ∀ (i : Fin n),
      DifferentiableAt.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) x) ↔
  DifferentiableAt 𝕜 φ x ∧ ∀ (i : Fin n), DifferentiableAt.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) (fun (x : E) ↦ φs x i) x
Tactic: rw [differentiableAt_pi, Fin.forall_fin_succ, differentiableAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableOn.{u_1, u_2, u_6} 𝕜 (F := (i : Fin (n + 1)) → F' i) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) s ↔
    DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s
have rw : (DifferentiableOn.{u_1, u_2, u_6} 𝕜 (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) s ∧
    ∀ (i : Fin n),
      DifferentiableOn.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) s) ↔
  DifferentiableOn 𝕜 φ s ∧ ∀ (i : Fin n), DifferentiableOn.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) (fun (x : E) ↦ φs x i) s
Tactic: rw [differentiableOn_pi, Fin.forall_fin_succ, differentiableOn_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Prod (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (Differentiable.{u_1, u_2, u_6} 𝕜 (F := (i : Fin (n + 1)) → F' i) fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) ↔
    Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs
have rw : ((Differentiable.{u_1, u_2, u_6} 𝕜 (F := F' 0) fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) ∧
    ∀ (i : Fin n),
      Differentiable.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) ↔
  Differentiable 𝕜 φ ∧ ∀ (i : Fin n), Differentiable.{u_1, u_2, u_6} 𝕜 (F := F' i.succ) fun (x : E) ↦ φs x i
Tactic: rw [differentiable_pi, Fin.forall_fin_succ, differentiable_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.RestrictScalars (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f g' s x
H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x
have h₁ : HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x
Tactic: rw [← H] at h
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.RestrictScalars (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
x : E
g' : E →L[𝕜] F
h : HasFDerivAt f g' x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivAt f f' x
have h₁ : HasFDerivAt f (restrictScalars 𝕜 f') x
Tactic: rw [← H] at h
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ DifferentiableWithinAt 𝕜' f s x ↔
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)
have mp : DifferentiableWithinAt 𝕜' f s x → ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.RestrictScalars (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜' E
inst_6 : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedSpace 𝕜' F
inst_10 : IsScalarTower 𝕜 𝕜' F
f : E → F
s : Set E
x : E
hf : DifferentiableWithinAt 𝕜 f s x
hs : UniqueDiffWithinAt 𝕜 s x
mp :
  DifferentiableWithinAt 𝕜' f s x →
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)
⊢ DifferentiableWithinAt 𝕜' f s x ↔
    ∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)
have mpr : (∃ (g' : E →L[𝕜'] F), Eq (α := E →L[𝕜] F) (restrictScalars 𝕜 g') (fderivWithin 𝕜 f s x)) →
  DifferentiableWithinAt 𝕜' f s x
Tactic: constructor