awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f g : 𝕜 → F
x : 𝕜
hfg : f =ᶠ[𝓝 x] g
rw rw₁ :
  Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
⊢ Eq.{u_2 + 1} (α := F) ((iteratedFDerivWithin 𝕜 n f Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)
    ((iteratedFDerivWithin 𝕜 n g Set.univ x : (a : (i : Fin n) → 𝕜) → F) fun (x : Fin n) ↦ 1 : F)

Tactic:
rw [(hfg.filter_mono nhdsWithin_le_nhds).iteratedFDerivWithin_eq hfg.eq_of_nhds n]

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.eq_of_nhds, nhdsWithin_le_nhds, Filter.EventuallyEq.iteratedFDerivWithin_eq
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
⊢ EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Tactic:
fun x hx ↦ Filter.EventuallyEq.iteratedDeriv_eq n ?_

Premises used: Set.EqOn, Filter.EventuallyEq.iteratedDeriv_eq
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
refine : ∀ (x : 𝕜) (hx : x ∈ s), f =ᶠ[𝓝 x] g
⊢ EqOn (iteratedDeriv n f) (iteratedDeriv n g) s

Tactic:
refine fun x hx ↦ Filter.EventuallyEq.iteratedDeriv_eq n ?_

Premises used: Filter.EventuallyEq.iteratedDeriv_eq
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
x : 𝕜
hx : x ∈ s
h : ∀ (a : 𝕜) (ha : a ∈ s), f a = g a
⊢ f =ᶠ[𝓝 x] g

Tactic:
filter_upwards [IsOpen.mem_nhds hs hx] with a ha

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
x : 𝕜
hx : x ∈ s
a : 𝕜
ha : a ∈ s
⊢ f a = g a

Tactic:
hfg ha
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f g : 𝕜 → F
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
n : ℕ
x : 𝕜
hx : x ∈ s
a : 𝕜
ha : a ∈ s
⊢ f a = g a

Tactic:
exact hfg ha
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (s + t)

Tactic:
simp only [iteratedDeriv_zero]

Premises used: iteratedDeriv_zero
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_1 : ℕ
f : 𝕜 → F
s : 𝕜
n : ℕ
IH : Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv n f (s + t)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv (n + 1) fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv (n + 1) f (s + t)

Tactic:
simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_const_add _ s

Premises used: iteratedDeriv_succ, funext, deriv_comp_const_add
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
zero : Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (s + t)
succ :
  ∀ (n : ℕ)
    (IH : Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv n f (s + t)),
    Eq (α := (x : 𝕜) → F) (iteratedDeriv (n + 1) fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv (n + 1) f (s + t)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (s + z)) fun (t : 𝕜) ↦ iteratedDeriv n f (s + t)

Tactic:
induction n with
  | zero => simp only [iteratedDeriv_zero]
  | succ n IH =>
    simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_const_add _ s

Premises used: iteratedDeriv_zero, iteratedDeriv_succ, funext, deriv_comp_const_add
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (t + s)

Tactic:
simp only [iteratedDeriv_zero]

Premises used: iteratedDeriv_zero
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n_1 : ℕ
f : 𝕜 → F
s : 𝕜
n : ℕ
IH : Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv n f (t + s)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv (n + 1) fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv (n + 1) f (t + s)

Tactic:
simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s

Premises used: iteratedDeriv_succ, deriv_comp_add_const, funext
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
zero : Eq (α := (x : 𝕜) → F) (iteratedDeriv 0 fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv 0 f (t + s)
succ :
  ∀ (n : ℕ)
    (IH : Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv n f (t + s)),
    Eq (α := (x : 𝕜) → F) (iteratedDeriv (n + 1) fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv (n + 1) f (t + s)
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (z + s)) fun (t : 𝕜) ↦ iteratedDeriv n f (t + s)

Tactic:
induction n with
  | zero => simp only [iteratedDeriv_zero]
  | succ n IH =>
    simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s

Premises used: iteratedDeriv_zero, iteratedDeriv_succ, deriv_comp_add_const, funext
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (z - s)) fun (t : 𝕜) ↦ iteratedDeriv n f (t - s)

Tactic:
simp [sub_eq_add_neg, iteratedDeriv_comp_add_const]

Premises used: sub_eq_add_neg, iteratedDeriv_comp_add_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ Eq (α := (x : 𝕜) → F) (iteratedDeriv n fun (z : 𝕜) ↦ f (s - z)) fun (t : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) n • iteratedDeriv n f (s - t)

Tactic:
simpa [funext_iff, neg_add_eq_sub, iteratedDeriv_comp_add_const] using
    iteratedDeriv_comp_neg n (fun z => f (z + s))

Premises used: neg_add_eq_sub, funext_iff, iteratedDeriv_comp_neg, HAdd.hAdd, iteratedDeriv_comp_add_const
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ ∅, f i) s x) (∑ i ∈ ∅, iteratedDerivWithin n (f i) s x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x)
hf : ∀ i_1 ∈ insert i t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i_1) s x
⊢ ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f x_1) s x

