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

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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
⊢ ‖(p.changeOriginSeries k l) fun x_1 ↦ x‖₊ ≤ (∑' (x : { s // s.card = l }), ‖p (k + l)‖₊) * ‖x‖₊ ^ l

Tactic:
← Fin.prod_const

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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
⊢ ‖(p.changeOriginSeries k l) fun x_1 ↦ x‖₊ ≤ (∑' (x : { s // s.card = l }), ‖p (k + l)‖₊) * ∏ _i, ‖x‖₊
Module: Mathlib.Analysis.Analytic.ChangeOrigin

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤ ∑' (y : { s // s.card = n }), ‖p (k + ⟨n, y⟩.fst)‖₊ * r ^ ⟨n, y⟩.fst

Tactic:
simp only [NNReal.tsum_mul_right]

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤ (∑' (x : { s // s.card = n }), ‖p (k + n)‖₊) * r ^ n
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius = ∞ → ∀ (r : ℝ≥0), Summable fun n ↦ ‖p n‖ * ↑r ^ n

Tactic:
intro h r
    obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
      (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)
    refine .of_norm_bounded
      (g := fun n ↦ (C : ℝ) * a ^ n) ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
      fun n ↦ ?_
    specialize hp n
    rwa [Real.norm_of_nonneg (by positivity)]

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

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f s y

Tactic:
by
  have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using! h.2
  have := hf.changeOrigin this (by simpa using! h.1)
  rw [add_sub_cancel] at this
  exact this.analyticWithinAt

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

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
x : E
m n : ℕ
hmn : n ≤ m
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f p x n r
⊢ HasFiniteFPowerSeriesAt f p x m

Tactic:
exact ⟨r, hr.of_le hmn⟩

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

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
hkl : n ≤ k + l
⊢ (ContinuousMultilinearMap.curryFinFinset 𝕜 E F hs ⋯) 0 = 0

Tactic:
map_zero

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
hkl : n ≤ k + l
⊢ 0 = 0
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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
⊢ x ∈ s + {y} → AnalyticAt 𝕜 (fun z ↦ f (z - y)) x

Tactic:
hx

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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x ∈ s + {y}
⊢ AnalyticAt 𝕜 (fun z ↦ f (z - y)) x
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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
⊢ x ∈ s + {y} → AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + {y}) x

Tactic:
hx

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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x ∈ s + {y}
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + {y}) x
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mp
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
⊢ HasFPowerSeriesWithinAt f p s x → ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

pp: case mpr
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) → HasFPowerSeriesWithinAt f p s x

Tactic:
· intro ⟨r, h⟩
    rcases hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mp h with ⟨g, e, h⟩
    refine ⟨g, ?_, ⟨r, h⟩⟩
    refine Filter.eventuallyEq_iff_exists_mem.mpr ⟨_, ?_, e⟩
    exact inter_mem_nhdsWithin _ (eball_mem_nhds _ h.r_pos)

Goal state after:
case mpr
𝕜 : 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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) → HasFPowerSeriesWithinAt f p s x
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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
let ⟨_p, hp⟩ := hf

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
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
_q : FormalMultilinearSeries 𝕜 F G
hq : HasFPowerSeriesWithinAt g _q t (f x)
_p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f _p s x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x
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)
⊢ a.sizeUpTo (b.sizeUpTo i + (j + 1)) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo (j + 1)

Tactic:
have D : sizeUpTo b i + j < length a := lt_of_lt_of_le C (b.sizeUpTo_le _)

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
⊢ a.sizeUpTo (b.sizeUpTo i + (j + 1)) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo (j + 1)
Module: Mathlib.Analysis.Analytic.Inverse

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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E)) ((p.leftInv i a).comp p) a
x : E
⊢ x ∈ f.source → (ContinuousLinearMap.id 𝕜 E) x = (↑f.symm ∘ ↑f) x

Tactic:
hx

Goal state after:
𝕜 : 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 : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E)) ((p.leftInv i a).comp p) a
x : E
hx : x ∈ f.source
⊢ (ContinuousLinearMap.id 𝕜 E) x = (↑f.symm ∘ ↑f) x
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ (pf.unshift z).radius

Tactic:
rw [FormalMultilinearSeries.radius_unshift]

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius
Module: Mathlib.Analysis.Analytic.Inverse

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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) (↑f.symm (↑f y))
x : E
⊢ HasSum (fun n ↦ (p.leftInv i a n) fun x_1 ↦ ↑f x - ↑f a) (↑f.symm (↑f x)) →
    x ∈ f.source → HasSum (fun n ↦ (p.leftInv i a n) fun x_1 ↦ ↑f x - ↑f a) x

Tactic:
hx

