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

Goal state before:
pp: case succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < (a.sigmaCompositionAux b ⟨i, ⋯⟩).length
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
⊢ a.sizeUpTo (b.sizeUpTo i + j) + a.blocks[b.sizeUpTo i + j] =
    (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo (j + 1)

Tactic:
IHj A,

Goal state after:
case succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < (a.sigmaCompositionAux b ⟨i, ⋯⟩).length
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
⊢ (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j + a.blocks[b.sizeUpTo i + j] =
    (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo (j + 1)
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case succ
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (f ^ m) s z
⊢ AnalyticWithinAt 𝕜 (f ^ (m + 1)) s z

Tactic:
simp only [pow_succ]

Goal state after:
case succ
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (f ^ m) s z
⊢ AnalyticWithinAt 𝕜 (f ^ m * f) s z
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →L[𝕜] E [⋀^ι]→L[𝕜] G
v : ι → E
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f).flipMultilinear.toFun v = 0

Tactic:
ext x; simp [(f x).map_eq_zero_of_eq v hv hne]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x : F
⊢ max (C * ‖x‖) 0 = max C 0 * ‖x‖

Tactic:
rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

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

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
x : E
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
m : ℕ
hmn : ↑m ≤ n
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ p x m = iteratedFDerivWithin 𝕜 m f s x

Tactic:
by
  induction m generalizing x with
  | zero => rw [h.zero_eq' hx, iteratedFDerivWithin_zero_eq_comp, comp_apply]
  | succ m IH =>
    have A : m < n := lt_of_lt_of_le (mod_cast lt_add_one m) hmn
    have :
      HasFDerivWithinAt (fun y : E => iteratedFDerivWithin 𝕜 m f s y)
        (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x :=
      (h.fderivWithin m A x hx).congr (fun y hy => (IH (le_of_lt A) hy).symm)
        (IH (le_of_lt A) hx).symm
    rw [iteratedFDerivWithin_succ_eq_comp_left, Function.comp_apply, this.fderivWithin (hs x hx)]
    exact (ContinuousMultilinearMap.uncurry_curryLeft _).symm

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

Goal state before:
pp: case step
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih : ↑l ≤ n → (tsupport fun x ↦ p x l) ⊆ tsupport fun x ↦ p x k
h2 : ↑l.succ ≤ n
hl : ↑l < n
⊢ (tsupport fun x ↦ p x l.succ) = tsupport (fderiv 𝕜 fun x ↦ p x l)

Tactic:
rw [funext <| hf.fderiv_eq (mod_cast hl)]

Goal state after:
case step
𝕜 : 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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
k m : ℕ
hf : HasFTaylorSeriesUpTo n f p
l : ℕ
h : k.le l
ih : ↑l ≤ n → (tsupport fun x ↦ p x l) ⊆ tsupport fun x ↦ p x k
h2 : ↑l.succ ≤ n
hl : ↑l < n
⊢ (tsupport fun x ↦ p x l.succ) = tsupport fun x ↦ (p x l.succ).curryLeft
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
s : Set E
inst✝ : CompleteSpace F
y : E
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
h : HasFPowerSeriesWithinOnBall f p s y r
hy : y ∈ insert y s ∩ Metric.eball y r
⊢ DifferentiableWithinAt 𝕜 f (insert y s ∩ Metric.eball y r) y

pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y

Tactic:
· exact Z.mono inter_subset_left

Goal state after:
case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
n : WithTop ℕ∞
h : AnalyticWithinAt 𝕜 f s x
g : E → F
fg : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
v : Set E
vx : v ∈ 𝓝 x
hv : AnalyticOnNhd 𝕜 g v
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ ftaylorSeries 𝕜 g x i) (insert x s ∩ v)

Tactic:
exact (hv.iteratedFDeriv i).analyticOn.mono Set.inter_subset_right

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x

Tactic:
have := (h.iteratedFDerivWithin hu m x hx).differentiableWithinAt.hasFDerivWithinAt

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
n : WithTop ℕ∞
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
m : ℕ
_hm : ↑m < n
x : E
hx : x ∈ s
this :
  HasFDerivWithinAt (iteratedFDerivWithin 𝕜 m f s) (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 m f s) (insert x s) x)
    (insert x s) x
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) (ftaylorSeriesWithin 𝕜 f s x m.succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case neg.h
𝕜 : 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
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
hke : ⟨k, ⋯⟩ = ((Equiv.embeddingFinSucc n ι) e).snd
⊢ e 0 ∈ range ⇑e

Tactic:
exact Set.mem_range_self _

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t)))

Tactic:
← Submodule.topologicalClosure_coe

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
⊢ derivWithin f s x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_3.e'_5
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ n + 1 = (Finset.powersetCard n Finset.univ).card

Tactic:
Finset.card_powersetCard,

Goal state after:
case e'_3.e'_5
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
x : E
⊢ n + 1 = Finset.univ.card.choose n
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ (h x)
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Tactic:
exact deriv.scomp x hg hh

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
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
⊢ m = n

