awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
(hh₂.hasDerivWithinAt.comp x hh.hasDerivWithinAt hs).derivWithin hsx

Premises used: HasDerivWithinAt.comp, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
exact (hh₂.hasDerivWithinAt.comp x hh.hasDerivWithinAt hs).derivWithin hsx

Premises used: HasDerivWithinAt.comp, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s 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 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
y : 𝕜'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hy : h x = y
⊢ DifferentiableWithinAt 𝕜' h₂ s' (h x)

Tactic:
subst hy
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
derivWithin_comp x hh₂ hh hs

Premises used: derivWithin_comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s s'
hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
exact derivWithin_comp x hh₂ hh hs

Premises used: derivWithin_comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh₂ : DifferentiableAt 𝕜' h₂ (h x)
hh : DifferentiableAt 𝕜 h x
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Tactic:
(hh₂.hasDerivAt.comp x hh.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
y : 𝕜'
hh₂ : DifferentiableAt 𝕜' h₂ y
hh : DifferentiableAt 𝕜 h x
hy : h x = y
⊢ DifferentiableAt 𝕜' h₂ (h x)

Tactic:
subst hy
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableAt 𝕜 h x
hh₂ : DifferentiableAt 𝕜' h₂ (h x)
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Tactic:
deriv_comp x hh₂ hh

Premises used: deriv_comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableAt 𝕜 h x
hh₂ : DifferentiableAt 𝕜' h₂ (h x)
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Tactic:
exact deriv_comp x hh₂ hh

Premises used: deriv_comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
⊢ HasFDerivAtFilter f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) L

