awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
inr₁ : ContinuousOn.{0, u_3} (Y := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]
inr₂ :
  ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) (deriv (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x_1)
      x_1
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
have inr₃ : ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
  HasDerivAt.{0, u_3} (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t)
    (deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1) x_1
Tactic: apply intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (u := fun t ↦ (x - t) ^ k / k !) (v := fun t ↦ iteratedDerivWithin k f (uIcc x₀ x) t)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
inr₁ : ContinuousOn.{0, u_3} (Y := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]
inr₂ :
  ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) (deriv (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x_1)
      x_1
inr₃ :
  ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt.{0, u_3} (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t)
      (deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1) x_1
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
have inr₄ : IntervalIntegrable (ε := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) MeasureTheory.volume x₀ x
Tactic: apply intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (u := fun t ↦ (x - t) ^ k / k !) (v := fun t ↦ iteratedDerivWithin k f (uIcc x₀ x) t)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
inr₁ : ContinuousOn.{0, u_3} (Y := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]
inr₂ :
  ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) (deriv (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x_1)
      x_1
inr₃ :
  ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt.{0, u_3} (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t)
      (deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1) x_1
inr₄ : IntervalIntegrable (ε := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) MeasureTheory.volume x₀ x
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have v : (t : ℝ) → F := fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
have inr₅ : IntervalIntegrable.{u_3} (ε := F) (deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) MeasureTheory.volume x₀ x
Tactic: apply intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (u := fun t ↦ (x - t) ^ k / k !) (v := fun t ↦ iteratedDerivWithin k f (uIcc x₀ x) t)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
have funProp : ∀ x_1 ∈ [[x₀, x]], Ne (α := ℝ) (↑k ! : ℝ) 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ LE.le (α := WithTop ℕ∞) (↑k : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
have norm_cast : k ≤ n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) (deriv (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) t) t
have inr : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) t
Tactic: apply DifferentiableAt.hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ HasDerivAt.{0, u_3} (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t)
    (deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) t) t
have inr : DifferentiableOn.{0, 0, u_3} ℝ (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) (uIoo x₀ x)
Tactic: refine DifferentiableOn.hasDerivAt (s := uIoo x₀ x) ?_ (by grind [Ioo_mem_nhds, uIoo])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ LT.lt (α := WithTop ℕ∞) (↑k : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
have norm_cast : k < n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable (ε := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) MeasureTheory.volume x₀ x
have inr : ContinuousOn (Y := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
Tactic: apply ContinuousOn.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable.{u_3} (ε := F) (deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) MeasureTheory.volume x₀ x
have inr : IntervalIntegrable (iteratedDerivWithin (k + 1) f [[x₀, x]]) MeasureTheory.volume x₀ x
Tactic: apply IntervalIntegrable.congr_ae (f := iteratedDerivWithin (k + 1) f [[x₀, x]])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : IntervalIntegrable (iteratedDerivWithin (k + 1) f [[x₀, x]]) MeasureTheory.volume x₀ x
⊢ IntervalIntegrable.{u_3} (ε := F) (deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) MeasureTheory.volume x₀ x
have inr₁ : iteratedDerivWithin (k + 1) f
    [[x₀,
      x]] =ᶠ[MeasureTheory.ae (F := MeasureTheory.Measure ℝ)
    (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι x₀ x))]
  deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t
Tactic: apply IntervalIntegrable.congr_ae (f := iteratedDerivWithin (k + 1) f [[x₀, x]])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ LE.le (α := WithTop ℕ∞) (↑(k + 1) : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)
have norm_cast : k + 1 ≤ n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ iteratedDerivWithin (k + 1) f
      [[x₀,
        x]] =ᶠ[MeasureTheory.ae (F := MeasureTheory.Measure ℝ)
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι x₀ x))]
    deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t
have inr : ∀ᵐ (x_1 : ℝ),
  x_1 ∈ Ι x₀ x →
    iteratedDerivWithin (k + 1) f [[x₀, x]] x_1 = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1
