awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivAt g₁ g₁' (h x)

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivWithinAt h h' s x
hy : y = h x
hg₁ : HasDerivAt g₁ g₁' (h x)
⊢ HasDerivWithinAt h h' s x

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivWithinAt h h' s x
hy : y = h x
hg₁ : HasDerivAt g₁ g₁' (h x)
hh₁ : HasDerivWithinAt h h' s x
⊢ y = h x

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
hg.scomp_hasDerivWithinAt x hh

Premises used: HasDerivAt.scomp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
exact hg.scomp_hasDerivWithinAt x hh

Premises used: HasDerivAt.scomp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
(HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh.hasDerivWithinAt hs).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
exact (HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh.hasDerivWithinAt hs).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ DifferentiableWithinAt 𝕜' g₁ t' (h x)

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
hg₁ : DifferentiableWithinAt 𝕜' g₁ t' (h x)
⊢ DifferentiableWithinAt 𝕜 h s x

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
hg₁ : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh₁ : DifferentiableWithinAt 𝕜 h s x
⊢ MapsTo h s t'

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
hg₁ : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh₁ : DifferentiableWithinAt 𝕜 h s x
hs₁ : MapsTo h s t'
⊢ y = h x

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
derivWithin.scomp x hg hh hs

Premises used: derivWithin.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
exact derivWithin.scomp x hg hh hs

