awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hf₁ : HasFDerivWithinAt f f' s 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[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivWithinAt f f' s x
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
hh.comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt
-- 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₂' (f x)
hf : HasFDerivWithinAt f f' s x
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
exact hh.comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt
-- 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
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
hh.comp_hasFDerivAtFilter hf <| hf.continuousWithinAt.tendsto_nhdsWithin hst |>.prodMap <|
    tendsto_pure_pure _ _

Premises used: HasDerivAtFilter.comp_hasFDerivAtFilter, Filter.tendsto_pure_pure, HasFDerivWithinAt, ContinuousWithinAt.tendsto_nhdsWithin, HasFDerivWithinAt.continuousWithinAt, 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
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t y
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasDerivWithinAt h₂ h₂' t (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
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t y
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
hh₁ : HasDerivWithinAt h₂ h₂' t (f x)
⊢ HasFDerivWithinAt f f' s 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
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t y
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
hh₁ : HasDerivWithinAt h₂ h₂' t (f x)
hf₁ : HasFDerivWithinAt f f' s x
⊢ MapsTo f s t

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
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t y
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
hh₁ : HasDerivWithinAt h₂ h₂' t (f x)
hf₁ : HasFDerivWithinAt f f' s x
hst₁ : MapsTo f s t
⊢ 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[𝕜] 𝕜'
s : Set E
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
hh.comp_hasFDerivWithinAt x hf hst

Premises used: HasDerivWithinAt.comp_hasFDerivWithinAt
-- 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
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
exact hh.comp_hasFDerivWithinAt x hf hst

Premises used: HasDerivWithinAt.comp_hasFDerivWithinAt
-- 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[𝕜] 𝕜'
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t (f x)
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
hh.comp_hasFDerivAtFilter hf <| tendsto_nhdsWithin_iff.mpr ⟨hf.continuousAt, ht⟩ |>.prodMap <|
    tendsto_pure_pure _ _

Premises used: Iff.mpr, HasFDerivAt, HasDerivAtFilter.comp_hasFDerivAtFilter, tendsto_nhdsWithin_iff, Filter.tendsto_pure_pure, And.intro, 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[𝕜] 𝕜'
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t y
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hy : y = f x
⊢ HasDerivWithinAt h₂ h₂' t (f x)

Tactic:
subst y
-- 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[𝕜] 𝕜'
t : Set 𝕜'
x : E
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hh : HasDerivWithinAt h₂ h₂' t (f x)
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
hh.comp_hasFDerivAt x hf ht

Premises used: HasDerivWithinAt.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[𝕜] 𝕜'
t : Set 𝕜'
x : E
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hh : HasDerivWithinAt h₂ h₂' t (f x)
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
exact hh.comp_hasFDerivAt x hf ht

Premises used: HasDerivWithinAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
hh₂ : HasDerivAtFilter h₂ h₂' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
rw : HasDerivAtFilter (h₂ ∘ h) (h' * h₂') L
⊢ HasDerivAtFilter (h₂ ∘ h) (h₂' * h') L

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
hh₂ : HasDerivAtFilter h₂ h₂' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h' * h₂') L

Tactic:
hh₂.scomp hh hL

Premises used: HasDerivAtFilter.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
hh₂ : HasDerivAtFilter h₂ h₂' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h' * h₂') L

Tactic:
exact hh₂.scomp hh hL