Tactic: rw [Filter.EventuallyEq, MeasureTheory.ae_restrict_iff' (by measurability)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ι x₀ x →
      iteratedDerivWithin (k + 1) f [[x₀, x]] x_1 = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1
have h : ∀ (a : ℝ),
  a ≠ x₀ →
    a ≠ x →
      a ∈ Ι x₀ x →
        iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
Tactic: filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
a : ℝ
h : a ≠ x₀
h_1 : a ≠ x
h_2 : a ∈ Ι x₀ x
⊢ iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
have h : derivWithin (iteratedDerivWithin k f [[x₀, x]]) [[x₀, x]] a =
  deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
Tactic: rw [iteratedDerivWithin_succ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
have rw : ∀ (hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)),
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)
Tactic: rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hf' ⊢
Cleared hypotheses: hf', this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)
have this₁ : TendstoUniformlyOnFilter
  (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
    (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
  (HAdd.hAdd (α := E → G) (-0) (-0)) (l ×ˢ l) (𝓝 x)
Tactic: have := this.1.neg.add this.2.neg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
this :
  TendstoUniformlyOnFilter
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    (HAdd.hAdd (α := E → G) (-0) (-0)) (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)
have this₁ : TendstoUniformlyOnFilter
  (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
    (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
  0 (l ×ˢ l) (𝓝 x)
Tactic: rw [neg_zero, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x_1 : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x_1, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x_1) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x_1)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G)
      (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x_1 - f n.2 x_1)) 0 (l ×ˢ l) (𝓝 x_1) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x : E) ↦ f n.1 x_1 - f n.2 x_1) 0 (l ×ˢ l)
      (𝓝 x_1)
this :
  TendstoUniformlyOnFilter
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x_1 - f n.2 x_1))
      (-fun (n : ι × ι) (x : E) ↦ f n.1 x_1 - f n.2 x_1))
    0 (l ×ˢ l) (𝓝 x_1)
x : Prod.{u_1, u_2} (ι × ι) E
⊢ HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
      (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x_1 - f n.2 x_1))
      (-fun (n : ι × ι) (x : E) ↦ f n.1 x_1 - f n.2 x_1) x.1 x.2 =
    -f x.1.1 x.2 + f x.1.2 x.2
have simp : f x.1.1 x_1 - f x.1.2 x_1 - (f x.1.1 x.2 - f x.1.2 x.2) + (f x.1.2 x_1 - f x.1.1 x_1) = -f x.1.1 x.2 + f x.1.2 x.2
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)
have TendstoUniformlyOnFilter : TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
    (l ×ˢ l) (𝓝 x) ∧
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
Tactic: suffices
    TendstoUniformlyOnFilter (fun (n : ι × ι) (z : E) => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
        (l ×ˢ l) (𝓝 x) ∧
      TendstoUniformlyOnFilter (fun (n : ι × ι) (_ : E) => f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x) by
    have := this.1.neg.add this.2.neg
    rw [neg_zero, add_zero] at this
    apply this.congr (.of_forall (fun x ↦ by simp; abel))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
have left : TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
  (l ×ˢ l) (𝓝 x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
left :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
    0 (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
have right : TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
    0 (l ×ˢ l) (𝓝 x)
have left : ∀
  (hf' :
    ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε),
  ∀ ε > 0,
    ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (f n.1.1 n.2 - f n.1.2 n.2 - (f n.1.1 x - f n.1.2 x)) < ε
Tactic: rw [Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢
Cleared hypotheses: hf', this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2) (f n.1.1 n.2 - f n.1.2 n.2 - (f n.1.1 x - f n.1.2 x)) < ε
have this₁ : ∀ᶠ (x : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
  HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1)
      (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2)
      (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧
    HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1)
      (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2)
      (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2
Tactic: have := (tendsto_swap4_prod.eventually (hf.prod_mk hf)).diag_of_prod_right