mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : IsEmpty ι
⊢ (∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

pp: case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ (∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))

Tactic:
· have (l : _) : 1 + l ≠ Fintype.card ι := by
      rw [add_comm, Fintype.card_eq_zero]; exact Nat.succ_ne_zero _
    simp_rw [Fintype.sum_empty, changeOriginSeries_support _ (this _), _root_.zero_apply _,
      tsum_zero]; rfl

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ (∑' (n : ℕ), (f.toFormalMultilinearSeries.changeOriginSeries 1 n) fun x_1 ↦ x) (Fin.snoc 0 y) =
    ∑ i, f (Function.update x i (y i))
Module: Mathlib.Analysis.Analytic.Uniqueness

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : E [×n + 1]→L[𝕜] F
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < min (δ * ‖y‖⁻¹) (ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹)
h₁ : ‖k • y‖ < δ
⊢ c * (‖k‖ ^ (n.succ + 1) * ‖y‖ ^ (n.succ + 1)) = ‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s : Set 𝕜
⊢ IsSeparable (range (derivWithin f s))

Tactic:
obtain ⟨t, ts, t_count, ht⟩ : ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t :=
    (IsSeparable.of_separableSpace s).exists_countable_dense_subset

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ IsSeparable (range (derivWithin f s))
Module: Mathlib.Analysis.Complex.ReImTopology

Goal state before:
pp: a : ℝ
⊢ frontier {z | a ≤ z.re} = {z | z.re = a}

Tactic:
simpa only [frontier_Ici] using! frontier_preimage_re (Ici a)

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| (List.map (fun i ↦ (List.map x (l.erase i)).prod •> proj i) l).sum

Tactic:
arg 1; arg 2; rw [← List.map_get_finRange l]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
| List.map l.get (List.finRange l.length)
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: R₁ R₂ θ₁ θ₂ : ℝ
⊢ ↑R₁ * cexp (↑θ₁ * I) * (↑R₂ * cexp (↑θ₂ * I)) = ↑R₁ * ↑R₂ * (cexp (↑θ₁ * I) * cexp (↑θ₂ * I))

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: R₁ R₂ θ₁ θ₂ : ℝ
⊢ ↑R₁ * cexp (↑θ₁ * I) / (↑R₂ * cexp (↑θ₂ * I)) = ↑R₁ / ↑R₂ * (cexp (↑θ₁ * I) / cexp (↑θ₂ * I))

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst✝³ : NormedCommRing 𝔸'
inst✝² : NormedAlgebra 𝕜 𝔸'
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
i : Fin l.length
x✝¹ : i ∈ Finset.univ
x✝ : ι → 𝔸'
⊢ (List.map x (List.take (↑i) l)).prod * ((List.map x (List.drop (↑i + 1) l)).prod * (proj l[↑i]) x✝) =
    (List.map x (List.take (↑i) l)).prod * (List.map x (List.drop (↑i + 1) l)).prod * (proj l[↑i]) x✝

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: c : ℂ
R θ : ℝ
⊢ circleMap c R (θ + 2 * π) = circleMap c R θ

Tactic:
by
  simp [circleMap, add_mul, exp_periodic _]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
n : ℤ
hn : ↑a * I = ↑b * I + ↑n * (2 * ↑π * I)
⊢ ↑n * (2 * ↑π * I) = ↑n * 2 * ↑π * I

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this : (fun p ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p ↦ (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ (y - z) * (y * z - x ^ 2) = x ^ 2 * (z - y) + y * z * (y - z)

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ -c' / c x ^ 2 = -(c x ^ 2)⁻¹ * c'

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ c' * d x - c x * d' = c' * d x + -(c x * d')

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: case e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ c' * d x - c x * d' = c' * d x + -(c x * d')

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Shift

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (a + x)) s x = derivWithin f (a +ᵥ s) (a + x)

Tactic:
simp only [derivWithin, fderivWithin_comp_add_left]

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
h₂f : ¬EventuallyConst f (𝓝 x)
hs : s ∈ 𝓝[≠] f x
⊢ f ⁻¹' s ∈ 𝓝[≠] x

Tactic:
have : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s := by
    filter_upwards [hfx.continuousAt.preimage_mem_nhds (insert_mem_nhds_iff.2 hs)]
    tauto
  contrapose h₂f with h
  rw [eventuallyConst_iff_exists_eventuallyEq]
  use f x
  rw [EventuallyEq, ← hfx.frequently_eq_iff_eventually_eq analyticAt_const]
  apply ((frequently_imp_distrib_right.2 h).and_eventually
    (eventually_nhdsWithin_of_eventually_nhds this)).mono
  intro z ⟨h₁z, h₂z⟩
  rw [Set.mem_insert_iff] at h₂z
  tauto

Goal state after:
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜' → 𝕜'
g : 𝕜 → 𝕜'
x : 𝕜
hf : DifferentiableAt 𝕜' f (g x)
hg : DifferentiableAt 𝕜 g x
⊢ deriv f (g x) * deriv g x / f (g x) = deriv f (g x) / f (g x) * deriv g x

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : IsRCLikeNormedField 𝕜
f g : 𝕜 → 𝕜'
s : Set 𝕜
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsc : IsPreconnected s
hgn : ∀ x ∈ s, g x ≠ 0
hfn : ∀ x ∈ s, f x ≠ 0
t : 𝕜
ht : t ∈ s
h : EqOn (logDeriv f) (logDeriv g) s
y : 𝕜
hy : y ∈ s
z : 𝕜
hz : z ∈ s
⊢ deriv f z * (g z)⁻¹ + -(f z * ((g z ^ 2)⁻¹ * deriv g z)) = deriv f z * (g z)⁻¹ - f z * deriv g z / g z ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : ℝ → E := fun x ↦ f x - f a
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)