Premises used: derivWithin.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableAt 𝕜' g₁ (h x)
hh : DifferentiableAt 𝕜 h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Tactic:
(HasDerivAt.scomp x hg.hasDerivAt hh.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ y
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ DifferentiableAt 𝕜' g₁ (h x)

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ y
hh : DifferentiableAt 𝕜 h x
hy : y = h x
hg₁ : DifferentiableAt 𝕜' g₁ (h x)
⊢ DifferentiableAt 𝕜 h x

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ y
hh : DifferentiableAt 𝕜 h x
hy : y = h x
hg₁ : DifferentiableAt 𝕜' g₁ (h x)
hh₁ : DifferentiableAt 𝕜 h x
⊢ y = h x

Tactic:
rw [hy] at hg
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ (h x)
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Tactic:
deriv.scomp x hg hh

Premises used: deriv.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ (h x)
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Tactic:
exact deriv.scomp x hg hh

Premises used: deriv.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
L'' : Filter (E × E)
hh₂ : HasDerivAtFilter h₂ h₂' L'
hf : HasFDerivAtFilter f f' L''
hL : Tendsto (Prod.map f f) L'' L'
⊢ HasFDerivAtFilter (h₂ ∘ f) (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.toSpanSingleton 𝕜' h₂') ∘SL f')
    L''

Tactic:
(hh₂.restrictScalars 𝕜).comp hf hL

Premises used: HasFDerivAtFilter.comp, HasFDerivAtFilter.restrictScalars
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
L'' : Filter (E × E)
hh₂ : HasDerivAtFilter h₂ h₂' L'
hf : HasFDerivAtFilter f f' L''
hL : Tendsto (Prod.map f f) L'' L'
h :
  Eq.{u_1 + 1} (α := AddCommGroup 𝕜') Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module 𝕜 𝕜') (NormedSpace.toModule : Module 𝕜 𝕜') (β := Module 𝕜 𝕜')
        (NormedSpace.toModule : Module 𝕜 𝕜') →
      Eq (α := (E →L[𝕜] 𝕜') → E →L[𝕜] 𝕜') (HSMul.hSMul h₂')
        (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.toSpanSingleton 𝕜' h₂')))
⊢ HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') L''

Tactic:
convert! (hh₂.restrictScalars 𝕜).comp hf hL

Premises used: HasFDerivAtFilter.comp, HasFDerivAtFilter.restrictScalars
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
L'' : Filter (E × E)
hh₂ : HasDerivAtFilter h₂ h₂' L'
hf : HasFDerivAtFilter f f' L''
hL : Tendsto (Prod.map f f) L'' L'
e_8 : Eq.{u_1 + 1} (α := AddCommGroup 𝕜') Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_9 :
  HEq (α := Module 𝕜 𝕜') (NormedSpace.toModule : Module 𝕜 𝕜') (β := Module 𝕜 𝕜') (NormedSpace.toModule : Module 𝕜 𝕜')
h :
  ∀ (x : E →L[𝕜] 𝕜') (x_1 : E),
    Eq.{u_1 + 1} (α := 𝕜') ((h₂' • x : (a : E) → 𝕜') x_1 : 𝕜')
      ((ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.toSpanSingleton 𝕜' h₂') ∘SL x : (a : E) → 𝕜') x_1 :
        𝕜')
⊢ Eq (α := (E →L[𝕜] 𝕜') → E →L[𝕜] 𝕜') (HSMul.hSMul h₂')
    (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.toSpanSingleton 𝕜' h₂')))

Tactic:
ext x
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
L'' : Filter (E × E)
hh₂ : HasDerivAtFilter h₂ h₂' L'
hf : HasFDerivAtFilter f f' L''
hL : Tendsto (Prod.map f f) L'' L'
e_8 : Eq.{u_1 + 1} (α := AddCommGroup 𝕜') Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_9 :
  HEq (α := Module 𝕜 𝕜') (NormedSpace.toModule : Module 𝕜 𝕜') (β := Module 𝕜 𝕜') (NormedSpace.toModule : Module 𝕜 𝕜')
x : E →L[𝕜] 𝕜'
x_1 : E
⊢ Eq.{u_1 + 1} (α := 𝕜') ((h₂' • x : (a : E) → 𝕜') x_1 : 𝕜')
    ((ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.toSpanSingleton 𝕜' h₂') ∘SL x : (a : E) → 𝕜') x_1 : 𝕜')

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L' : Filter 𝕜'
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (SProd.sprod (β := Filter 𝕜') L' (pure y))
hf : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L'' (pure x))
hL : Tendsto f L'' L'
hy : y = f x
⊢ Tendsto f (pure x) (pure y)

Tactic:
simp [hy]
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' (f x)
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
HasDerivAtFilter.comp_hasFDerivAtFilter hh hf <| hf.continuousAt.prodMap hf.continuousAt

Premises used: HasDerivAtFilter.comp_hasFDerivAtFilter, ContinuousAt.prodMap, HasStrictFDerivAt, HasStrictFDerivAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' y
hf : HasStrictFDerivAt f f' x
hy : y = f x
⊢ HasStrictDerivAt h₂ h₂' (f x)

Tactic:
rw [hy] at hh
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' y
hf : HasStrictFDerivAt f f' x
hy : y = f x
hh₁ : HasStrictDerivAt h₂ h₂' (f x)
⊢ HasStrictFDerivAt f f' x

Tactic:
rw [hy] at hh
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' y
hf : HasStrictFDerivAt f f' x
hy : y = f x
hh₁ : HasStrictDerivAt h₂ h₂' (f x)
hf₁ : HasStrictFDerivAt f f' x
⊢ y = f x

Tactic:
rw [hy] at hh
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' (f x)
hf : HasStrictFDerivAt f f' x
hy : y = f x
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
hh.comp_hasStrictFDerivAt x hf

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasStrictDerivAt h₂ h₂' (f x)
hf : HasStrictFDerivAt f f' x
hy : y = f x
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
exact hh.comp_hasStrictFDerivAt x hf

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
hh.comp_hasFDerivAtFilter hf <| hf.continuousAt.tendsto.prodMap <| tendsto_pure_pure _ _

Premises used: HasFDerivAt, HasDerivAtFilter.comp_hasFDerivAtFilter, Filter.tendsto_pure_pure, ContinuousAt.tendsto, HasFDerivAt.continuousAt, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivAt f f' x
hy : y = f x
⊢ HasDerivAt h₂ h₂' (f x)

Tactic:
rw [hy] at hh
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivAt f f' x
hy : y = f x
hh₁ : HasDerivAt h₂ h₂' (f x)
⊢ HasFDerivAt f f' x

Tactic:
rw [hy] at hh
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivAt f f' x
hy : y = f x
hh₁ : HasDerivAt h₂ h₂' (f x)
hf₁ : HasFDerivAt f f' x
⊢ y = f x

Tactic:
rw [hy] at hh
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivAt f f' x
hy : y = f x
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
hh.comp_hasFDerivAt x hf

Premises used: HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivAt f f' x
hy : y = f x
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
exact hh.comp_hasFDerivAt x hf

Premises used: HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
hh.comp_hasFDerivAtFilter hf <| hf.continuousWithinAt.tendsto.prodMap <| tendsto_pure_pure _ _

Premises used: HasDerivAtFilter.comp_hasFDerivAtFilter, Filter.tendsto_pure_pure, HasFDerivWithinAt, HasFDerivWithinAt.continuousWithinAt, ContinuousWithinAt.tendsto, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivWithinAt f f' s x
hy : y = f x
⊢ HasDerivAt h₂ h₂' (f x)

Tactic:
rw [hy] at hh
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivWithinAt f f' s x
hy : y = f x
hh₁ : HasDerivAt h₂ h₂' (f x)
⊢ HasFDerivWithinAt f f' s x

Tactic:
rw [hy] at hh