mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
g : α → F
inst✝ : ContinuousNeg E
f₁ f₂ : α → E
h : (f₁ - f₂) =O[𝕜; l] g
⊢ (f₂ - f₁) =O[𝕜; l] g

Tactic:
simpa using h.neg_left

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousAdd E
inst✝⁶ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T2Space F
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt f f₁' s x
⊢ EqOn (⇑f') (⇑f₁') (tangentConeAt 𝕜 s x)

Tactic:
intro y hy
  rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩
  exact tendsto_nhds_unique (hf.lim hd₀ hds hcd) (hg.lim hd₀ hds hcd)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun x ↦ G) G'
m : ι ⊕ ι' → G
⊢ f.currySum.uncurrySum m = f m

Tactic:
exact congr_arg f (Sum.elim_comp_inl_inr m)

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

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 →L[𝕜] F
x : E
m : ℕ
hm : 2 ≤ m
⊢ f.fpowerSeries x m = 0

Tactic:
match m with
    | 0 | 1 => linarith
    | n + 2 => simp [fpowerSeries]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
hjn : 0 < (Composition.ones n).blocksFun i
hj1 : 0 < 1
⊢ (v ∘ ⇑((Composition.ones n).embedding i)) ⟨0, hjn⟩ = v (Fin.castLE ⋯ i)

Tactic:
refine congr_arg v ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
i : Fin (Composition.ones n).length
hjn : 0 < (Composition.ones n).blocksFun i
hj1 : 0 < 1
⊢ ((Composition.ones n).embedding i) ⟨0, hjn⟩ = Fin.castLE ⋯ i
Module: Mathlib.Analysis.Analytic.Composition

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
x : E
n : ℕ
v : Fin n → E
i✝ : ℕ
him✝ : i✝ < (Composition.ones n).length
hin✝ : i✝ < n
⊢ (fun v i ↦ (id 𝕜 E x 1) fun x ↦ v (Fin.castLE ⋯ i)) v ⟨i✝, him✝⟩ = v ⟨i✝, hin✝⟩

Tactic:
refine congr_arg v ?_

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
x : E
n : ℕ
v : Fin n → E
i✝ : ℕ
him✝ : i✝ < (Composition.ones n).length
hin✝ : i✝ < n
⊢ Fin.castLE ⋯ ⟨i✝, him✝⟩ = ⟨i✝, hin✝⟩
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 ∞
⊢ ((if h : Fintype.card ι = Fintype.card ι then
        domDomCongr (Fintype.equivFinOfCardEq h) (f.compContinuousLinearMap ContinuousLinearMap.proj)
      else 0)
      fun x ↦ y) =
    f y

Tactic:
dif_pos rfl

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 ∞
⊢ ((domDomCongr (Fintype.equivFinOfCardEq ⋯) (f.compContinuousLinearMap ContinuousLinearMap.proj)) fun x ↦ y) = f y
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 ∞
⊢ ((if h : Fintype.card (Option ι) = Fintype.card (Option ι) then
        ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq h) f.continuousMultilinearMapOption
      else 0)
      fun x ↦ y) =
    (f y.1) y.2

Tactic:
dif_pos rfl

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 ∞
⊢ ((ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq ⋯) f.continuousMultilinearMapOption) fun x ↦ y) =
    (f y.1) y.2
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∞
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 → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
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 := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
hA : HasSum (fun n ↦ A (n + 2)) (f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2)
B : ℕ → ℝ := fun n ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((↑n + 2) * a ^ n)
n : ℕ
⊢ C * a ^ (n + 2) / ↑r' ^ (n + 2) * ↑r' ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) = B n

Tactic:
by
          simp [field, B, pow_succ]

Goal state after:
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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)

Tactic:
inter_comm

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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (insert x s ×ˢ insert x s ∩ Metric.eball (x, x) ↑r')
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
this✝ : Metric.ball ↑z ‖↑z⁻¹‖⁻¹ ∈ 𝓝 ↑z
y : A
hy : ‖y - ↑z‖ < ‖↑z⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ (↑(z.ofNearby y hy))⁻¹ʳ = (f1 ∘ f2 ∘ f3) ↑(z.ofNearby y hy)

Tactic:
simp only [Ring.inverse_unit, Function.comp_apply]

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 := fun a ↦ a * z.inv
f2 : A → A := fun b ↦ (1 - b)⁻¹ʳ
f3 : A → A := fun c ↦ 1 - z.inv * c
this✝ : Metric.ball ↑z ‖↑z⁻¹‖⁻¹ ∈ 𝓝 ↑z
y : A
hy : ‖y - ↑z‖ < ‖↑z⁻¹‖⁻¹
this : y = ↑(z.ofNearby y hy)
⊢ ↑(z.ofNearby y hy)⁻¹ = f1 (f2 (f3 ↑(z.ofNearby y hy)))
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case mpr
𝕜 : 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
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
⊢ g =ᶠ[𝓝 z] (f⁻¹ • f) • g

Tactic:
· filter_upwards [h₁f.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.2 h₂f)]
      intro y hy
      rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff] at hy
      simp [hy]

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
f' g' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hg : HasFDerivAtFilter g g' L
x✝ : E × E
⊢ f x✝.1 - f x✝.2 - f' (x✝.1 - x✝.2) + (g x✝.1 - g x✝.2 - g' (x✝.1 - x✝.2)) =
    (f + g) x✝.1 - (f + g) x✝.2 - (f' + g') (x✝.1 - x✝.2)

