mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
⊢ C * (a * (‖y‖ / ↑r')) ^ n ≤ C * a ^ n

Tactic:
have := ha.1.le

Goal state after:
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
this : 0 ≤ a
⊢ C * (a * (‖y‖ / ↑r')) ^ n ≤ C * a ^ n
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
⊢ ∀ b ∈ Finset.range (Fintype.card ι + 1), b ≠ Fintype.card ι → ((f.toFormalMultilinearSeries b) fun x ↦ y) = 0

Tactic:
intro m _ ne

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
x✝ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card ι + 1)
ne : m ≠ Fintype.card ι
⊢ ((f.toFormalMultilinearSeries m) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
a✝ : y ∈ Metric.eball 0 ∞
⊢ ∀ b ∈ Finset.range (Fintype.card (Option ι) + 1),
    b ≠ Fintype.card (Option ι) → ((f.toFormalMultilinearSeriesOfMultilinear b) fun x ↦ y) = 0

Tactic:
intro m _ ne

Goal state after:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
a✝¹ : y ∈ Metric.eball 0 ∞
m : ℕ
a✝ : m ∈ Finset.range (Fintype.card (Option ι) + 1)
ne : m ≠ Fintype.card (Option ι)
⊢ ((f.toFormalMultilinearSeriesOfMultilinear m) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case h₁
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := ⋯
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := ⋯
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := ⋯
n : ℕ
this : 0 < a
⊢ ‖p (n + 2)‖ ≤ C * a ^ (n + 2) / ↑r' ^ (n + 2)

pp: case hab
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := ⋯
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := ⋯
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := ⋯
n : ℕ
this : 0 < a
⊢ ‖y - (x, x)‖ ≤ ↑r'

Tactic:
· apply hp

Goal state after:
case hab
𝕜 : 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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := ⋯
y : E × E
hy' : ‖y - (x, x)‖₊ < r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := ⋯
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := ⋯
n : ℕ
this : 0 < a
⊢ ‖y - (x, x)‖ ≤ ↑r'
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case e_5
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : ⟨k, blocksFun⟩ ∈ compPartialSumSource 2 (n + 1) n
K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k
⊢ (fun j ↦ r * (a ^ ⟨k, blocksFun⟩.snd j * p (⟨k, blocksFun⟩.snd j))) ≍ fun j ↦
    r *
      (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun j *
        p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun j))

Tactic:
Fin.heq_fun_iff K.symm

Goal state after:
case e_5
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
k : ℕ
blocksFun : Fin k → ℕ
H : ⟨k, blocksFun⟩ ∈ compPartialSumSource 2 (n + 1) n
K : (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.length = k
⊢ ∀ (i : Fin k),
    r * (a ^ ⟨k, blocksFun⟩.snd i * p (⟨k, blocksFun⟩.snd i)) =
      r *
        (a ^ (compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun ⟨↑i, ⋯⟩ *
          p ((compChangeOfVariables 2 (n + 1) n ⟨k, blocksFun⟩ H).snd.blocksFun ⟨↑i, ⋯⟩))
Module: Mathlib.Analysis.Analytic.Composition

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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
this✝ : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
δ : ℝ≥0∞
δpos : δ > 0
Hδ : Metric.eball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ Metric.eball (f x) rg)
z : E
hz : z ∈ insert x s ∩ Metric.eball x δ
⊢ z ∈ Metric.eball x δ ∩ insert x s

Tactic:
Set.inter_comm

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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
this✝ : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
δ : ℝ≥0∞
δpos : δ > 0
Hδ : Metric.eball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ Metric.eball (f x) rg)
z : E
hz : z ∈ insert x s ∩ Metric.eball x δ
⊢ z ∈ insert x s ∩ Metric.eball x δ
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case hbc
𝕜 : 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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ ∑ k ∈ Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖ ≤
    ∑ x_1 ∈ Ico 2 (n + 1), r ^ x_1 * (∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ x_1

Tactic:
apply
        radius_right_inv_pos_of_radius_pos_aux1 n (fun k => ‖p.rightInv i x k‖)
          (fun k => norm_nonneg _) hr ha

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
st : t ∩ s ⊆ {x}
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
ys : x + y ∈ insert x s
yr : y ∈ eball 0 (ENNReal.ofReal r)
⊢ HasSum (fun n ↦ (constFormalMultilinearSeries 𝕜 E (f x) n) fun x ↦ y) (f (x + y))

Tactic:
simp only [subset_singleton_iff, mem_inter_iff, and_imp] at st

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : {x} ∈ 𝓝[s] x
t : Set E
ot : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
r : ℝ
r0 : r > 0
rt : ball x r ⊆ t
y : E
ys : x + y ∈ insert x s
yr : y ∈ eball 0 (ENNReal.ofReal r)
st : ∀ y ∈ t, y ∈ s → y = x
⊢ HasSum (fun n ↦ (constFormalMultilinearSeries 𝕜 E (f x) n) fun x ↦ y) (f (x + y))
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
⊢ i < (List.map sum (a.blocks.splitWrtComposition b)).length

Tactic:
simp [A]

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ (n + 1)) L

Tactic:
pow_succ

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L
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).succ = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo (j + 1)

Tactic:
sizeUpTo_succ _ D,

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.sizeUpTo (b.sizeUpTo i + 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: 𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := fun a ↦ a * z.inv
f2 : A → A := fun b ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun c ↦ 1 - z.inv * c
⊢ Metric.ball ↑z ‖↑z⁻¹‖⁻¹ ∈ 𝓝 ↑z

Tactic:
apply Metric.ball_mem_nhds

Goal state after:
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
f1 : A → A := ⋯
f2 : A → A := ⋯
f3 : A → A := ⋯
⊢ 0 < ‖↑z⁻¹‖⁻¹
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt 𝕜 (fun z ↦ ∏ n ∈ N, f n z) c

Tactic:
simp_rw [← analyticWithinAt_univ] at h ⊢
  exact N.analyticWithinAt_fun_prod h

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

Goal state before:
pp: case inr
𝕜 : 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
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
hc : c ≠ 0
⊢ fderivWithin 𝕜 (fun x ↦ f (c • x)) s x = c • fderivWithin 𝕜 f (c • s) (c • x)

Tactic:
rw [fderivWithin_comp_smul_eq_fderivWithin_smul, fderivWithin_const_smul_field]
    exact hs.smul hc

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completion

Goal state before:
pp: case hp
E : Type u_1
inst✝ : SeminormedAddCommGroup E
⊢ IsClosed {x | dist x.1 x.2 = ‖-x.1 + x.2‖}

Tactic:
refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_
      exact Continuous.comp Completion.continuous_extension (continuous_neg.fst.add continuous_snd)

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

Goal state before:
pp: case succ
𝕜 : 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 : ℕ
IH : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
⊢ tsupport (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) ⊆ tsupport f

Tactic:
exact closure_minimal ((support_comp_subset (map_zero _) _).trans
      ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure

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

Goal state before:
pp: 𝕜 : 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
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u

Tactic:
rcases hg.exists_mem_nhds_analyticOnNhd with ⟨v, vx, hv⟩

Goal state after:
𝕜 : 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
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this✝ : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
y : 𝕜
hy : y ∈ s \ {x}
⊢ 0 ≤ slope g x y

Tactic:
simp only [Set.mem_sdiff, mem_singleton_iff] at hy

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this✝ : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
y : 𝕜
hy : y ∈ s ∧ ¬y = x
⊢ 0 ≤ slope g x y
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case pos
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
hd : c = 0
⊢ (-1) ^ k * ↑k ! * c ^ k * deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z =
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * z + d) ^ (-1 - (1 + ↑k))

Tactic:
simp [hd]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁶ : NormedRing A
inst✝⁵ : IsDomain A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this✝ : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
cases frequently_or_distrib.mp this with
  | inl h => exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h
  | inr h => exact Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
⊢ f x - g x = f y - g y

Tactic:
refine hs.is_const_of_fderivWithin_eq_zero (hf.sub hg) (fun z hz => ?_) hx hy

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 g : E → G
s : Set E
x : E
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : EqOn (fderivWithin 𝕜 f s) (fderivWithin 𝕜 g s) s
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
⊢ fderivWithin 𝕜 (f - g) s z = 0
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x y : 𝕜
hx : x ∈ s
hy : y ∈ s
a : 𝕜
ha : a ∈ s
⊢ fderiv 𝕜 f a = 0 a

Tactic:
by
    ext; simp [← toSpanSingleton_deriv, hf' ha]

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
f : E → F
g : F → G
x : E
n : ℕ∞ω
t : Set F
hg : ContDiffWithinAt 𝕜 n g t (f x)
hf : ContDiffWithinAt 𝕜 n f s x
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hxs : x ∈ s
hst : ∀ᶠ (y : E) in 𝓝[s] x, f y ∈ t
i : ℕ
hi : ↑i ≤ n
hxt : f x ∈ t
hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] f x)
H₁ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) u
H₂ : ∀ᶠ (u : Set E) in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' u)
u : Set E
hu :
  ∀ ⦃x : Set E⦄,
    x ∈ 𝒫 (u ∩ s) →
      HasFTaylorSeriesUpToOn (↑i) f (ftaylorSeriesWithin 𝕜 f s) x ∧
        HasFTaylorSeriesUpToOn (↑i) g (ftaylorSeriesWithin 𝕜 g t) (f '' x)
hxu : x ∈ u
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
⊢ s ∩ u ∈ 𝒫 (u ∩ s)

Tactic:
by simp [inter_comm]

Goal state after:
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
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ 0
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑1) f p u
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
tu : t ∩ insert x s ⊆ u
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x

Tactic:
rw [inter_comm] at tu

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
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ 0
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn (↑1) f p u
t : Set E
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xt : x ∈ t
tu : insert x s ∩ t ⊆ u
⊢ DifferentiableWithinAt 𝕜 f (insert x s) x