awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
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
⊢ 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

Tactic:
rw [differentiableWithinAt_pi, Fin.forall_fin_succ, differentiableWithinAt_pi]

Premises used: differentiableWithinAt_pi, Fin.forall_fin_succ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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 := 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:
simp only [Fin.cons_zero, Fin.cons_succ]

Premises used: Fin.cons_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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

Tactic:
differentiableWithinAt_finCons

Premises used: differentiableWithinAt_finCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
h : DifferentiableWithinAt 𝕜 φ s x
hs : DifferentiableWithinAt 𝕜 φs s x
⊢ 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

Tactic:
differentiableWithinAt_finCons'.mpr ⟨h, hs⟩

Premises used: differentiableWithinAt_finCons', Iff.mpr, And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
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
⊢ 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

Tactic:
rw [differentiableAt_pi, Fin.forall_fin_succ, differentiableAt_pi]

Premises used: Fin.forall_fin_succ, differentiableAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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 := 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:
simp only [Fin.cons_zero, Fin.cons_succ]

Premises used: Fin.cons_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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

Tactic:
differentiableAt_finCons

Premises used: differentiableAt_finCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
h : DifferentiableAt 𝕜 φ x
hs : DifferentiableAt 𝕜 φs x
⊢ DifferentiableAt.{u_1, u_2, u_6} 𝕜 (F := (i : Fin (n + 1)) → F' i) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) x

Tactic:
differentiableAt_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, And.intro, differentiableAt_finCons'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
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
⊢ 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

Tactic:
rw [differentiableOn_pi, Fin.forall_fin_succ, differentiableOn_pi]

Premises used: differentiableOn_pi, Fin.forall_fin_succ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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 := 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:
simp only [Fin.cons_zero, Fin.cons_succ]

Premises used: Fin.cons_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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

Tactic:
differentiableOn_finCons

Premises used: differentiableOn_finCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
h : DifferentiableOn 𝕜 φ s
hs : DifferentiableOn 𝕜 φs s
⊢ DifferentiableOn.{u_1, u_2, u_6} 𝕜 (F := (i : Fin (n + 1)) → F' i) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) s

Tactic:
differentiableOn_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, differentiableOn_finCons', And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
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
⊢ (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

Tactic:
rw [differentiable_pi, Fin.forall_fin_succ, differentiable_pi]

Premises used: differentiable_pi, Fin.forall_fin_succ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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 := 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:
simp only [Fin.cons_zero, Fin.cons_succ]

Premises used: Fin.cons_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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

Tactic:
differentiable_finCons

Premises used: differentiable_finCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
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
h : Differentiable 𝕜 φ
hs : Differentiable 𝕜 φs
⊢ Differentiable.{u_1, u_2, u_6} 𝕜 (F := (i : Fin (n + 1)) → F' i) fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)

Tactic:
differentiable_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, differentiable_finCons', And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
L : Filter (E × E)
h : HasFDerivAtFilter f f' L
⊢ HasFDerivAtFilter f (ContinuousLinearMap.restrictScalars 𝕜 f') L

Tactic:
.of_isLittleO h.isLittleO

Premises used: HasFDerivAtFilter.isLittleO, HasFDerivAtFilter.of_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
h : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x

Tactic:
HasFDerivAtFilter.restrictScalars 𝕜 h

Premises used: HasStrictFDerivAt, HasFDerivAtFilter.restrictScalars
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
h : HasFDerivAt f f' x
⊢ HasFDerivAt f (ContinuousLinearMap.restrictScalars 𝕜 f') x

Tactic:
HasFDerivAtFilter.restrictScalars 𝕜 h

Premises used: HasFDerivAt, HasFDerivAtFilter.restrictScalars
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
h : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x

Tactic:
HasFDerivAtFilter.restrictScalars 𝕜 h

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.restrictScalars
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
x : E
h : DifferentiableAt 𝕜' f x
⊢ DifferentiableAt 𝕜 f x

Tactic:
(h.hasFDerivAt.restrictScalars 𝕜).differentiableAt

Premises used: HasFDerivAt.restrictScalars, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
h : DifferentiableWithinAt 𝕜' f s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
(h.hasFDerivWithinAt.restrictScalars 𝕜).differentiableWithinAt

Premises used: HasFDerivWithinAt.restrictScalars, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
h : DifferentiableOn 𝕜' f s
⊢ DifferentiableOn 𝕜 f s

Tactic:
fun x hx => (h x hx).restrictScalars 𝕜

Premises used: DifferentiableWithinAt.restrictScalars, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
h : Differentiable 𝕜' f
⊢ Differentiable 𝕜 f

Tactic:
fun x =>
  (h x).restrictScalars 𝕜

Premises used: Differentiable, DifferentiableAt.restrictScalars
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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 (ContinuousLinearMap.restrictScalars 𝕜 f') s x

Tactic:
rw [← H] at h
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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'
h₁ : HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x
⊢ ContinuousLinearMap.restrictScalars 𝕜 f' = g'

Tactic:
rw [← H] at h
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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 (ContinuousLinearMap.restrictScalars 𝕜 f') s x
H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x

Tactic:
.of_isLittleO h.isLittleO

Premises used: HasFDerivWithinAt.of_isLittleO, HasFDerivWithinAt.isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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 (ContinuousLinearMap.restrictScalars 𝕜 f') s x
H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x

Tactic:
exact .of_isLittleO h.isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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 (restrictScalars 𝕜 f') x

Tactic:
rw [← H] at h
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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'
h₁ : HasFDerivAt f (restrictScalars 𝕜 f') x
⊢ restrictScalars 𝕜 f' = g'

Tactic:
rw [← H] at h
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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 (restrictScalars 𝕜 f') x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivAt f f' x

Tactic:
.of_isLittleO h.isLittleO

Premises used: HasFDerivAt.of_isLittleO, HasFDerivAt.isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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 (restrictScalars 𝕜 f') x
H : restrictScalars 𝕜 f' = g'
⊢ HasFDerivAt f f' x

Tactic:
exact .of_isLittleO h.isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
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
x : E
h : DifferentiableAt 𝕜' f x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) (ContinuousLinearMap.restrictScalars 𝕜 (fderiv 𝕜' f x))

Tactic:
(h.hasFDerivAt.restrictScalars 𝕜).fderiv

Premises used: HasFDerivAt.restrictScalars, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv