awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
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 (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') ((R : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
have convert_3 : HasDerivAt f f' ((R : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: rwa [← hasDerivAt_iff_hasFDerivAt, hR, RingHomInvPair.comp_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Basic (goal)
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 : 𝕜))
⊢ HasFDerivAt (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') ((R : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
have convert_3₁ : HasDerivAt f f' ((σ' : (a : 𝕜) → 𝕜) ((σ : (a : 𝕜) → 𝕜) x : 𝕜))
Tactic: rwa [← hasDerivAt_iff_hasFDerivAt, hR, RingHomInvPair.comp_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x
have hg₁ : HasDerivWithinAt g₁ g₁' s' (h x)
Tactic: rw [hy] at hg
Cleared hypotheses: hg, hh, hs, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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₁ ∘ h) (h' • g₁') s x
have hg₁ : HasDerivWithinAt g₁ g₁' t' (h x)
Tactic: rw [hy] at hg
Cleared hypotheses: hg, hh, hst, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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₁ ∘ h) (h' • g₁') x
have hg₁ : HasDerivAt g₁ g₁' (h x)
Tactic: rw [hy] at hg
Cleared hypotheses: hg, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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₁ ∘ h) (h' • g₁') x
have hg₁ : HasStrictDerivAt g₁ g₁' (h x)
Tactic: rw [hy] at hg
Cleared hypotheses: hg, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
have hg₁ : HasDerivAt g₁ g₁' (h x)
Tactic: rw [hy] at hg
Cleared hypotheses: hg, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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'
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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)
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
have hg₁ : DifferentiableWithinAt 𝕜' g₁ t' (h x)
Tactic: rw [hy] at hg
Cleared hypotheses: hg, hh, hs, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)
have hg₁ : DifferentiableAt 𝕜' g₁ (h x)
Tactic: rw [hy] at hg
Cleared hypotheses: hg, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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) (h₂' • f') L''
have 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₂')))
Tactic: convert! (hh₂.restrictScalars 𝕜).comp hf hL
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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 𝕜 𝕜')
⊢ Eq (α := (E →L[𝕜] 𝕜') → E →L[𝕜] 𝕜') (HSMul.hSMul h₂')
    (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.toSpanSingleton 𝕜' h₂')))
have 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 : 𝕜')
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
have hh₁ : HasStrictDerivAt h₂ h₂' (f x)
Tactic: rw [hy] at hh
Cleared hypotheses: hh, hf, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x
have hh₁ : HasDerivAt h₂ h₂' (f x)
Tactic: rw [hy] at hh
Cleared hypotheses: hh, hf, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
have hh₁ : HasDerivAt h₂ h₂' (f x)
Tactic: rw [hy] at hh
Cleared hypotheses: hh, hf, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
have hh₁ : HasDerivWithinAt h₂ h₂' t (f x)
Tactic: rw [hy] at hh
Cleared hypotheses: hh, hf, hst, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x
have hh₁ : HasDerivWithinAt h₂ h₂' t (f x)
Tactic: subst y
Cleared hypotheses: y, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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
have rw : HasDerivAtFilter (h₂ ∘ h) (h' * h₂') L
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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
have rw : HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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) (h₂' * h') s x
have hh₃ : HasDerivWithinAt h₂ h₂' s' (h x)
Tactic: rw [hy] at hh₂
Cleared hypotheses: hh₂, hh, hst, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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₂' * h') x
have hh₃ : HasDerivAt h₂ h₂' (h x)
Tactic: rw [hy] at hh₂
Cleared hypotheses: hh₂, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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
have rw : HasStrictDerivAt (h₂ ∘ h) (h' * h₂') x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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₂' * h') x
have hh₃ : HasStrictDerivAt h₂ h₂' (h x)
Tactic: rw [hy] at hh₂
Cleared hypotheses: hh₂, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
have hh₃ : HasDerivAt h₂ h₂' (h x)
Tactic: rw [hy] at hh₂
Cleared hypotheses: hh₂, hh, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x
have hh₃ : HasDerivWithinAt h₂ h₂' t (h x)
Tactic: subst y
Cleared hypotheses: y, hh₂, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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'
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
have hh₃ : DifferentiableWithinAt 𝕜' h₂ s' (h x)
Tactic: subst hy
Cleared hypotheses: y, hh₂, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
have hh₃ : DifferentiableAt 𝕜' h₂ (h x)
Tactic: subst hy
Cleared hypotheses: y, hh₂, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
⊢ HasDerivAtFilter f^[n] (f' ^ n) L
have this : HasFDerivAtFilter f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) L
Tactic: have := hf.hasFDerivAtFilter.iterate hL n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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
⊢ HasDerivAtFilter f^[n] (f' ^ n) L
have rwa : ∀ (this : HasFDerivAtFilter (𝕜 := 𝕜) f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 (f' ^ n)) L),
  HasDerivAtFilter f^[n] (f' ^ n) L
Tactic: rwa [ContinuousLinearMap.toSpanSingleton_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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 : ℕ
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x
have this : HasFDerivWithinAt f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) s x
Tactic: have := HasFDerivWithinAt.iterate hf hx hs n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x
have rwa : ∀ (this : HasFDerivWithinAt (𝕜 := 𝕜) f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 (f' ^ n)) s x),
  HasDerivWithinAt f^[n] (f' ^ n) s x
Tactic: rwa [ContinuousLinearMap.toSpanSingleton_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasStrictDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasStrictDerivAt f^[n] (f' ^ n) x
have this : HasStrictFDerivAt f^[n] (HPow.hPow (α := 𝕜 →L[𝕜] 𝕜) (ContinuousLinearMap.toSpanSingleton 𝕜 f') n) x
Tactic: have := hf.hasStrictFDerivAt.iterate hx n
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
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
⊢ HasStrictDerivAt f^[n] (f' ^ n) x
have rwa : ∀ (this : HasStrictFDerivAt (𝕜 := 𝕜) f^[n] (ContinuousLinearMap.toSpanSingleton 𝕜 (f' ^ n)) x),
  HasStrictDerivAt f^[n] (f' ^ n) x
Tactic: rwa [ContinuousLinearMap.toSpanSingleton_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x
have hl₁ : HasFDerivWithinAt l l' t (f x)
Tactic: rw [hy] at hl
Cleared hypotheses: hl, hf, hst, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x
have hl₁ : HasFDerivWithinAt l l' t (f x)
Tactic: subst y
Cleared hypotheses: y, hl, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivWithinAt (l ∘ f) ((l' : (a : F) → E) f') s x
have hl₁ : HasFDerivAt l l' (f x)
Tactic: rw [hy] at hl
Cleared hypotheses: hl, hf, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasDerivAt (l ∘ f) ((l' : (a : F) → E) f') x
have hl₁ : HasFDerivAt l l' (f x)
Tactic: rw [hy] at hl
Cleared hypotheses: hl, hf, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
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
⊢ HasStrictDerivAt (l ∘ f) ((l' : (a : F) → E) f') x
have hl₁ : HasStrictFDerivAt l l' (f x)
Tactic: rw [hy] at hl
Cleared hypotheses: hl, hf, hy