Premises used: HasDerivAtFilter.scomp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
L : Filter 𝕜
L' : Filter 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' (SProd.sprod (β := Filter 𝕜') L' (pure y))
hh : HasDerivAtFilter h h' (SProd.sprod (β := Filter 𝕜) L (pure x))
hL : Tendsto h L L'
hy : y = h x
⊢ Tendsto h (pure x) (pure y)

Tactic:
simp [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₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
rw : HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x

Tactic:
hh₂.scomp x hh hst

Premises used: HasDerivWithinAt.scomp
-- 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₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x

Tactic:
exact hh₂.scomp x hh hst

Premises used: HasDerivWithinAt.scomp
-- 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₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
⊢ HasDerivWithinAt h₂ h₂' s' (h x)

Tactic:
rw [hy] at hh₂
-- 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₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
hh₃ : HasDerivWithinAt h₂ h₂' s' (h x)
⊢ HasDerivWithinAt h h' s x

Tactic:
rw [hy] at hh₂
-- 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₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
hh₃ : HasDerivWithinAt h₂ h₂' s' (h x)
hh₁ : HasDerivWithinAt h h' s x
⊢ MapsTo h s s'

Tactic:
rw [hy] at hh₂
-- 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₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' y
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
hh₃ : HasDerivWithinAt h₂ h₂' s' (h x)
hh₁ : HasDerivWithinAt h h' s x
hst₁ : MapsTo h s s'
⊢ y = h x

Tactic:
rw [hy] at hh₂
-- 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₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
hh₂.comp x hh hst

Premises used: HasDerivWithinAt.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₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
exact hh₂.comp x hh hst

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

Tactic:
HasDerivAtFilter.comp hh₂ hh <| hh.continuousAt.tendsto.prodMap <| tendsto_pure_pure _ _

Premises used: HasDerivAt, Filter.tendsto_pure_pure, HasDerivAt.continuousAt, ContinuousAt.tendsto, HasDerivAtFilter.comp, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' y
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt h₂ h₂' (h x)

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' y
hh : HasDerivAt h h' x
hy : y = h x
hh₃ : HasDerivAt h₂ h₂' (h x)
⊢ HasDerivAt h h' x

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' y
hh : HasDerivAt h h' x
hy : y = h x
hh₃ : HasDerivAt h₂ h₂' (h x)
hh₁ : HasDerivAt h h' x
⊢ y = h x

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
hh₂.comp x hh

Premises used: 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₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
exact hh₂.comp x hh

Premises used: 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₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
rw : HasStrictDerivAt (h₂ ∘ h) (h' * h₂') x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
rw [mul_comm]

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

Tactic:
hh₂.scomp x hh

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

Tactic:
exact hh₂.scomp x hh

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

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' y
hh : HasStrictDerivAt h h' x
hy : y = h x
hh₃ : HasStrictDerivAt h₂ h₂' (h x)
⊢ HasStrictDerivAt h h' x

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' y
hh : HasStrictDerivAt h h' x
hy : y = h x
hh₃ : HasStrictDerivAt h₂ h₂' (h x)
hh₁ : HasStrictDerivAt h h' x
⊢ y = h x

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
hh₂.comp x hh

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

Tactic:
exact hh₂.comp x hh

Premises used: HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivWithinAt h h' s x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
hh₂.hasDerivWithinAt.comp x hh (mapsTo_univ _ _)

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

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' y
hh : HasDerivWithinAt h h' s x
hy : y = h x
hh₃ : HasDerivAt h₂ h₂' (h x)
⊢ HasDerivWithinAt h h' s x

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' y
hh : HasDerivWithinAt h h' s x
hy : y = h x
hh₃ : HasDerivAt h₂ h₂' (h x)
hh₁ : HasDerivWithinAt h h' s x
⊢ y = h x

Tactic:
rw [hy] at hh₂
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
hh₂.comp_hasDerivWithinAt x hh

Premises used: HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
exact hh₂.comp_hasDerivWithinAt x hh

Premises used: HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
t : Set 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' t (h x)
hh : HasDerivAt h h' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, h x' ∈ t
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
HasDerivAtFilter.comp hh₂ hh <| tendsto_nhdsWithin_iff.mpr ⟨hh.continuousAt, ht⟩ |>.prodMap <|
    tendsto_pure_pure _ _

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, HasDerivAt, Filter.tendsto_pure_pure, HasDerivAt.continuousAt, And.intro, HasDerivAtFilter.comp, Filter.Tendsto.prodMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
t : Set 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' t y
hh : HasDerivAt h h' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, h x' ∈ t
hy : y = h x
⊢ HasDerivWithinAt h₂ h₂' t (h x)

Tactic:
subst y
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
t : Set 𝕜'
hh : HasDerivAt h h' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, h x' ∈ t
hh₂ : HasDerivWithinAt h₂ h₂' t (h x)
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
hh₂.comp_hasDerivAt x hh ht

Premises used: HasDerivWithinAt.comp_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Comp
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
t : Set 𝕜'
hh : HasDerivAt h h' x
ht : ∀ᶠ (x' : 𝕜) in 𝓝 x, h x' ∈ t
hh₂ : HasDerivWithinAt h₂ h₂' t (h x)
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
exact hh₂.comp_hasDerivAt x hh ht

Premises used: HasDerivWithinAt.comp_hasDerivAt
-- 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'
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt