awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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)
rw₁ 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)
⊢ Eq (α := 𝔸 →L[𝕜] 𝔸) (fderivWithin 𝕜 (fun (x : 𝔸) ↦ x ^ n) s x)
    (∑ 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]

Premises used: fderivWithin_fun_pow', fderivWithin_fun_id, DifferentiableAt.differentiableWithinAt, differentiableAt_fun_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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 : ℕ
simp_rw : HSMul.hSMul (α := 𝔸) (∑ i ∈ Finset.range n, f x ^ (i + (n.pred - i))) f' = (n • f x ^ (n - 1)) • f'
⊢ ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f' = (n • f x ^ (n - 1)) • f'

Tactic:
simp_rw [op_smul_eq_smul, smul_smul, ← pow_add, ← Finset.sum_smul]

Premises used: Finset.sum_smul, pow_add, smul_smul, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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 : ℕ
rw : ∀ a ∈ Finset.range n, f x ^ (a + (n.pred - a)) = f x ^ (n - 1)
⊢ HSMul.hSMul (α := 𝔸) (∑ i ∈ Finset.range n, f x ^ (i + (n.pred - i))) f' = (n • f x ^ (n - 1)) • f'

Tactic:
rw [Finset.sum_eq_card_nsmul, Finset.card_range, smul_assoc]

Premises used: smul_assoc, Finset.card_range, Finset.sum_eq_card_nsmul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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
e_a : a + (n.pred - a) = n - 1
⊢ f x ^ (a + (n.pred - a)) = f x ^ (n - 1)

Tactic:
congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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
⊢ a + (n.pred - a) = n - 1

Tactic:
add_tsub_cancel_of_le (Nat.le_pred_of_lt <| Finset.mem_range.1 ha)

Premises used: Finset.mem_range, Nat.le_pred_of_lt, Iff.mp, Nat.pred, add_tsub_cancel_of_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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
⊢ a + (n.pred - a) = n - 1

Tactic:
exact add_tsub_cancel_of_le (Nat.le_pred_of_lt <| Finset.mem_range.1 ha)

Premises used: Finset.mem_range, Nat.le_pred_of_lt, Iff.mp, add_tsub_cancel_of_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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
h : HasStrictFDerivAt f f' x
n : ℕ
⊢ HasStrictFDerivAt (fun (x : E) ↦ f x ^ n) ((n • f x ^ (n - 1)) • f') x

Tactic:
h.pow' n |>.congr_fderiv <| aux_sum_eq_pow _

Premises used: HasStrictFDerivAt.pow', _private.0.aux_sum_eq_pow, HasStrictFDerivAt.congr_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
⊢ HasStrictFDerivAt (fun (x : 𝔸) ↦ x ^ n) (HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸))
    x

Tactic:
hasStrictFDerivAt_id _ |>.pow n

Premises used: HasStrictFDerivAt.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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
s : Set E
h : HasFDerivWithinAt f f' s x
n : ℕ
⊢ HasFDerivWithinAt (fun (x : E) ↦ f x ^ n) ((n • f x ^ (n - 1)) • f') s x

Tactic:
h.pow' n |>.congr_fderiv <| aux_sum_eq_pow _

Premises used: HasFDerivWithinAt.congr_fderiv, HasFDerivWithinAt.pow', _private.0.aux_sum_eq_pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
s : Set 𝔸
⊢ HasFDerivWithinAt (fun (x : 𝔸) ↦ x ^ n) (HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸))
    s x

Tactic:
hasFDerivWithinAt_id _ _ |>.pow n

Premises used: HasFDerivWithinAt.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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
h : HasFDerivAt f f' x
n : ℕ
⊢ HasFDerivAt (fun (x : E) ↦ f x ^ n) ((n • f x ^ (n - 1)) • f') x

Tactic:
h.pow' n |>.congr_fderiv <| aux_sum_eq_pow _

Premises used: HasFDerivAt.congr_fderiv, HasFDerivAt.pow', _private.0.aux_sum_eq_pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
⊢ HasFDerivAt (fun (x : 𝔸) ↦ x ^ n) (HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)) x

Tactic:
hasFDerivAt_id _ |>.pow n

Premises used: HasFDerivAt.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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 → 𝔸
x : E
n : ℕ
hf : DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 (f ^ n) x = HSMul.hSMul (β := E →L[𝕜] 𝔸) (n • f x ^ (n - 1)) (fderiv 𝕜 f x)

Tactic:
hf.hasFDerivAt.pow n |>.fderiv

Premises used: HasFDerivAt.pow, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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 𝕜 𝔸)
rw₁ rw₂ :
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸) =
    HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)
⊢ fderiv 𝕜 (fun (x : 𝔸) ↦ x ^ n) x = HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸)

Tactic:
rw [fderiv_fun_pow n differentiableAt_fun_id, fderiv_fun_id]

Premises used: fderiv_fun_id, fderiv_fun_pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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 → 𝔸
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
n : ℕ
hf : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (f ^ n) s x = HSMul.hSMul (β := E →L[𝕜] 𝔸) (n • f x ^ (n - 1)) (fderivWithin 𝕜 f s x)

