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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _

Premises used: AnalyticOn.iteratedFDerivWithin, ftaylorSeriesWithin, uniqueDiffOn_univ, ContDiffOn.analyticOn
-- 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
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOn 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (fun (x : E) ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
exact H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _

Premises used: AnalyticOn.iteratedFDerivWithin, uniqueDiffOn_univ, ContDiffOn.analyticOn
-- 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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo ω f p
h'p :
  ∀ (i : ℕ),
    AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) univ
x : E
h : Membership.mem (γ := Set E) univ x
⊢ ContDiffWithinAt 𝕜 ω f univ x

Tactic:
⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top,
        fun i ↦ (h'p i).analyticOn⟩

Premises used: Set.univ, HasFTaylorSeriesUpToOn.of_le, AnalyticOnNhd.analyticOn, HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn, le_top, And.intro, Exists.intro, ContDiffWithinAt, Filter.univ_sets
-- 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
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo ω f p
h'p :
  ∀ (i : ℕ),
    AnalyticOnNhd 𝕜 (F := ContinuousMultilinearMap.{u, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (fun (x : E) ↦ p x i) univ
x : E
h : Membership.mem (γ := Set E) univ x
⊢ ContDiffWithinAt 𝕜 ω f univ x

Tactic:
exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top,
        fun i ↦ (h'p i).analyticOn⟩
-- 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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
mp : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ → ContDiff 𝕜 (↑n : ℕ∞ω) f
mpr : ContDiff 𝕜 (↑n : ℕ∞ω) f → ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ ↔ ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
constructor
-- 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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
h : HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ)
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
use ftaylorSeriesWithin 𝕜 f univ

Premises used: Set.univ, ftaylorSeriesWithin
-- 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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
h : HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ
⊢ HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ)

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff]

Premises used: hasFTaylorSeriesUpToOn_univ_iff
-- 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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
⊢ HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
H.ftaylorSeriesWithin uniqueDiffOn_univ

Premises used: uniqueDiffOn_univ, ContDiffOn.ftaylorSeriesWithin
-- 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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
H : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ
⊢ HasFTaylorSeriesUpToOn (↑n : ℕ∞ω) f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
exact H.ftaylorSeriesWithin uniqueDiffOn_univ

Premises used: uniqueDiffOn_univ, ContDiffOn.ftaylorSeriesWithin
-- 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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f p
x : E
h : Membership.mem (γ := Set E) univ x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[insert x univ] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

Tactic:
⟨univ, Filter.univ_sets _, p,
        (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩

Premises used: WithTop.coe_le_coe._simp_1, Set.univ, HasFTaylorSeriesUpToOn.of_le, cast, HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn, And.intro, Exists.intro, Eq.symm, Filter.univ_sets
-- 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
f : E → F
n_1 : ℕ∞ω
n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpTo (↑n : ℕ∞ω) f p
x : E
h : Membership.mem (γ := Set E) univ x
m : ℕ
hm : (↑m : ℕ∞) ≤ n
⊢ ∃ u ∈ 𝓝[insert x univ] x, ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m : ℕ∞ω) f p u

Tactic:
exact ⟨univ, Filter.univ_sets _, p,
        (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast 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
f : E → F
n : ℕ∞ω
⊢ ContDiffOn 𝕜 n f univ ↔ ContDiff 𝕜 n f

Tactic:
match n with
  | ω =>
    constructor
    · intro H
      use ftaylorSeriesWithin 𝕜 f univ
      rw [← hasFTaylorSeriesUpToOn_univ_iff]
      refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩
      rw [← analyticOn_univ]
      exact H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _
    · rintro ⟨p, hp, h'p⟩ x _
      exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top,
        fun i ↦ (h'p i).analyticOn⟩
  | (n : ℕ∞) =>
    constructor
    · intro H
      use ftaylorSeriesWithin 𝕜 f univ
      rw [← hasFTaylorSeriesUpToOn_univ_iff]
      exact H.ftaylorSeriesWithin uniqueDiffOn_univ
    · rintro ⟨p, hp⟩ x _ m hm
      exact ⟨univ, Filter.univ_sets _, p,
        (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast 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
f : E → F
n : ℕ∞ω
⊢ ContDiff 𝕜 n f ↔ ∀ (x : E), ContDiffAt 𝕜 n f x

Tactic:
simp [← contDiffOn_univ, ContDiffOn, ContDiffAt]

Premises used: ContDiffAt, ContDiffOn, contDiffOn_univ
-- 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
f : E → F
x : E
n : ℕ∞ω
h : ContDiff 𝕜 n f
⊢ ContDiffAt 𝕜 n f x

Tactic:
contDiff_iff_contDiffAt.1 h x

Premises used: Iff.mp, contDiff_iff_contDiffAt
-- 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 : ContDiff 𝕜 n f
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
h.contDiffAt.contDiffWithinAt

Premises used: ContDiffAt.contDiffWithinAt, ContDiff.contDiffAt
-- 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
f : E → F
⊢ ContDiff 𝕜 ∞ f ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
simp [contDiffOn_univ.symm, contDiffOn_infty]

Premises used: contDiffOn_infty, contDiffOn_univ, Iff.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
f : E → F
⊢ (∀ (n : ℕ∞), ContDiff 𝕜 (↑n : ℕ∞ω) f) ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n : ℕ∞ω) f

Tactic:
simp only [← contDiffOn_univ, contDiffOn_all_iff_nat]

Premises used: contDiffOn_all_iff_nat, contDiffOn_univ
-- 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
n : ℕ∞ω
h : ContDiff 𝕜 n f
⊢ ContDiffOn 𝕜 n f s

Tactic:
(contDiffOn_univ.2 h).mono (subset_univ _)

Premises used: Iff.mpr, Set.subset_univ, ContDiffOn.mono, contDiffOn_univ
-- 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
f : E → F
rw : ContDiffOn 𝕜 0 f univ ↔ ContinuousOn f univ
⊢ ContDiff 𝕜 0 f ↔
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      f

Tactic:
rw [← contDiffOn_univ, ← continuousOn_univ]

Premises used: continuousOn_univ, contDiffOn_univ
-- 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
f : E → F
⊢ ContDiffOn 𝕜 0 f univ ↔ ContinuousOn f univ

Tactic:
contDiffOn_zero

Premises used: contDiffOn_zero
-- 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
f : E → F
⊢ ContDiffOn 𝕜 0 f univ ↔ ContinuousOn f univ

Tactic:
exact contDiffOn_zero

Premises used: contDiffOn_zero
-- 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
f : E → F
x : E
⊢ ContDiffWithinAt 𝕜 0 f univ x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u

Tactic:
simp [contDiffWithinAt_zero, nhdsWithin_univ]

Premises used: nhdsWithin_univ, contDiffWithinAt_zero
-- 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
f : E → F
x : E
simp_rw :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑0 : ℕ∞ω) f' x) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
simp_rw₁ :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 0 f' x) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
simp_rw₂ :
  (∃ (f' : E → E →L[𝕜] F), (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ∃ u ∈ 𝓝 x, ContinuousOn f' u) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
simp_rw₃ :
  (∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, (∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContinuousOn f' u) ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x
⊢ ContDiffAt 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑0 : ℕ∞ω) 1) f x ↔
    ∃ (f' : E → E →L[𝕜] F), ∃ u ∈ 𝓝 x, ContinuousOn f' u ∧ ∀ x ∈ u, HasFDerivAt f (f' x) x

Tactic:
simp_rw [contDiffAt_succ_iff_hasFDerivAt, show ((0 : ℕ) : ℕ∞ω) = 0 from rfl,
    contDiffAt_zero, exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]

Premises used: antitone_continuousOn, and_comm, Set.antitone_bforall, contDiffAt_succ_iff_hasFDerivAt, Filter.exists_mem_and_iff, contDiffAt_zero, rfl
-- 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
f : E → F
m n : ℕ∞ω
h : ContDiff 𝕜 n f
hmn : m ≤ n
⊢ ContDiff 𝕜 m f

Tactic:
contDiffOn_univ.1 <| (contDiffOn_univ.2 h).of_le hmn

Premises used: Iff.mpr, ContDiffOn.of_le, Iff.mp, contDiffOn_univ
-- 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
f : E → F
n : ℕ∞ω
h : ContDiff 𝕜 (n + 1) f
⊢ ContDiff 𝕜 n f

Tactic:
h.of_le le_self_add

Premises used: ContDiff.of_le, le_self_add
-- 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
f : E → F
n : ℕ∞ω
h : ContDiff 𝕜 (n + 1) f
⊢ ContDiff 𝕜 1 f

Tactic:
apply h.of_le le_add_self

Premises used: ContDiff.of_le, le_add_self
-- 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
f : E → F
n : ℕ∞ω
h : ContDiff 𝕜 n f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
contDiff_zero.1 (h.of_le bot_le)

Premises used: contDiff_zero, ContDiff.of_le, Iff.mp, bot_le
-- 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
f : E → F
h : ContDiff 𝕜 0 f
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
contDiff_zero.1 (h.of_le bot_le)

Premises used: contDiff_zero, ContDiff.of_le, Iff.mp, bot_le
-- 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
f : E → F
n : ℕ∞ω
h : ContDiff 𝕜 n f
hn : n ≠ 0
⊢ Differentiable 𝕜 f

Tactic:
differentiableOn_univ.1 <| (contDiffOn_univ.2 h).differentiableOn hn

Premises used: Iff.mpr, differentiableOn_univ, ContDiffOn.differentiableOn, Iff.mp, contDiffOn_univ
-- 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
f : E → F
h : ContDiff 𝕜 1 f
⊢ Differentiable 𝕜 f

Tactic:
differentiableOn_univ.1 <| (contDiffOn_univ.2 h).differentiableOn one_ne_zero

Premises used: Iff.mpr, differentiableOn_univ, ContDiffOn.differentiableOn, Iff.mp, one_ne_zero, contDiffOn_univ
-- 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
f : E → F
n : ℕ∞
simp_rw : ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiffOn 𝕜 (↑m : ℕ∞ω) f univ
⊢ ContDiff 𝕜 (↑n : ℕ∞ω) f ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiff 𝕜 (↑m : ℕ∞ω) f

Tactic:
simp_rw [← contDiffOn_univ]

Premises used: contDiffOn_univ
-- 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
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiffOn 𝕜 (↑m : ℕ∞ω) f univ

Tactic:
contDiffOn_iff_forall_nat_le

Premises used: contDiffOn_iff_forall_nat_le
-- 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
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n : ℕ∞ω) f univ ↔ ∀ (m : ℕ), (↑m : ℕ∞) ≤ n → ContDiffOn 𝕜 (↑m : ℕ∞ω) f univ

Tactic:
exact contDiffOn_iff_forall_nat_le

Premises used: contDiffOn_iff_forall_nat_le
-- 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
f : E → F
n : ℕ
⊢ ContDiff 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑n : ℕ∞ω) 1) f ↔
    ∃ (f' : E → E →L[𝕜] F), ContDiff 𝕜 (↑n : ℕ∞ω) f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x

Tactic:
simp only [← contDiffOn_univ, ← hasFDerivWithinAt_univ, Set.mem_univ, forall_true_left,
    contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn uniqueDiffOn_univ,
    WithTop.natCast_ne_top, analyticOn_univ, false_implies, true_and]

Premises used: forall_true_left, false_implies, uniqueDiffOn_univ, WithTop.natCast_ne_top, analyticOn_univ, Set.mem_univ, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, contDiffOn_univ, hasFDerivWithinAt_univ, true_and
-- 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
f : E → F
⊢ ContDiff 𝕜 (HAdd.hAdd (α := ℕ∞ω) (↑0 : ℕ∞ω) 1) f ↔
    ∃ (f' : E → E →L[𝕜] F), ContDiff 𝕜 (↑0 : ℕ∞ω) f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x

Tactic:
contDiff_succ_iff_hasFDerivAt

Premises used: contDiff_succ_iff_hasFDerivAt
-- 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
f : E → F
h :
  ∀ (x : E → E →L[𝕜] F), Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] x ↔ ContDiff 𝕜 (↑0 : ℕ∞ω) x
⊢ ContDiff 𝕜 1 f ↔
    ∃ (f' : E → E →L[𝕜] F),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x

Tactic:
convert! contDiff_succ_iff_hasFDerivAt using 4

Premises used: contDiff_succ_iff_hasFDerivAt
-- 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
f : E → F
x : E → E →L[𝕜] F
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] x ↔ ContDiff 𝕜 (↑0 : ℕ∞ω) x

Tactic:
simp
-- 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
f : E → F
n : ℕ∞ω
hf : AnalyticOn 𝕜 f univ
rw : ContDiffOn 𝕜 n f univ
⊢ ContDiff 𝕜 n f

Tactic:
rw [← contDiffOn_univ]

Premises used: contDiffOn_univ
-- 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
f : E → F
n : ℕ∞ω
hf : AnalyticOn 𝕜 f univ
⊢ ContDiffOn 𝕜 n f univ

Tactic:
hf.contDiffOn (n := n) uniqueDiffOn_univ

Premises used: AnalyticOn.contDiffOn, uniqueDiffOn_univ
-- 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
f : E → F
n : ℕ∞ω
hf : AnalyticOn 𝕜 f univ
⊢ ContDiffOn 𝕜 n f univ

Tactic:
exact hf.contDiffOn (n := n) uniqueDiffOn_univ

Premises used: AnalyticOn.contDiffOn, uniqueDiffOn_univ
-- 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
f : E → F
n : ℕ∞ω
hf : AnalyticOnNhd 𝕜 f univ
⊢ ContDiff 𝕜 n f

Tactic:
hf.analyticOn.contDiff

Premises used: AnalyticOnNhd.analyticOn, AnalyticOn.contDiff
-- 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
h : ContDiff 𝕜 ω f
⊢ ContDiffOn 𝕜 ω f univ

Tactic:
rw [← contDiffOn_univ] at h

Premises used: contDiffOn_univ
-- 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
h : ContDiffOn 𝕜 ω f univ
⊢ AnalyticOn 𝕜 f univ

Tactic:
have := h.analyticOn
-- 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
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOn 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f univ

Tactic:
rw [analyticOn_univ] at this

Premises used: analyticOn_univ
-- 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
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOnNhd 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
this.mono (subset_univ _)

Premises used: Set.subset_univ, AnalyticOnNhd.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
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOnNhd 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
exact this.mono (subset_univ _)

Premises used: Set.subset_univ, AnalyticOnNhd.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
f : E → F
⊢ ContDiff 𝕜 ω f ↔ AnalyticOnNhd 𝕜 f univ

Tactic:
⟨fun h ↦ h.analyticOnNhd, fun h ↦ h.contDiff⟩

Premises used: AnalyticOnNhd.contDiff, Iff.intro, ContDiff.analyticOnNhd