Tactic:
rw [forall_mem_insert] at hf

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x)
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f x_1) s x
insert :
  ∀
    (IH :
      ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
        Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x)
          (∑ i ∈ t, iteratedDerivWithin n (f i) s x)),
    iteratedDerivWithin n (f i + fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x =
      iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ Insert.insert i t, f i) s x)
    (∑ i ∈ Insert.insert i t, iteratedDerivWithin n (f i) s x)

Tactic:
simp only [sum_insert hi, sum_fn] at IH ⊢

Premises used: Finset.sum_fn, Finset.sum_insert
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
i : ι
t : Finset ι
hi : i ∉ t
hf : ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x ∧ ∀ x_1 ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f x_1) s x
IH :
  ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x)
      (∑ i ∈ t, iteratedDerivWithin n (f i) s x)
insert :
  iteratedDerivWithin n (f i) s x + iteratedDerivWithin n (fun (x : 𝕜) ↦ ∑ i ∈ t, f i x) s x =
    iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
insert₁ insert₂ :
  iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x =
    iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x
⊢ iteratedDerivWithin n (f i + fun (a : 𝕜) ↦ ∑ c ∈ t, f c a) s x =
    iteratedDerivWithin n (f i) s x + ∑ i ∈ t, iteratedDerivWithin n (f i) s x

Tactic:
rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]

Premises used: ContDiffWithinAt.sum, And.right, And.left, iteratedDerivWithin_add
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ ∅, f i) s x) (∑ i ∈ ∅, iteratedDerivWithin n (f i) s x)
insert :
  ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
    (IH :
      ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
        Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x))
    (hf : ∀ i_1 ∈ Insert.insert i t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i_1) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ Insert.insert i t, f i) s x)
      (∑ i ∈ Insert.insert i t, iteratedDerivWithin n (f i) s x)
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ I, f i) s x) (∑ i ∈ I, iteratedDerivWithin n (f i) s x)

Tactic:
induction I using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    rw [forall_mem_insert] at hf
    simp only [sum_insert hi, sum_fn] at IH ⊢
    rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]

Premises used: Finset.forall_mem_insert, Insert.insert, Finset.sum_fn
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ ∅, f i) s x) (∑ i ∈ ∅, iteratedDerivWithin n (f i) s x)
insert :
  ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
    (IH :
      ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
        Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x))
    (hf : ∀ i_1 ∈ Insert.insert i t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i_1) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ Insert.insert i t, f i) s x)
      (∑ i ∈ Insert.insert i t, iteratedDerivWithin n (f i) s x)
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ I, f i) s x) (∑ i ∈ I, iteratedDerivWithin n (f i) s x)

Tactic:
classical
  induction I using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    rw [forall_mem_insert] at hf
    simp only [sum_insert hi, sum_fn] at IH ⊢
    rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]

Premises used: Finset.forall_mem_insert, Insert.insert, Finset.sum_fn
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (fun (x : 𝕜) ↦ ∑ i ∈ I, f i x) s x)
    (∑ i ∈ I, iteratedDerivWithin n (f i) s x)

Tactic:
simpa [sum_fn] using iteratedDerivWithin_sum hx hs hf

Premises used: iteratedDerivWithin_sum, Finset.sum_fn
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
hf : ∀ i ∈ I, ContDiffAt 𝕜 (↑n : WithTop ℕ∞) (f i) x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDeriv n (∑ i ∈ I, f i) x) (∑ i ∈ I, iteratedDeriv n (f i) x)

Tactic:
simpa using iteratedDerivWithin_sum (Set.mem_univ x) uniqueDiffOn_univ hf

Premises used: iteratedDerivWithin_sum, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
hf : ∀ i ∈ I, ContDiffAt 𝕜 (↑n : WithTop ℕ∞) (f i) x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDeriv n (fun (z : 𝕜) ↦ ∑ i ∈ I, f i z) x) (∑ i ∈ I, iteratedDeriv n (f i) x)