Tactic:
hf.hasFDerivWithinAt.pow n |>.fderivWithin hxs

Premises used: HasFDerivWithinAt.pow, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
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 𝕜 𝔸)
rw₁ rw₂ :
  HSMul.hSMul (β := 𝔸 →L[𝕜] 𝔸) (n • x ^ (n - 1)) (ContinuousLinearMap.id 𝕜 𝔸) =
    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 𝕜 𝔸)

Tactic:
rw [fderivWithin_fun_pow hxs n differentiableAt_fun_id.differentiableWithinAt,
    fderivWithin_fun_id hxs]

Premises used: fderivWithin_fun_id, DifferentiableAt.differentiableWithinAt, fderivWithin_fun_pow, differentiableAt_fun_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
f₁' : E →L[𝕜] F
L : Filter (E × E)
f₂ : E → G
f₂' : E →L[𝕜] G
hf₁ : HasFDerivAtFilter f₁ f₁' L
hf₂ : HasFDerivAtFilter f₂ f₂' L
⊢ HasFDerivAtFilter (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) (f₁'.prod f₂') L

Tactic:
.of_isLittleO <| hf₁.isLittleO.prod_left hf₂.isLittleO

Premises used: setOf, Asymptotics.IsLittleO.prod_left, HasFDerivAtFilter.isLittleO, HasFDerivAtFilter.of_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
f₁' : E →L[𝕜] F
x : E
f₂ : E → G
f₂' : E →L[𝕜] G
hf₁ : HasStrictFDerivAt f₁ f₁' x
hf₂ : HasStrictFDerivAt f₂ f₂' x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) (f₁'.prod f₂') x

Tactic:
HasFDerivAtFilter.prodMk hf₁ hf₂

Premises used: HasFDerivAtFilter.prodMk, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
f₁' : E →L[𝕜] F
x : E
s : Set E
f₂ : E → G
f₂' : E →L[𝕜] G
hf₁ : HasFDerivWithinAt f₁ f₁' s x
hf₂ : HasFDerivWithinAt f₂ f₂' s x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) (f₁'.prod f₂') s x

Tactic:
hf₁.prodMk hf₂

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
f₁' : E →L[𝕜] F
x : E
f₂ : E → G
f₂' : E →L[𝕜] G
hf₁ : HasFDerivAt f₁ f₁' x
hf₂ : HasFDerivAt f₂ f₂' x
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) (f₁'.prod f₂') x

Tactic:
hf₁.prodMk hf₂

Premises used: HasFDerivAt, HasFDerivAtFilter.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e₀ : E
f₀ : F
⊢ HasFDerivAt (𝕜 := 𝕜) (F := E × F) (fun (e : E) ↦ (e, f₀)) (inl 𝕜 E F) e₀

Tactic:
(hasFDerivAt_id e₀).prodMk (hasFDerivAt_const f₀ e₀)

Premises used: hasFDerivAt_id, hasFDerivAt_const, HasFDerivAt.prodMk, ContinuousLinearMap.inl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e₀ : E
f₀ : F
⊢ HasFDerivAt (𝕜 := 𝕜) (F := E × F) (fun (f : F) ↦ (e₀, f)) (inr 𝕜 E F) f₀

Tactic:
(hasFDerivAt_const e₀ f₀).prodMk (hasFDerivAt_id f₀)

Premises used: hasFDerivAt_id, hasFDerivAt_const, ContinuousLinearMap.inr, HasFDerivAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
x : E
s : Set E
f₂ : E → G
hf₁ : DifferentiableWithinAt 𝕜 f₁ s x
hf₂ : DifferentiableWithinAt 𝕜 f₂ s x
⊢ DifferentiableWithinAt 𝕜 (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) s x