Tactic:
by
    grind [Pi.add_apply]

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
n : ℕ∞ω
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x ↦ p x m) (fun x ↦ q x m) s
x : E
hx : x ∈ s
⊢ (q x 0).curry0 = f x

Tactic:
by simp only [← hpq 0 zero_le hx, hp.zero_eq x hx]

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

Goal state before:
pp: case fderivWithin
𝕜 : 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
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
⊢ ↑m < ↑n → ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ (p x).shift m) ((p x).shift m.succ).curryLeft s x

Tactic:
(hm : (m : ℕ∞ω) < n)

Goal state after:
case fderivWithin
𝕜 : 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
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
hm : ↑m < ↑n
⊢ ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ (p x).shift m) ((p x).shift m.succ).curryLeft s x
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 : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn (ω + 1) f p s ↔
    (∀ x ∈ s, (p x 0).curry0 = f x) ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
        HasFTaylorSeriesUpToOn ω (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s

Tactic:
exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)

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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn (∞ + 1) f p s ↔
    (∀ x ∈ s, (p x 0).curry0 = f x) ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x) ∧
        HasFTaylorSeriesUpToOn ∞ (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s

Tactic:
exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (b + x)) (-b + a)

Tactic:
simp [differentiableAt_comp_add_left]

Goal state after:
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
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
⊢ HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (0 - 1) r

Tactic:
rw [zero_tsub]

Goal state after:
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
x : E
h : HasFiniteFPowerSeriesOnBall f p x 0 r
⊢ HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x 0 r
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

pp: case neg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)

Tactic:
· exact (hc.hasDerivWithinAt.clm_apply hu.hasDerivWithinAt).derivWithin hsx

Goal state after:
case neg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) = f b -ᵥ f a

Tactic:
smul_inv_smul₀ (sub_ne_zero.2 hne.symm)

Goal state after:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ f b -ᵥ f a = f b -ᵥ f a
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_12.hl.e_f.e_6.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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : ContinuousMultilinearMap 𝕜 E F
j : ι
⊢ Function.update fa.2 j 0 j = (Function.update (fun x ↦ fa) (some j) (g, 0) (some j)).2 j

Tactic:
simp [*]

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

Goal state before:
pp: case e'_12.hl.e_f.e_6.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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : ContinuousMultilinearMap 𝕜 E F
i j : ι
hij : j ≠ i
⊢ Function.update fa.2 i 0 j = (Function.update (fun x ↦ fa) (some i) (g, 0) (some j)).2 j

Tactic:
simp [*]

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

Goal state before:
pp: case hr.e_f.e_6.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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : (i : ι) → E i
j : ι
⊢ Function.update fa.2 j (g j) j = (Function.update (fun x ↦ fa) (some j) (0, g) (some j)).2 j

Tactic:
simp [*]

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

Goal state before:
pp: case hr.e_f.e_6.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 ι
inst✝ : DecidableEq ι
fa : ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)
f : ContinuousMultilinearMap 𝕜 (fun x ↦ ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)) F :=
  (ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F)).continuousMultilinearMapOption
Hf :
  HasStrictFDerivAt (fun x ↦ f fun x_1 ↦ x)
    ((f.linearDeriv fun x ↦ fa) ∘SL
      ContinuousLinearMap.pi fun x ↦ ContinuousLinearMap.id 𝕜 (ContinuousMultilinearMap 𝕜 E F × ((i : ι) → E i)))
    fa
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
g : (i : ι) → E i
i j : ι
hij : j ≠ i
⊢ Function.update fa.2 i (g i) j = (Function.update (fun x ↦ fa) (some i) (0, g) (some j)).2 j

Tactic:
simp [*]

Goal state after:
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
inst✝ : CompleteSpace F
f : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
u : Set E := ⋯
x : E
xu : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xU : x ∈ U
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
y : E
yu : y ∈ u
hxy : edist x y < r / 2
q : FormalMultilinearSeries 𝕜 E F := ⋯
A : ↑‖y - x‖₊ < r / 2
this : HasFPowerSeriesOnBall f (p.changeOrigin (y - x)) y (r - ↑‖y - x‖₊)
⊢ r / 2 + r / 2 = r

Tactic:
exact ENNReal.add_halves _

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
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') =ᶠ[L ⊓ 𝓟 {x}ᶜ] fun y ↦ slope f x y - f'

Tactic:
refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right
      rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']

Goal state after:
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 g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
⊢ EqOn f g U

Tactic:
have hfg' : f - g =ᶠ[𝓝 z₀] 0 := hfg.mono fun z h => by simp [h]

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 g : E → F
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfg : f =ᶠ[𝓝 z₀] g
hfg' : f - g =ᶠ[𝓝 z₀] 0
⊢ EqOn f g U