awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
this : ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn 0 f p u
rcases :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (H : HasFTaylorSeriesUpToOn 0 f p u),
    ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x

Tactic:
rcases this with ⟨u, hu, p, H⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
rw :
  ∀ (hu : x ∈ u ∧ u ∈ 𝓝[s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (H : HasFTaylorSeriesUpToOn 0 f p u),
    ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x

Tactic:
rw [mem_nhdsWithin_insert] at hu

Premises used: mem_nhdsWithin_insert
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : x ∈ u ∧ u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x

Tactic:
(H.continuousOn.continuousWithinAt hu.1).mono_of_mem_nhdsWithin hu.2

Premises used: HasFTaylorSeriesUpToOn.continuousOn, ContinuousWithinAt.mono_of_mem_nhdsWithin, And.right, And.left, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : x ∈ u ∧ u ∈ 𝓝[s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x

Tactic:
exact (H.continuousOn.continuousWithinAt hu.1).mono_of_mem_nhdsWithin hu.2

Premises used: HasFTaylorSeriesUpToOn.continuousOn, ContinuousWithinAt.mono_of_mem_nhdsWithin, And.right, And.left, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : ContDiffWithinAt 𝕜 ω f s x
obtain :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (H : HasFTaylorSeriesUpToOn ω f p u)
    (H' :
      ∀ (i : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u),
    ContDiffWithinAt 𝕜 ω f₁ s x
⊢ ContDiffWithinAt 𝕜 ω f₁ s x

Tactic:
obtain ⟨u, hu, p, H, H'⟩ := h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn ω f p u
H' :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt 𝕜 ω f₁ s x

Tactic:
⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right,
      fun i ↦ (H' i).mono (sep_subset _ _)⟩

Premises used: Iff.mpr, Filter.inter_mem, setOf, Membership.mem, HasFTaylorSeriesUpToOn.mono, HasFTaylorSeriesUpToOn.congr, And, mem_nhdsWithin_insert, And.right, And.intro, Exists.intro, ContDiffWithinAt, Set.sep_subset, Eq, AnalyticOn.mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn ω f p u
H' :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt 𝕜 ω f₁ s x

Tactic:
exact ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right,
      fun i ↦ (H' i).mono (sep_subset _ _)⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n_1 : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
let :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
    (H : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
    ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f₁ p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f₁ p u

Tactic:
let ⟨u, hu, p, H⟩ := h m hm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n_1 : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f₁ p u

Tactic:
⟨{ x ∈ u | f₁ x = f x }, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩

Premises used: Iff.mpr, Filter.inter_mem, setOf, Membership.mem, HasFTaylorSeriesUpToOn.mono, HasFTaylorSeriesUpToOn.congr, And, mem_nhdsWithin_insert, And.right, And.intro, Exists.intro, Set.sep_subset, Eq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n_1 : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f₁ p u

Tactic:
exact ⟨{ x ∈ u | f₁ x = f x }, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right,
      fun i ↦ (H' i).mono (sep_subset _ _)⟩
  | (n : ℕ∞) =>
    intro m hm
    let ⟨u, hu, p, H⟩ := h m hm
    exact ⟨{ x ∈ u | f₁ x = f x }, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
⟨fun H ↦ H.congr_of_eventuallyEq h₁.symm hx.symm, fun H ↦ H.congr_of_eventuallyEq h₁ hx⟩

Premises used: Iff.intro, ContDiffWithinAt.congr_of_eventuallyEq, Eq.symm, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
h.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) h₁)
    (mem_of_mem_nhdsWithin (mem_insert x s) h₁ :)

Premises used: mem_of_mem_nhdsWithin, ContDiffWithinAt.congr_of_eventuallyEq, Set.mem_insert, Set.subset_insert, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[insert x s] x] f
⊢ ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
⟨fun H ↦ H.congr_of_eventuallyEq_insert h₁.symm, fun H ↦ H.congr_of_eventuallyEq_insert h₁⟩

Premises used: ContDiffWithinAt.congr_of_eventuallyEq_insert, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
h.congr_of_eventuallyEq h₁ <| h₁.self_of_nhdsWithin hx

Premises used: Filter.Eventually.self_of_nhdsWithin, ContDiffWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
⟨fun H ↦ H.congr_of_eventuallyEq_of_mem h₁.symm hx, fun H ↦ H.congr_of_eventuallyEq_of_mem h₁ hx⟩

Premises used: ContDiffWithinAt.congr_of_eventuallyEq_of_mem, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : ∀ y ∈ s, f₁ y = f y
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
h.congr_of_eventuallyEq (Filter.eventuallyEq_of_mem self_mem_nhdsWithin h₁) hx

Premises used: Filter.eventuallyEq_of_mem, self_mem_nhdsWithin, ContDiffWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : ∀ y ∈ s, f₁ y = f y
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
⟨fun h' ↦ h'.congr (fun x hx ↦ (h₁ x hx).symm) hx.symm, fun h' ↦  h'.congr h₁ hx⟩

Premises used: ContDiffWithinAt.congr, Iff.intro, Eq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : ∀ y ∈ s, f₁ y = f y
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
h.congr h₁ (h₁ _ hx)

Premises used: ContDiffWithinAt.congr
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : ∀ y ∈ s, f₁ y = f y
hx : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
contDiffWithinAt_congr h₁ (h₁ x hx)

Premises used: contDiffWithinAt_congr
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : ∀ y ∈ insert x s, f₁ y = f y
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
h.congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

Premises used: Set.mem_insert_of_mem, ContDiffWithinAt.congr, Set.mem_insert
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h₁ : ∀ y ∈ insert x s, f₁ y = f y
⊢ ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
contDiffWithinAt_congr (fun y hy ↦ h₁ y (mem_insert_of_mem _ hy)) (h₁ x (mem_insert _ _))

Premises used: Set.mem_insert_of_mem, Set.mem_insert, contDiffWithinAt_congr
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
t : Set E
hst : s ∈ 𝓝[t] x
h : ContDiffWithinAt 𝕜 ω f s x
obtain :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F) (H : HasFTaylorSeriesUpToOn ω f p u)
    (H' :
      ∀ (i : ℕ),
        AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u),
    ContDiffWithinAt 𝕜 ω f t x
⊢ ContDiffWithinAt 𝕜 ω f t x

Tactic:
obtain ⟨u, hu, p, H, H'⟩ := h
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
t : Set E
hst : s ∈ 𝓝[t] x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn ω f p u
H' :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt 𝕜 ω f t x

Tactic:
⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩

Premises used: insert_mem_nhdsWithin_insert, nhdsWithin_le_of_mem, And.intro, Exists.intro, ContDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
t : Set E
hst : s ∈ 𝓝[t] x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn ω f p u
H' :
  ∀ (i : ℕ),
    AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) u
⊢ ContDiffWithinAt 𝕜 ω f t x

Tactic:
exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n_1 : ℕ∞ω
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
rcases :
  ∀ (u : Set E) (hu : u ∈ 𝓝[insert x s] x) (p : E → FormalMultilinearSeries 𝕜 E F)
    (H : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u),
    ∃ u ∈ 𝓝[insert x t] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x t] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

Tactic:
rcases h m hm with ⟨u, hu, p, H⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n_1 : ℕ∞ω
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x t] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

Tactic:
⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H⟩

Premises used: insert_mem_nhdsWithin_insert, nhdsWithin_le_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n_1 : ℕ∞ω
t : Set E
hst : s ∈ 𝓝[t] x
n : ℕ∞
h : ContDiffWithinAt 𝕜 (↑n : ℕ∞ω) f s x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u
⊢ ∃ u ∈ 𝓝[insert x t] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

Tactic:
exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : s ∈ 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H, H'⟩
  | (n : ℕ∞) =>
    intro m hm
    rcases h m hm with ⟨u, hu, p, H⟩
    exact ⟨u, nhdsWithin_le_of_mem (insert_mem_nhdsWithin_insert hst) hu, p, H⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : t ⊆ s
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
h.mono_of_mem_nhdsWithin <| Filter.mem_of_superset self_mem_nhdsWithin hst

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin, self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s s₁ : Set E
f f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h' : EqOn f₁ f s₁
h₁ : s₁ ⊆ s
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s₁ x

Tactic:
(h.mono h₁).congr h' hx

Premises used: ContDiffWithinAt.congr, ContDiffWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : s =ᶠ[𝓝 x] t
⊢ 𝓝[s] x = 𝓝[t] x

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq] at hst