Goal state after:
𝕜 : 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 : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 0, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
C : ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) (↑f.symm (↑f y))
x : E
hx : HasSum (fun n ↦ (p.leftInv i a n) fun x_1 ↦ ↑f x - ↑f a) (↑f.symm (↑f x))
⊢ x ∈ f.source → HasSum (fun n ↦ (p.leftInv i a n) fun x_1 ↦ ↑f x - ↑f a) x
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ (pf.unshift z).radius

Tactic:
rw [FormalMultilinearSeries.radius_unshift]

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius
Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
⊢ ((fun p_1 ↦ b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x ↦ (p, p) + x) =o[𝓝 0]
    ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (p, p) + x)

Tactic:
set T := (E × F) × E × F

Goal state after:
𝕜 : 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
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ ((fun p_1 ↦ b p_1.1 - b p_1.2 - (h.deriv p) (p_1.1 - p_1.2)) ∘ fun x ↦ (p, p) + x) =o[𝓝 0]
    ((fun p ↦ p.1 - p.2) ∘ fun x ↦ (p, p) + x)
Module: Mathlib.Analysis.Calculus.FDeriv.Add

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
f g : E → F
x : E
hg : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 g x

Tactic:
by
  simp only [add_comm f, hg.add_iff_left]

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

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
f g : E → F
s : Set E
hg : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (f + g) s ↔ DifferentiableOn 𝕜 g s

Tactic:
by
  simp only [add_comm f, hg.add_iff_left]

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

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
f g : E → F
hg : Differentiable 𝕜 f
⊢ Differentiable 𝕜 (f + g) ↔ Differentiable 𝕜 g

Tactic:
by
  simp only [add_comm f, hg.add_iff_left]

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 ι
ι' : Type u_1
inst✝ : Fintype ι'
f : E [⋀^ι]→ₗ[𝕜] F [⋀^ι']→ₗ[𝕜] G
C : ℝ
H : ∀ (m₁ : ι → E) (m₂ : ι' → F), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
m : ι → E
⊢ ‖{ toFun := fun m ↦ (f m).mkContinuous (C * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯,
          map_eq_zero_of_eq' := ⋯ }
        m‖ ≤
    max C 0 * ∏ i, ‖m i‖

Tactic:
by
      simp only [coe_mk, MultilinearMap.coe_mk]
      refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
      rw [max_mul_of_nonneg, zero_mul]
      positivity

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
mem_iInf_of_directed

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.1 p.2 < ↑i}

case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun ε ↦ 𝓟 {p | dist p.1 p.2 < ↑ε}
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
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
this : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t =ᶠ[𝓝[s] x] fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 (n + 1) f t

Tactic:
refine this.mono fun y hy => ?_

Goal state after:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
this : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t =ᶠ[𝓝[s] x] fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t
y : E
hy : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t y = fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t y = iteratedFDerivWithin 𝕜 (n + 1) f t y
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
n : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
⊢ x ∈ s → iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x

Tactic:
hx

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 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
z : E
hz : z ∈ insert x s ∩ Metric.eball x r
⊢ ↑‖z - x‖₊ < r

Tactic:
simpa only [edist_eq_enorm_sub, Metric.mem_eball] using! hz.2

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y ↦ v y * u) s x = derivWithin v s x * u

pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y ↦ v y * u) s x = derivWithin v s x * u

Tactic:
· rw [derivWithin_mul_const hv u]

Goal state after:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
⊢ derivWithin (fun y ↦ v y * u) s x = derivWithin v s x * u
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
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
x : E
⊢ x ∈ s → AnalyticWithinAt 𝕜 (fderivWithin 𝕜 f s) s x

Tactic:
hx

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
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ AnalyticWithinAt 𝕜 (fderivWithin 𝕜 f s) s x
Module: Mathlib.Analysis.Calculus.Deriv.Add

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ deriv (fun x ↦ c + x) x = 1

Tactic:
deriv_const_add c,

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ deriv (fun x ↦ x) x = 1
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
⊢ slope (-f) = -slope f

Tactic:
ext x y

Goal state after:
k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
x y : k
⊢ slope (-f) x y = (-slope f) x y
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
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
x : E
⊢ f x = 0 x → (⇑e ∘ f) x = 0 x

Tactic:
hx

Goal state after:
𝕜 : 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
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
x : E
hx : f x = 0 x
⊢ (⇑e ∘ f) x = 0 x
Module: Mathlib.Analysis.Complex.ReImTopology

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

Tactic:
simpa only [interior_Ici] using! interior_preimage_re (Ici a)

Goal state after:
Module: Mathlib.Analysis.Complex.ReImTopology

Goal state before:
pp: a : ℝ
⊢ closure {z | a < z.im} = {z | a ≤ z.im}

Tactic:
by
  simpa only [closure_Ioi] using! closure_preimage_im (Ioi a)

Goal state after: