awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
⊢ ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)

Tactic:
have hR (k : 𝕜) : R k = σ' k := rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
⊢ HasFDerivAt ((⇑L : (a : F) → F') ∘ f ∘ (⇑R : (a : 𝕜) → 𝕜)) (L ∘SL toSpanSingleton 𝕜 f' ∘SL R) ((σ : (a : 𝕜) → 𝕜) x)

Tactic:
HasFDerivAt.comp_semilinear L R (f' := toSpanSingleton 𝕜 f') ?_

Premises used: HasFDerivAt.comp_semilinear
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
h :
  Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜) →
      toSpanSingleton 𝕜 ((L : (a : F) → F') f') = L ∘SL toSpanSingleton 𝕜 f' ∘SL R
convert_3 : HasFDerivAt (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') ((R : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
⊢ HasFDerivAt.{u, u, u_1} (𝕜 := 𝕜) (E := 𝕜) (F := F') ((⇑L : (a : F) → F') ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → F')
    (toSpanSingleton 𝕜 ((L : (a : F) → F') f') : 𝕜 →L[𝕜] F') ((σ : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
convert! HasFDerivAt.comp_semilinear L R (f' := toSpanSingleton 𝕜 f') ?_

Premises used: HasFDerivAt.comp_semilinear
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
e_4 : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜)
h :
  Eq.{u_1 + 1} (α := F') (((toSpanSingleton 𝕜 ((L : (a : F) → F') f') : 𝕜 →L[𝕜] F') : (a : 𝕜) → F') 1 : F')
    ((L ∘SL toSpanSingleton 𝕜 f' ∘SL R : (a : 𝕜) → F') 1 : F')
⊢ toSpanSingleton 𝕜 ((L : (a : F) → F') f') = L ∘SL toSpanSingleton 𝕜 f' ∘SL R

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
e_4 : Eq.{u + 1} (α := AddCommGroup 𝕜) Ring.toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq.{u + 1} (α := Module 𝕜 𝕜) Semiring.toModule (β := Module 𝕜 𝕜) (NormedSpace.toModule : Module 𝕜 𝕜)
⊢ Eq.{u_1 + 1} (α := F') (((toSpanSingleton 𝕜 ((L : (a : F) → F') f') : 𝕜 →L[𝕜] F') : (a : 𝕜) → F') 1 : F')
    ((L ∘SL toSpanSingleton 𝕜 f' ∘SL R : (a : 𝕜) → F') 1 : F')

Tactic:
simp [R]
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
this : RingHomIsometric σ'
R : 𝕜 →SL[σ'] 𝕜 := { toLinearMap := σ'.toSemilinearMap, cont := ⋯ }
hR : ∀ (k : 𝕜), Eq (α := 𝕜) ((R : (a : 𝕜) → 𝕜) k : 𝕜) ((σ' : (a : 𝕜) → 𝕜) k : 𝕜)
convert_3 : HasDerivAt f f' ((R : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
convert_3₁ : HasDerivAt f f' ((σ' : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
convert_3₂ convert_3₃ convert_3₄ convert_3₅ : HasDerivAt f f' x
⊢ HasFDerivAt (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') ((R : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))

Tactic:
rwa [← hasDerivAt_iff_hasFDerivAt, hR, RingHomInvPair.comp_apply_eq]

Premises used: RingHomInvPair.comp_apply_eq, hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_3 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt.{u, u, u_1} 𝕜 (E := 𝕜) (F := F') ((⇑L : (a : F) → F') ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → F')
    ((σ : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
(hf.hasDerivAt.comp_semilinear σ' L).differentiableAt

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, HasDerivAt.comp_semilinear
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_1 : RingHomIsometric σ
inst_2 : RingHomInvPair σ σ'
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAt f f' x
⊢ HasDerivAt (𝕜 := 𝕜) (F := 𝕜) ((⇑σ : (a : 𝕜) → 𝕜) ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → 𝕜) ((σ : (a : 𝕜) → 𝕜) f' : 𝕜)
    ((σ : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
hf.comp_semilinear σ' ⟨σ.toSemilinearMap, σ.isometry.continuous⟩

Premises used: ContinuousLinearMap.mk, RingHom.isometry, Isometry.continuous, RingHom.toSemilinearMap, HasDerivAt.comp_semilinear
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
σ σ' : 𝕜 →+* 𝕜
inst_1 : RingHomIsometric σ
inst_2 : RingHomInvPair σ σ'
f : 𝕜 → 𝕜
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (E := 𝕜) (F := 𝕜) ((⇑σ : (a : 𝕜) → 𝕜) ∘ f ∘ (⇑σ' : (a : 𝕜) → 𝕜) : 𝕜 → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
(hf.hasDerivAt.comp_ringHom σ σ').differentiableAt

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, HasDerivAt.comp_ringHom
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
L' : Filter (𝕜' × 𝕜')
hg : HasDerivAtFilter g₁ g₁' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (g₁ ∘ h) (h' • g₁') L

Tactic:
simpa using ((hg.hasFDerivAtFilter.restrictScalars 𝕜).comp hh hL).hasDerivAtFilter

Premises used: HasFDerivAtFilter.comp, HasDerivAtFilter.hasFDerivAtFilter, HasFDerivAtFilter.restrictScalars, HasFDerivAtFilter.hasDerivAtFilter
-- 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
L : Filter 𝕜
L' : Filter 𝕜'
hg : HasDerivAtFilter g₁ g₁' (SProd.sprod (β := Filter 𝕜') L' (pure y))
hh : HasDerivAtFilter h h' (SProd.sprod (β := Filter 𝕜) L (pure x))
hy : y = h x
hL : Tendsto h L L'
⊢ Tendsto h (pure x) (pure y)

Tactic:
simp [hy]
-- 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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
hg.scomp hh <| .prodMap (tendsto_nhdsWithin_iff.mpr ⟨hh.continuousAt, .of_forall hs⟩)
    (tendsto_pure_pure _ _)

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, HasDerivAt, Filter.tendsto_pure_pure, Filter.Eventually.of_forall, HasDerivAtFilter.scomp, HasDerivAt.continuousAt, And.intro, Filter.Tendsto.prodMap
-- 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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' y
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivWithinAt g₁ g₁' s' (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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' y
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
hg₁ : HasDerivWithinAt g₁ g₁' s' (h x)
⊢ HasDerivAt h 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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' y
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
hg₁ : HasDerivWithinAt g₁ g₁' s' (h x)
hh₁ : HasDerivAt h h' x
⊢ ∀ (x : 𝕜), h x ∈ s'

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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' y
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
hg₁ : HasDerivWithinAt g₁ g₁' s' (h x)
hh₁ : HasDerivAt h h' x
hs₁ : ∀ (x : 𝕜), h x ∈ s'
⊢ 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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
hg.scomp_hasDerivAt x hh hs

Premises used: HasDerivWithinAt.scomp_hasDerivAt
-- 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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
exact hg.scomp_hasDerivAt x hh hs

Premises used: HasDerivWithinAt.scomp_hasDerivAt
-- 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
HasDerivAtFilter.scomp hg hh <| hh.continuousWithinAt.tendsto_nhdsWithin hst |>.prodMap <|
    tendsto_pure_pure ..

Premises used: Filter.tendsto_pure_pure, HasDerivWithinAt, ContinuousWithinAt.tendsto_nhdsWithin, HasDerivAtFilter.scomp, HasDerivWithinAt.continuousWithinAt, Filter.Tendsto.prodMap
-- 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt g₁ 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
hg₁ : HasDerivWithinAt g₁ g₁' t' (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
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
hg₁ : HasDerivWithinAt g₁ g₁' t' (h x)
hh₁ : HasDerivWithinAt h 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
hg₁ : HasDerivWithinAt g₁ g₁' t' (h x)
hh₁ : HasDerivWithinAt h h' s x
hst₁ : 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
hg.scomp x hh hst

Premises used: 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
exact hg.scomp x hh hst

Premises used: 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 : 𝕜
𝕜' : Type u_1
inst_3 : NontriviallyNormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : NormedSpace 𝕜' F
inst_6 : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
HasDerivAtFilter.scomp hg hh <| hh.continuousAt.tendsto.prodMap <| tendsto_pure_pure _ _

Premises used: HasDerivAt, Filter.tendsto_pure_pure, HasDerivAtFilter.scomp, HasDerivAt.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.prodMap
-- 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivAt h h' 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 : 𝕜
𝕜' : 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 : HasDerivAt h h' x
hy : y = h x
hg₁ : HasDerivAt g₁ g₁' (h x)
⊢ HasDerivAt h 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivAt h h' x
hy : y = h x
hg₁ : HasDerivAt g₁ g₁' (h x)
hh₁ : HasDerivAt h 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
hg.scomp x hh

Premises used: 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
exact hg.scomp x hh

Premises used: 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
HasDerivAtFilter.scomp hg hh <|
    hh.hasStrictFDerivAt.continuousAt.prodMap hh.hasStrictFDerivAt.continuousAt

Premises used: ContinuousAt.prodMap, HasDerivAtFilter.scomp, HasStrictDerivAt.hasStrictFDerivAt, HasStrictDerivAt, HasStrictFDerivAt.continuousAt
-- 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' y
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt 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 : 𝕜
𝕜' : 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 : HasStrictDerivAt g₁ g₁' y
hh : HasStrictDerivAt h h' x
hy : y = h x
hg₁ : HasStrictDerivAt g₁ g₁' (h x)
⊢ HasStrictDerivAt h 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' y
hh : HasStrictDerivAt h h' x
hy : y = h x
hg₁ : HasStrictDerivAt g₁ g₁' (h x)
hh₁ : HasStrictDerivAt h 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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
hg.scomp x hh

Premises used: HasStrictDerivAt.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 : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
exact hg.scomp x hh

Premises used: HasStrictDerivAt.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
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivWithinAt h h' s x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh (mapsTo_univ _ _)

Premises used: HasDerivAt.hasDerivWithinAt, Set.mapsTo_univ, HasDerivWithinAt.scomp