Tactic:
let ⟨g, hg_an, _, hg_eq⟩ := hm

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
⊢ m = n
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ x ^ (↑m - 1) = x ^ (m - 1)

Tactic:
rw [← Int.ofNat_one, ← Int.ofNat_sub, zpow_natCast]

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ 1 ≤ m
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), fderiv 𝕜 f x = 0
x✝¹ y : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x : E
x✝ : x ∈ univ
⊢ fderiv 𝕜 f x = 0

Tactic:
exact hf' x

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

Goal state before:
pp: 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
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖

Tactic:
filter_upwards [this] with x ⟨h_segment, h⟩

Goal state after:
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
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case refine_2
𝕜 : 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
f : E → F
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ (p (g x) i).compContinuousLinearMap fun x ↦ g) (⇑g ⁻¹' u)

Tactic:
change AnalyticOn 𝕜 (fun x ↦
        ContinuousMultilinearMap.compContinuousLinearMapL (fun _ ↦ g) (p (g x) i)) (⇑g ⁻¹' u)

Goal state after:
case refine_2
𝕜 : 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
f : E → F
n : ℕ∞ω
x : G
g : G →L[𝕜] E
u : Set E
hu : u ∈ 𝓝[insert (g x) s] g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ (ContinuousMultilinearMap.compContinuousLinearMapL fun x ↦ g) (p (g x) i)) (⇑g ⁻¹' u)
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case succ
𝕜 : 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 ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
this :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x =
    fderivWithin 𝕜 (⇑(continuousMultilinearMapCongrLeft F fun _x ↦ g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g) (⇑g ⁻¹' s) x
⊢ (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x) ∘SL ↑g) (m 0)) fun i_1 ↦ g (tail m i_1)) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i ↦ g (m i))

Tactic:
ContinuousLinearMap.comp_apply,

Goal state after:
case succ
𝕜 : 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 ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
this :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x =
    fderivWithin 𝕜 (⇑(continuousMultilinearMapCongrLeft F fun _x ↦ g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g) (⇑g ⁻¹' s) x
⊢ (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (↑g (m 0))) fun i_1 ↦ g (tail m i_1)) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i ↦ g (m i))
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
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn ω f p s
h : AnalyticOn 𝕜 (fun x ↦ p x 0) s
⊢ AnalyticOn 𝕜 f s

Tactic:
have : AnalyticOn 𝕜 (fun x ↦ (continuousMultilinearCurryFin0 𝕜 E F) (p x 0)) s :=
    (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn
      h (Set.mapsTo_univ _ _)
  exact this.congr (fun y hy ↦ (hf.zero_eq _ hy).symm)

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

Goal state before:
pp: n plength : ℕ
psize : Fin plength → ℕ
partSize_pos✝¹ : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono✝¹ : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono✝¹ : StrictMono fun m ↦ pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m ↦ range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos✝ : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m ↦ qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m ↦ range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq :
  embSigma n
      { length := plength, partSize := psize, partSize_pos := partSize_pos✝¹, emb := pemb,
        emb_strictMono := emb_strictMono✝¹, parts_strictMono := parts_strictMono✝¹, disjoint := disjoint✝¹,
        cover := cover✝¹ } =
    embSigma n
      { length := qlength, partSize := qsize, partSize_pos := partSize_pos✝, emb := qemb,
        emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝,
        cover := cover✝ }
⊢ { length := plength, partSize := psize, partSize_pos := partSize_pos✝¹, emb := pemb,
      emb_strictMono := emb_strictMono✝¹, parts_strictMono := parts_strictMono✝¹, disjoint := disjoint✝¹,
      cover := cover✝¹ } =
    { length := qlength, partSize := qsize, partSize_pos := partSize_pos✝, emb := qemb,
      emb_strictMono := emb_strictMono✝, parts_strictMono := parts_strictMono✝, disjoint := disjoint✝, cover := cover✝ }

Tactic:
simp_all only [Sigma.mk.inj_iff, true_and, mk.injEq, Fin.mk.injEq, embSigma]

Goal state after:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos✝¹ : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono✝¹ : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono✝¹ : StrictMono fun m ↦ pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m ↦ range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos✝ : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m ↦ qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m ↦ range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq : plength = qlength ∧ ⟨fun m ↦ ⟨psize m, ⋯⟩, fun j ↦ pemb j⟩ ≍ ⟨fun m ↦ ⟨qsize m, ⋯⟩, fun j ↦ qemb j⟩
⊢ psize ≍ qsize ∧ pemb ≍ qemb
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ e.restr (e.source ∩ s) = e.restr s

Tactic:
refine OpenPartialHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) ?_
  simp [e.open_source.interior_eq, ← inter_assoc]

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

Goal state before:
pp: case mpr
𝕜 : 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 :
  ∀ x ∈ s,
    ∃ u ∈ 𝓝[insert x s] x,
      (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
x : E
hx : x ∈ s
u : Set E
u_nhbd : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hu : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffOn 𝕜 n f' u
this : x ∈ u
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x

Tactic:
exact ⟨u, u_nhbd, f_an, f', hu, hf' x this⟩

Goal state after: