awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Polynomial (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
add :
  ∀ (p q : 𝕜[X]) (hp : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x)
    (hq : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x q) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) q)) x),
    HasStrictDerivAt (fun (x : 𝕜) ↦ eval x (p + q)) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) (p + q))) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x
have monomial : ∀ (n : ℕ) (a : 𝕜),
  HasStrictDerivAt (fun (x : 𝕜) ↦ eval x ((monomial n : (a : 𝕜) → 𝕜[X]) a))
    (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) ((monomial n : (a : 𝕜) → 𝕜[X]) a))) x
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simpa using hp.add hq
  | monomial n a => simpa [mul_assoc, derivative_monomial]
                      using (hasStrictDerivAt_pow n x).const_mul a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Polynomial (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ eval x p) s x = eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)
have rw : deriv (fun (x : 𝕜) ↦ eval x p) x = eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)
Tactic: rw [DifferentiableAt.derivWithin p.differentiableAt hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
⊢ Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
      (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)
⊢ Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
⊢ derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x
⊢ derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pow (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
h : UniqueDiffWithinAt 𝕜 s x
n : ℕ
⊢ derivWithin (fun (x : 𝕜) ↦ x ^ n) s x = (↑n : 𝕜) * x ^ (n - 1)
have rw : (↑n : 𝕜) * x ^ (n - 1) * derivWithin (fun (x : 𝕜) ↦ x) s x = (↑n : 𝕜) * x ^ (n - 1)
Tactic: rw [derivWithin_fun_pow (differentiableWithinAt_fun_id) n, derivWithin_id' _ _ h, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pow (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
h : UniqueDiffWithinAt 𝕜 s x
n : ℕ
rw : (↑n : 𝕜) * x ^ (n - 1) * derivWithin (fun (x : 𝕜) ↦ x) s x = (↑n : 𝕜) * x ^ (n - 1)
⊢ derivWithin (fun (x : 𝕜) ↦ x ^ n) s x = (↑n : 𝕜) * x ^ (n - 1)
have rw₁ : (↑n : 𝕜) * x ^ (n - 1) * 1 = (↑n : 𝕜) * x ^ (n - 1)
Tactic: rw [derivWithin_fun_pow (differentiableWithinAt_fun_id) n, derivWithin_id' _ _ h, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Pow (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
h : UniqueDiffWithinAt 𝕜 s x
n : ℕ
rw : (↑n : 𝕜) * x ^ (n - 1) * derivWithin (fun (x : 𝕜) ↦ x) s x = (↑n : 𝕜) * x ^ (n - 1)
rw₁ : (↑n : 𝕜) * x ^ (n - 1) * 1 = (↑n : 𝕜) * x ^ (n - 1)
⊢ derivWithin (fun (x : 𝕜) ↦ x ^ n) s x = (↑n : 𝕜) * x ^ (n - 1)
have rw₂ : (↑n : 𝕜) * x ^ (n - 1) = (↑n : 𝕜) * x ^ (n - 1)
Tactic: rw [derivWithin_fun_pow (differentiableWithinAt_fun_id) n, derivWithin_id' _ _ h, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Prod (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
⊢ derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Prod (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
⊢ derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Prod (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
have pos : Eq (α := (i : ι) → E' i)
  (((ContinuousLinearMap.pi (φ := E') fun (i : ι) ↦ fderivWithin 𝕜 (fun (x : 𝕜) ↦ φ x i) s x : 𝕜 →L[𝕜] (i : ι) → E' i) :
        (a : 𝕜) → (i : ι) → E' i)
      1 :
    (i : ι) → E' i)
  fun (i : ι) ↦ (derivWithin (fun (x : 𝕜) ↦ φ x i) s x : E' i)
Tactic: rw [derivWithin, fderivWithin_pi h hsx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Prod (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin φ s x = fun (i : ι) ↦ derivWithin (fun (x : 𝕜) ↦ φ x i) s x
have hsx₁ : ¬AccPt x (𝓟 s)
Tactic: rw [uniqueDiffWithinAt_iff_accPt] at hsx
Cleared hypotheses: hsx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Prod (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_1
E' : ι → Type u_2
inst_1 : (i : ι) → NormedAddCommGroup (E' i)
inst_2 : (i : ι) → NormedSpace.{u, u_2} 𝕜 (E' i)
φ : 𝕜 → (i : ι) → E' i
h : ∀ (i : ι), DifferentiableAt.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) x
⊢ deriv φ x = fun (i : ι) ↦ deriv (fun (x : 𝕜) ↦ φ x i) x
have simp : Eq (α := (i : ι) → E' i)
  (((ContinuousLinearMap.pi (φ := E') fun (i : ι) ↦ fderiv 𝕜 (fun (x : 𝕜) ↦ φ x i) x : 𝕜 →L[𝕜] (i : ι) → E' i) :
        (a : 𝕜) → (i : ι) → E' i)
      1 :
    (i : ι) → E' i)
  fun (i : ι) ↦
  (((fderiv.{u, u, u_2} 𝕜 (F := E' i) (fun (x : 𝕜) ↦ φ x i) x :
          ContinuousLinearMap.{u, u, u, u_2} (RingHom.id 𝕜) 𝕜 (E' i)) :
        (a : 𝕜) → E' i)
      1 :
    E' i)
Tactic: simp only [deriv, fderiv_pi h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Shift (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (a - x)) s x = -derivWithin f (a +ᵥ -s) (a - x)
have simp : derivWithin (fun (x : 𝕜) ↦ f (a + -x)) s x = -derivWithin f (a +ᵥ -s) (a + -x)
Tactic: simp only [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Shift (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (a + -x)) s x = -derivWithin f (a +ᵥ -s) (a + -x)
have rw : -derivWithin (fun (x : 𝕜) ↦ f (a + x)) (-s) (-x) = -derivWithin f (a +ᵥ -s) (a + -x)
Tactic: rw [derivWithin_comp_neg (f <| a + ·), derivWithin_comp_const_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Shift (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
rw : -derivWithin (fun (x : 𝕜) ↦ f (a + x)) (-s) (-x) = -derivWithin f (a +ᵥ -s) (a + -x)
⊢ derivWithin (fun (x : 𝕜) ↦ f (a + -x)) s x = -derivWithin f (a +ᵥ -s) (a + -x)
have rw₁ : -derivWithin f (a +ᵥ -s) (a + -x) = -derivWithin f (a +ᵥ -s) (a + -x)
Tactic: rw [derivWithin_comp_neg (f <| a + ·), derivWithin_comp_const_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Shift (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ f (a - x)) x = -deriv f (a - x)
have simp_rw : deriv (fun (x : 𝕜) ↦ f (a + -x)) x = -deriv f (a + -x)
Tactic: simp_rw [sub_eq_add_neg, deriv_comp_neg (f <| a + ·), deriv_comp_const_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Shift (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
simp_rw : deriv (fun (x : 𝕜) ↦ f (a + -x)) x = -deriv f (a + -x)
⊢ deriv (fun (x : 𝕜) ↦ f (a - x)) x = -deriv f (a - x)
have simp_rw₁ : -deriv (fun (x : 𝕜) ↦ f (a + x)) (-x) = -deriv f (a + -x)
Tactic: simp_rw [sub_eq_add_neg, deriv_comp_neg (f <| a + ·), deriv_comp_const_add]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Shift (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (x - a)) s x = derivWithin f (-a +ᵥ s) (x - a)
have simp_rw : derivWithin (fun (x : 𝕜) ↦ f (x + -a)) s x = derivWithin f (-a +ᵥ s) (x + -a)
Tactic: simp_rw [sub_eq_add_neg, derivWithin_comp_add_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Shift (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ f (x - a)) x = deriv f (x - a)
have simp_rw : deriv (fun (x : 𝕜) ↦ f (x + -a)) x = deriv f (x + -a)
Tactic: simp_rw [sub_eq_add_neg, deriv_comp_add_const]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ EventuallyEq.{u, v} (β := F) (L ⊓ 𝓟 {x}ᶜ) (fun (y : 𝕜) ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') fun (y : 𝕜) ↦
    slope f x y - f'
have refine : ∀ (y : 𝕜) (hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y), slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'
Tactic: refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'
have rw : slope f x y - f' = slope f x y - f'
Tactic: rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto.{u, v} (β := F) (fun (y : 𝕜) ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f')
have rw : Tendsto.{u, v} (β := F) (fun (y : 𝕜) ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔
  Tendsto (β := F) ((fun (x : F) ↦ x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)
Tactic: rw [← nhds_translation_sub f', tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')
have simp : HasDerivAtFilter f f' (SProd.sprod (β := Filter 𝕜) (𝓝 x ⊓ 𝓟 s) (pure x)) ↔
  Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')
Tactic: simp only [HasDerivWithinAt, nhdsWithin, diff_eq, ← inf_assoc, inf_principal.symm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
hs : x ∉ s
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
have rw : Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f') ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
Tactic: rw [hasDerivWithinAt_iff_tendsto_slope, diff_singleton_eq_self hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
hs : x ∉ s
rw : Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f') ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
have rw₁ : Tendsto (slope f x) (𝓝[s] x) (𝓝 f') ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
Tactic: rw [hasDerivWithinAt_iff_tendsto_slope, diff_singleton_eq_self hs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ HasDerivAt f f' x ↔ Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')
have this : 𝓝[≠] x = map (fun (t : 𝕜) ↦ x + t) (𝓝[≠] 0)
Tactic: have : 𝓝[≠] x = Filter.map (fun t ↦ x + t) (𝓝[≠] 0) := by simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have pos : ∀ (H : UniqueDiffWithinAt 𝕜 s x),
  derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
Tactic: by_cases H : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
pos :
  ∀ (H : UniqueDiffWithinAt 𝕜 s x),
    derivWithin f s x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have neg : ∀ (H : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
Tactic: by_cases H : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have pos : ∀ (H' : DifferentiableWithinAt 𝕜 f s x),
  derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
Tactic: by_cases H' : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (H' : DifferentiableWithinAt 𝕜 f s x),
    derivWithin f s x ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have neg : ∀ (H' : ¬DifferentiableWithinAt 𝕜 f s x),
  derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
Tactic: by_cases H' : DifferentiableWithinAt 𝕜 f s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have neg : 0 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
Tactic: rw [derivWithin_zero_of_not_differentiableWithinAt H']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
⊢ (𝓝[(s ∩ t) \ {x}] x).NeBot
have rw : UniqueDiffWithinAt 𝕜 (s ∩ t) x
Tactic: rw [← accPt_principal_iff_nhdsWithin, ← uniqueDiffWithinAt_iff_accPt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have I : (𝓝[(s ∩ t) \ {x}] x).NeBot
Tactic: have I : (𝓝[(s ∩ t) \ {x}] x).NeBot := by
    rw [← accPt_principal_iff_nhdsWithin, ← uniqueDiffWithinAt_iff_accPt]
    exact H.mono_closure h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
have apply : 𝓝[(s ∩ t) \ {x}] x ≤ 𝓝[s \ {x}] x
Tactic: apply Tendsto.mono_left (hasDerivWithinAt_iff_tendsto_slope.1 H'.hasDerivWithinAt)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ 𝓝[(s ∩ t) \ {x}] x ≤ 𝓝[s \ {x}] x
have rw : 𝓝[t ∩ (s \ {x})] x ≤ 𝓝[s \ {x}] x
Tactic: rw [inter_comm, inter_diff_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
Tactic: have : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x)) := by
    apply Tendsto.mono_left (hasDerivWithinAt_iff_tendsto_slope.1 H'.hasDerivWithinAt)
    rw [inter_comm, inter_diff_assoc]
    exact nhdsWithin_mono _ inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span 𝕜 (f '' t)) : Set F)
have pos : derivWithin f s x ∈
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
Tactic: rw [← closure_closure, ← Submodule.topologicalClosure_coe]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Slope (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
have pos : ∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x,
  slope f x x_1 ∈ (↑(Submodule.topologicalClosure (Submodule.span 𝕜 (f '' t))) : Set F)
Tactic: apply mem_closure_of_tendsto this