Tactic:
have hg : ContinuousOn g (Icc a b) := hf.sub continuousOn_const

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
f' : ℝ → E
C : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C
g : ℝ → E := fun x ↦ f x - f a
hg : ContinuousOn g (Icc a b)
⊢ ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a)
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
⊢ ∃ a, ∀ x ∈ s, f x = a

Tactic:
refine ⟨f y, fun x hx ↦ ?_⟩
    have h₁ := hs.isOpen_inter_preimage_of_fderiv_eq_zero hf hf' {f y}
    have h₂ := hf.continuousOn.comp_continuous continuous_subtype_val (fun x ↦ x.2)
    by_contra h₃
    obtain ⟨t, ht, ht'⟩ := (isClosed_singleton (x := f y)).preimage h₂
    have ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y := by simpa [Set.ext_iff] using ht'
    obtain ⟨z, H₁, H₂, H₃⟩ := hs' _ _ h₁ ht (fun x h ↦ by simp [h, ht'', eq_or_ne]) ⟨y, by simpa⟩
      ⟨x, by simp [ht'' _ hx, hx, h₃]⟩
    exact (ht'' _ H₁).mp H₃ H₂.2

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : G ≃ₗᵢ[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
this :
  iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑↑g
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Tactic:
rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
i : ℕ
hi : ↑i ≤ n
x : E
hx : x ∈ s
u : F
m : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u

Tactic:
by
  induction i generalizing x with
  | zero => simp
  | succ i ih =>
    replace hi : (i : ℕ∞ω) < n := lt_of_lt_of_le (by norm_cast; simp) hi
    have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
      (hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
    have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
      hc.differentiableOn_iteratedFDerivWithin hi hs
    simp only [iteratedFDerivWithin_succ_apply_left]
    rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]
    rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
    rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
      (differentiableWithinAt_const u)]
    rw [fderivWithin_const_apply]
    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]
    rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
n : ℕ∞ω
hf : ContDiffOn 𝕜 n f s
hf' : ContDiffOn 𝕜 n f t
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ContDiffOn 𝕜 n f (s ∪ t)

Tactic:
by
  rintro x (hx | hx)
  · exact (hf x hx).contDiffAt (hs.mem_nhds hx) |>.contDiffWithinAt
  · exact (hf' x hx).contDiffAt (ht.mem_nhds hx) |>.contDiffWithinAt

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ω g s x₀
hmn : ω + 1 ≤ n
this : ∀ (k : ℕ), ↑k ≤ ω → ContDiffWithinAt 𝕜 (↑k) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 ω (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
obtain rfl : n = ω := by simpa using hmn

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x₀ : E
m : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ω g s x₀
this : ∀ (k : ℕ), ↑k ≤ ω → ContDiffWithinAt 𝕜 (↑k) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
hf : ContDiffWithinAt 𝕜 ω (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hmn : ω + 1 ≤ ω
⊢ ContDiffWithinAt 𝕜 ω (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f

Tactic:
iteratedDeriv_eq_equiv_comp,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedFDeriv 𝕜 n f =
    ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘
      ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[u] x
v'u : v ⊆ u
hv : ContDiffOn 𝕜 n f' v
xu : x ∈ u
⊢ ∃ u ∈ 𝓝[s] x, (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
exact ⟨v, nhdsWithin_le_of_mem hu vu, fun h ↦ (f_an h).mono v'u, f',
      fun y hy ↦ (hf' y (v'u hy)).mono v'u, hv⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖

Tactic:
iteratedDeriv_eq_equiv_comp,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ ‖iteratedFDeriv 𝕜 n f x‖ = ‖(⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f) x‖
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).index 0 ≠ i
⊢ (c.extendMiddle i).emb i 0 ≠ (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)

Tactic:
exact (c.extendMiddle i).emb_ne_emb_of_ne (Ne.symm this)

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg.refine_2
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ c.emb i (Fin.cast ⋯ j) ≠ c.emb (c.index 0) (c.invEmbedding 0)

Tactic:
exact c.emb_ne_emb_of_ne h

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_3.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩) = ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩)

pp: case e'_3.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ 1 ≤ ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)

Tactic:
· congr; omega

Goal state after:
case e'_3.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ 1 ≤ ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x✝ : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ f', ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
h : ∃ f', ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s

Tactic:
rcases h with ⟨f', h1, h2⟩

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x✝ : (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ f', ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
f_an : n = ω → AnalyticOn 𝕜 f s
f' : E → E →L[𝕜] F
h1 : ContDiffOn 𝕜 n f' s
h2 : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 ∞ f x ↔ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) f x

Tactic:
by
  simp [← contDiffWithinAt_univ, contDiffWithinAt_infty]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case hs
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
hs : UniqueDiffOn 𝕜 s
h : ContDiffAt 𝕜 (↑n) f x
hx : x ∈ s
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : ContDiffOn 𝕜 (↑n) f (insert x univ ∩ u)
⊢ UniqueDiffOn 𝕜 (s ∩ u)

Tactic:
exact hs.inter u_open

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → HasFTaylorSeriesUpTo (↑n) f (ftaylorSeries 𝕜 f)

Tactic:
← hasFTaylorSeriesUpToOn_univ_iff,

Goal state after:
case mp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ → HasFTaylorSeriesUpToOn (↑n) f (ftaylorSeries 𝕜 f) univ