Premises used: nhdsWithin_eq_iff_eventuallyEq
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
t : Set E
hst : 𝓝[s] x = 𝓝[t] x
⊢ ContDiffWithinAt 𝕜 n f t x

Tactic:
apply h.mono_of_mem_nhdsWithin <| hst ▸ self_mem_nhdsWithin

Premises used: ContDiffWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
t : Set E
hst : s =ᶠ[𝓝 x] t
⊢ ContDiffWithinAt 𝕜 n f s x ↔ ContDiffWithinAt 𝕜 n f t x

Tactic:
⟨fun h => h.congr_set hst, fun h => h.congr_set hst.symm⟩

Premises used: ContDiffWithinAt.congr_set, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
n : ℕ∞ω
h : t ∈ 𝓝[s] x
⊢ ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
contDiffWithinAt_congr_set (mem_nhdsWithin_iff_eventuallyEq.1 h).symm

Premises used: contDiffWithinAt_congr_set, mem_nhdsWithin_iff_eventuallyEq, Iff.mp, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
n : ℕ∞ω
h : t ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
contDiffWithinAt_inter' (mem_nhdsWithin_of_mem_nhds h)

Premises used: contDiffWithinAt_inter', mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 ω f (insert x s) x ↔ ContDiffWithinAt 𝕜 ω f s x

Tactic:
simp [ContDiffWithinAt]

Premises used: ContDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
⊢ ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
match n with
  | ω => simp [ContDiffWithinAt]
  | (n : ℕ∞) => simp_rw [ContDiffWithinAt, insert_idem]
-- Module: Mathlib.Analysis.Calculus.ContDiff.Defs
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
y : E
inl : ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x
inr : ∀ (hx : x ≠ y), ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
rcases eq_or_ne x y with (rfl | hx)

Premises used: eq_or_ne, rfl