Tactic:
(hf₁.hasFDerivWithinAt.prodMk hf₂.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.prodMk, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
x : E
f₂ : E → G
hf₁ : DifferentiableAt 𝕜 f₁ x
hf₂ : DifferentiableAt 𝕜 f₂ x
⊢ DifferentiableAt 𝕜 (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) x

Tactic:
(hf₁.hasFDerivAt.prodMk hf₂.hasFDerivAt).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
s : Set E
f₂ : E → G
hf₁ : DifferentiableOn 𝕜 f₁ s
hf₂ : DifferentiableOn 𝕜 f₂ s
⊢ DifferentiableOn 𝕜 (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) s

Tactic:
fun x hx => (hf₁ x hx).prodMk (hf₂ x hx)

Premises used: DifferentiableWithinAt.prodMk, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
f₂ : E → G
hf₁ : Differentiable 𝕜 f₁
hf₂ : Differentiable 𝕜 f₂
⊢ Differentiable 𝕜 (F := F × G) fun (x : E) ↦ (f₁ x, f₂ x)

Tactic:
fun x ↦
  (hf₁ x).prodMk (hf₂ x)

Premises used: Differentiable, DifferentiableAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
x : E
f₂ : E → G
hf₁ : DifferentiableAt 𝕜 f₁ x
hf₂ : DifferentiableAt 𝕜 f₂ x
⊢ Eq (α := E →L[𝕜] F × G) (fderiv 𝕜 (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) x : E →L[𝕜] F × G)
    (ContinuousLinearMap.prod (fderiv 𝕜 f₁ x) (fderiv 𝕜 f₂ x) : E →L[𝕜] F × G)

Tactic:
(hf₁.hasFDerivAt.prodMk hf₂.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.prodMk
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₁ : E → F
x : E
s : Set E
f₂ : E → G
hf₁ : DifferentiableWithinAt 𝕜 f₁ s x
hf₂ : DifferentiableWithinAt 𝕜 f₂ s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F × G) (fderivWithin 𝕜 (F := F × G) (fun (x : E) ↦ (f₁ x, f₂ x)) s x : E →L[𝕜] F × G)
    (ContinuousLinearMap.prod (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f₂ s x) : E →L[𝕜] F × G)

Tactic:
(hf₁.hasFDerivWithinAt.prodMk hf₂.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.prodMk, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter ((E × F) × E × F)
⊢ HasFDerivAtFilter (𝕜 := 𝕜) Prod.fst (fst 𝕜 E F) L

Tactic:
(fst 𝕜 E F).hasFDerivAtFilter

Premises used: ContinuousLinearMap.hasFDerivAtFilter, ContinuousLinearMap.fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ HasStrictFDerivAt (𝕜 := 𝕜) Prod.fst (fst 𝕜 E F) p

Tactic:
hasFDerivAtFilter_fst

Premises used: hasFDerivAtFilter_fst, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasStrictFDerivAt (𝕜 := 𝕜) f₂ f₂' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ (f₂ x).1) (fst 𝕜 F G ∘SL f₂') x

Tactic:
hasStrictFDerivAt_fst.comp x h

Premises used: setOf, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : Filter (E × E)
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasFDerivAtFilter (𝕜 := 𝕜) f₂ f₂' L
⊢ HasFDerivAtFilter (fun (x : E) ↦ (f₂ x).1) (fst 𝕜 F G ∘SL f₂') L

Tactic:
hasFDerivAtFilter_fst.comp h tendsto_map

Premises used: setOf, HasFDerivAtFilter.comp, Filter.tendsto_map
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ HasFDerivAt (𝕜 := 𝕜) Prod.fst (fst 𝕜 E F) p

Tactic:
hasFDerivAtFilter_fst

Premises used: HasFDerivAt, hasFDerivAtFilter_fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasFDerivAt (𝕜 := 𝕜) f₂ f₂' x
⊢ HasFDerivAt (fun (x : E) ↦ (f₂ x).1) (fst 𝕜 F G ∘SL f₂') x

Tactic:
h.fst

Premises used: HasFDerivAt, HasFDerivAtFilter.fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
s : Set (E × F)
⊢ HasFDerivWithinAt (𝕜 := 𝕜) Prod.fst (fst 𝕜 E F) s p

Tactic:
hasFDerivAtFilter_fst

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasFDerivWithinAt (𝕜 := 𝕜) f₂ f₂' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ (f₂ x).1) (fst 𝕜 F G ∘SL f₂') s x

Tactic:
h.fst

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ DifferentiableAt 𝕜 Prod.fst p

Tactic:
hasFDerivAt_fst.differentiableAt

Premises used: HasFDerivAt.differentiableAt, hasFDerivAt_fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
h : DifferentiableAt 𝕜 f₂ x
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ (f₂ x).1) x

Tactic:
differentiableAt_fst.comp x h

Premises used: DifferentiableAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ Differentiable 𝕜 (E := E × F) Prod.fst

Tactic:
fun _ =>
  differentiableAt_fst

Premises used: Differentiable, differentiableAt_fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₂ : E → F × G
h : Differentiable 𝕜 f₂
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (x : E) ↦ (f₂ x).1

Tactic:
differentiable_fst.comp h

Premises used: Differentiable.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
s : Set (E × F)
⊢ DifferentiableWithinAt 𝕜 Prod.fst s p

Tactic:
differentiableAt_fst.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
f₂ : E → F × G
h : DifferentiableWithinAt 𝕜 f₂ s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ (f₂ x).1) s x

Tactic:
differentiableAt_fst.comp_differentiableWithinAt x h

Premises used: DifferentiableAt.comp_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set (E × F)
⊢ DifferentiableOn 𝕜 Prod.fst s

Tactic:
differentiable_fst.differentiableOn

Premises used: differentiable_fst, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f₂ : E → F × G
h : DifferentiableOn 𝕜 f₂ s
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ (f₂ x).1) s

Tactic:
differentiable_fst.comp_differentiableOn h

Premises used: Differentiable.comp_differentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ Eq (α := E × F →L[𝕜] E) (fderiv 𝕜 Prod.fst p : E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E)

Tactic:
hasFDerivAt_fst.fderiv

Premises used: HasFDerivAt.fderiv, hasFDerivAt_fst