Tactic:
have := hf.hasFDerivAtFilter.iterate hL n
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
this : HasFDerivAtFilter f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) L
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : HasFDerivAtFilter (𝕜 := 𝕜) f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 (f' ^ n)) L),
    HasDerivAtFilter f^[n] (f' ^ n) L
⊢ HasDerivAtFilter f^[n] (f' ^ n) L

Tactic:
rwa [ContinuousLinearMap.toSpanSingleton_pow] at this

Premises used: ContinuousLinearMap.toSpanSingleton_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAt f f' x
hx : f x = x
n : ℕ
⊢ Tendsto (Prod.map f f) (SProd.sprod (β := Filter 𝕜) (𝓝 x) (pure x)) (SProd.sprod (β := Filter 𝕜) (𝓝 x) (pure x))

Tactic:
simpa [hx] using hf.continuousAt.tendsto.prodMap <| tendsto_pure_pure f x

Premises used: Filter.tendsto_pure_pure, HasDerivAt.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ HasFDerivWithinAt f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) s x

Tactic:
have := HasFDerivWithinAt.iterate hf hx hs n
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
this : HasFDerivWithinAt f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) s x
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : HasFDerivWithinAt (𝕜 := 𝕜) f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 (f' ^ n)) s x),
    HasDerivWithinAt f^[n] (f' ^ n) s x
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x

Tactic:
rwa [ContinuousLinearMap.toSpanSingleton_pow] at this

Premises used: ContinuousLinearMap.toSpanSingleton_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasStrictDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasStrictFDerivAt f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) x

Tactic:
have := hf.hasStrictFDerivAt.iterate hx n
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasStrictDerivAt f f' x
hx : f x = x
n : ℕ
this : HasStrictFDerivAt f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) x
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : HasStrictFDerivAt (𝕜 := 𝕜) f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 (f' ^ n)) x),
    HasStrictDerivAt f^[n] (f' ^ n) x
⊢ HasStrictDerivAt f^[n] (f' ^ n) x

Tactic:
rwa [ContinuousLinearMap.toSpanSingleton_pow] at this

Premises used: ContinuousLinearMap.toSpanSingleton_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
t : Set F
hl : HasFDerivWithinAt l l' t (f x)
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x

Tactic:
simpa using (hl.comp x hf.hasFDerivWithinAt hst).hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt l l' t (f x)

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
hl₁ : HasFDerivWithinAt l l' t (f x)
⊢ HasDerivWithinAt f f' s x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
hl₁ : HasFDerivWithinAt l l' t (f x)
hf₁ : HasDerivWithinAt f f' s x
⊢ MapsTo f s t

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
hl₁ : HasFDerivWithinAt l l' t (f x)
hf₁ : HasDerivWithinAt f f' s x
hst₁ : MapsTo f s t
⊢ y = f x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t (f x)
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x

Tactic:
hl.comp_hasDerivWithinAt x hf hst

Premises used: HasFDerivWithinAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t (f x)
hf : HasDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x

Tactic:
exact hl.comp_hasDerivWithinAt x hf hst

Premises used: HasFDerivWithinAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
t : Set F
hl : HasFDerivWithinAt l l' t (f x)
hf : HasDerivAt f f' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, f x' ∈ t
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
simpa using (hl.comp_hasFDerivAt x hf.hasFDerivAt ht).hasDerivAt

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.hasDerivAt, HasFDerivWithinAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
t : Set F
hl : HasFDerivWithinAt l l' t y
hf : HasDerivAt f f' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, f x' ∈ t
hy : y = f x
⊢ HasFDerivWithinAt l l' t (f x)

Tactic:
subst y
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
t : Set F
hf : HasDerivAt f f' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, f x' ∈ t
hl : HasFDerivWithinAt l l' t (f x)
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
hl.comp_hasDerivAt x hf ht

Premises used: HasFDerivWithinAt.comp_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
t : Set F
hf : HasDerivAt f f' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, f x' ∈ t
hl : HasFDerivWithinAt l l' t (f x)
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
exact hl.comp_hasDerivAt x hf ht

Premises used: HasFDerivWithinAt.comp_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
hl : HasFDerivAt l l' (f x)
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x

Tactic:
hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivWithinAt f f' s x
hy : y = f x
⊢ HasFDerivAt l l' (f x)

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivWithinAt f f' s x
hy : y = f x
hl₁ : HasFDerivAt l l' (f x)
⊢ HasDerivWithinAt f f' s x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivWithinAt f f' s x
hy : y = f x
hl₁ : HasFDerivAt l l' (f x)
hf₁ : HasDerivWithinAt f f' s x
⊢ y = f x

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivWithinAt f f' s x
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x

Tactic:
hl.comp_hasDerivWithinAt x hf

Premises used: HasFDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivWithinAt f f' s x
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x

Tactic:
exact hl.comp_hasDerivWithinAt x hf

Premises used: HasFDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
hl : HasFDerivAt l l' (f x)
hf : HasDerivAt f f' x
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
hasDerivWithinAt_univ.mp <| hl.comp_hasDerivWithinAt x hf.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, HasFDerivAt.comp_hasDerivWithinAt, hasDerivWithinAt_univ, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivAt f f' x
hy : y = f x
⊢ HasFDerivAt l l' (f x)

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

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

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivAt f f' x
hy : y = f x
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
hl.comp_hasDerivAt x hf

Premises used: HasFDerivAt.comp_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivAt f f' x
hy : y = f x
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
exact hl.comp_hasDerivAt x hf

Premises used: HasFDerivAt.comp_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
hl : HasStrictFDerivAt l l' (f x)
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
simpa using (hl.comp x hf.hasStrictFDerivAt).hasStrictDerivAt

Premises used: HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasStrictFDerivAt l l' y
hf : HasStrictDerivAt f f' x
hy : y = f x
⊢ HasStrictFDerivAt l l' (f x)

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

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

Tactic:
rw [hy] at hl
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasStrictFDerivAt l l' (f x)
hf : HasStrictDerivAt f f' x
hy : y = f x
⊢ HasStrictDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
hl.comp_hasStrictDerivAt x hf

Premises used: HasStrictFDerivAt.comp_hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasStrictFDerivAt l l' (f x)
hf : HasStrictDerivAt f f' x
hy : y = f x
⊢ HasStrictDerivAt (l ∘ f) ((l' : (a : F) → E) f') x

Tactic:
exact hl.comp_hasStrictDerivAt x hf

Premises used: HasStrictFDerivAt.comp_hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s 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
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)

Tactic:
(hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf.hasDerivWithinAt hs).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasFDerivWithinAt.comp_hasDerivWithinAt, DifferentiableWithinAt.hasFDerivWithinAt