Tactic:
simpa [sum_fn] using iteratedDeriv_sum hf

Premises used: Finset.sum_fn, iteratedDeriv_sum
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
m : ℤ
k : ℕ
hs : IsOpen s
apply :
  Set.EqOn (β := 𝕜) (deriv^[k] fun (y : 𝕜) ↦ y ^ m)
    (fun (y : 𝕜) ↦ (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * y ^ (m - (↑k : ℤ))) s
⊢ Set.EqOn (β := 𝕜) (iteratedDerivWithin k (fun (y : 𝕜) ↦ y ^ m) s)
    (fun (y : 𝕜) ↦ (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * y ^ (m - (↑k : ℤ))) s

Tactic:
apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen_eq_iterate hs)

Premises used: Set.EqOn.trans, iteratedDerivWithin_of_isOpen_eq_iterate
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
m : ℤ
k : ℕ
hs : IsOpen s
t : 𝕜
ht : t ∈ s
⊢ Eq.{u_1 + 1} (α := 𝕜) (deriv^[k] (fun (y : 𝕜) ↦ y ^ m) t : 𝕜)
    ((fun (y : 𝕜) ↦ (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * y ^ (m - (↑k : ℤ))) t : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
k : ℕ
hs : IsOpen s
apply :
  Set.EqOn (β := 𝕜) (deriv^[k] fun (y : 𝕜) ↦ 1 / y)
    (fun (y : 𝕜) ↦ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * y ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) s
⊢ Set.EqOn (β := 𝕜) (iteratedDerivWithin k (fun (y : 𝕜) ↦ 1 / y) s)
    (fun (y : 𝕜) ↦ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * y ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) s

Tactic:
apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen_eq_iterate hs)

Premises used: Set.EqOn.trans, iteratedDerivWithin_of_isOpen_eq_iterate
-- Module: Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
k : ℕ
hs : IsOpen s
t : 𝕜
ht : t ∈ s
⊢ Eq.{u_1 + 1} (α := 𝕜) (deriv^[k] (fun (y : 𝕜) ↦ 1 / y) t : 𝕜)
    ((fun (y : 𝕜) ↦ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * y ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) t : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
⊢ ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b

Tactic:
have sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b := fun x hx =>
    Ioo_subset_Ioo (le_refl a) (le_of_lt hx.2)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
rw : Tendsto g (𝓝[Ioo a x] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[<] x) (𝓝 0)

Tactic:
rw [← h, ← nhdsWithin_Ioo_eq_nhdsLT hx.1]

Premises used: nhdsWithin_Ioo_eq_nhdsLT, And.left
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ Tendsto g (𝓝[Ioo a x] x) (𝓝 (g x))

Tactic:
((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, ContinuousWithinAt.mono, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ Tendsto g (𝓝[Ioo a x] x) (𝓝 (g x))

Tactic:
exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, ContinuousWithinAt.mono, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ Tendsto g (𝓝[<] x) (𝓝 0)

Tactic:
have : Tendsto g (𝓝[<] x) (𝓝 0) := by
      rw [← h, ← nhdsWithin_Ioo_eq_nhdsLT hx.1]
      exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[<] x) (𝓝 0)
⊢ ∃ c ∈ Ioo a x, g' c = 0

Tactic:
exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy

Premises used: exists_hasDerivAt_eq_zero', And.left
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[<] x) (𝓝 0)
obtain : ∀ (y : ℝ) (hyx : y ∈ Ioo a x) (hy : g' y = 0), False
⊢ False

Tactic:
obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0 :=
      exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy

Premises used: exists_hasDerivAt_eq_zero', And.left, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[<] x) (𝓝 0)
y : ℝ
hyx : y ∈ Ioo a x
hy : g' y = 0
⊢ False

Tactic:
hg' y (sub x hx hyx) hy
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[<] x) (𝓝 0)
y : ℝ
hyx : y ∈ Ioo a x
hy : g' y = 0
⊢ False

Tactic:
exact hg' y (sub x hx hyx) hy
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
⊢ ∀ x ∈ Ioo a b, g x ≠ 0

Tactic:
have hg : ∀ x ∈ Ioo a b, g x ≠ 0 := by
    intro x hx h
    have : Tendsto g (𝓝[<] x) (𝓝 0) := by
      rw [← h, ← nhdsWithin_Ioo_eq_nhdsLT hx.1]
      exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
    obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0 :=
      exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy
    exact hg' y (sub x hx hyx) hy