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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
hc' : ‖‖c n‖‖ * ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
norm_norm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
hc' : ‖c n‖ * ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖
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 t : Set E
x : E
h : HasFPowerSeriesWithinAt f p s x
hst : s ∈ 𝓝[t] x
⊢ HasFPowerSeriesWithinAt f p t x

Tactic:
by
  rcases h with ⟨r, hr⟩
  rcases EMetric.mem_nhdsWithin_iff.1 hst with ⟨r', r'_pos, hr'⟩
  refine ⟨min r r', ?_⟩
  have Z := hr.of_le (by simp [r'_pos, hr.r_pos]) (min_le_left r r')
  refine ⟨Z.r_le, Z.r_pos, fun {y} hy h'y ↦ ?_⟩
  apply Z.hasSum ?_ h'y
  simp only [mem_insert_iff, add_eq_left] at hy
  rcases hy with rfl | hy
  · simp
  apply mem_insert_of_mem _ (hr' ?_)
  simp only [Metric.mem_eball, edist_eq_enorm_sub, sub_zero, lt_min_iff, mem_inter_iff,
    add_sub_cancel_left, hy, and_true] at h'y ⊢
  exact h'y.2

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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := ⇑(c.embedding (c.index j))
j' : Fin (c.blocksFun (c.index j)) := c.invEmbedding j
C : Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z
⊢ Function.update v j z ∘ r = Function.update (v ∘ r) j' z

Tactic:
convert! C

Goal state after:
case e'_5
𝕜 : 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 : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
r : Fin (c.blocksFun (c.index j)) → Fin n := ⇑(c.embedding (c.index j))
j' : Fin (c.blocksFun (c.index j)) := c.invEmbedding j
C : Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z
⊢ j = r j'
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
⊢ (id 𝕜 E x).applyComposition (Composition.ones n) v ⟨i✝, him✝⟩ = v ⟨i✝, hin✝⟩

Tactic:
rw [applyComposition_ones]

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
⊢ (fun v i ↦ (id 𝕜 E x 1) fun x ↦ v (Fin.castLE ⋯ i)) v ⟨i✝, him✝⟩ = v ⟨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 ∞
⊢ (∑ i ∈ Finset.range (Fintype.card ι + 1), (f.toFormalMultilinearSeries i) fun x ↦ y) = f (0 + y)

Tactic:
rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
    · rw [toFormalMultilinearSeries, dif_pos rfl]; rfl
    · intro m _ ne; rw [toFormalMultilinearSeries, dif_neg ne.symm]; rfl

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
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 : ℕ
⊢ ‖p (n + 2)‖ * ‖y - (x, x)‖ ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) ≤
    C * a ^ (n + 2) / ↑r' ^ (n + 2) * ↑r' ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖)

Tactic:
by
          have : 0 < a := ha.1
          gcongr
          · apply hp
          · apply hy'.le

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

Goal state before:
pp: case neg
𝕜 : 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
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
c : Composition n
x✝ : c ∈ univ
h : ¬1 < c.length
⊢ c ∈ {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}

Tactic:
have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
      rw [← Composition.eq_single_iff_length hn] at this
      simp [this]

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

Goal state before:
pp: case inl
𝕜 : 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : Fin i → E
hc : m ≤ c.length
⊢ (q c.length) (p.applyComposition c v) = 0

pp: case inr
𝕜 : 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : Fin i → E
hc : c.length < m
⊢ (q c.length) (p.applyComposition c v) = 0

Tactic:
· simp [hg.finite _ hc]

Goal state after:
case inr
𝕜 : 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
hi : m * n ≤ i
c : Composition i
v : Fin i → E
hc : c.length < m
⊢ (q c.length) (p.applyComposition c v) = 0
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a.left
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
n : ℕ
⊢ ‖‖p n‖‖ * ‖↑r ^ n‖ ≤ ‖‖p.prod q n‖ * ↑r ^ n‖

Tactic:
norm_norm,

Goal state after:
case a.left
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
n : ℕ
⊢ ‖p n‖ * ‖↑r ^ n‖ ≤ ‖‖p.prod q n‖ * ↑r ^ n‖
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a.right
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
n : ℕ
⊢ ‖‖q n‖‖ * ‖↑r ^ n‖ ≤ ‖‖p.prod q n‖ * ↑r ^ n‖

Tactic:
norm_norm,

Goal state after:
case a.right
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
n : ℕ
⊢ ‖q n‖ * ‖↑r ^ n‖ ≤ ‖‖p.prod q n‖ * ↑r ^ n‖
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasFDerivAt f^[n] (f' ^ n) x

Tactic:
refine HasFDerivAtFilter.iterate hf ?_ n
  simpa [hx] using hf.continuousAt.tendsto.prodMap (tendsto_pure_pure f x)

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

Goal state before:
pp: case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ ‖‖p.prod q n‖‖ * ‖↑r ^ n‖ ≤ ‖‖p n‖ * ↑r ^ n + ‖q n‖ * ↑r ^ n‖

Tactic:
norm_norm,

Goal state after:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ ‖p.prod q n‖ * ‖↑r ^ n‖ ≤ ‖‖p n‖ * ↑r ^ n + ‖q n‖ * ↑r ^ n‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case e'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
⊢ List.map sum
      ((ofFn fun j ↦ (d j).blocks).flatten.splitWrtComposition
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }) =
    c.blocks

Tactic:
rwa [splitWrtComposition_flatten]

Goal state after:
case e'_2.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
⊢ List.map List.length (ofFn fun j ↦ (d j).blocks) =
    { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }.blocks
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: α : Type u_1
𝕜 : 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 → F
c : E
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (∑ n ∈ N, f n) s c

Tactic:
by
  classical
  induction N using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty]
    exact analyticWithinAt_const
  | insert a B aB hB =>
    simp_rw [Finset.sum_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).add (hB fun b m ↦ h b (Or.inr m))

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

Goal state before:
pp: case insert
α : 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
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : (∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ B, f n z) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ insert a B, f n z) s c

Tactic:
Finset.prod_insert aB

Goal state after:
case insert
α : 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
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : (∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ B, f n z) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f a z * ∏ n ∈ B, f n z) s c
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
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✝ : Finite ι
val✝ : Fintype ι
⊢ Continuous compContinuousLinearMapCLM

Tactic:
refine UniformConvergenceCLM.isUniformInducing_postcomp (.id 𝕜)
    (toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] G) →L[𝕜] _)
    isUniformEmbedding_toContinuousMultilinearMap.isUniformInducing _ |>.isInducing
    |>.continuous_iff |>.mpr ?_

Goal state after:
𝕜 : Type u
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✝ : Finite ι
val✝ : Fintype ι
⊢ Continuous ((toContinuousMultilinearMapCLM 𝕜).comp ∘ compContinuousLinearMapCLM)
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
by_cases hxu : x ∈ tsupport u
  · by_cases hxv : x ∈ tsupport v
    · simpa using (B.hasFDerivAt_of_bilinear (hu hxv).hasFDerivAt (hv hxu).hasFDerivAt).hasDerivAt
    · have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
        mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxv
      convert! HasDerivAt.of_notMem_tsupport hx
      simp [(hv hxu).unique <| .of_notMem_tsupport hxv, image_eq_zero_of_notMem_tsupport hxv]
  · have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
      mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxu
    convert! HasDerivAt.of_notMem_tsupport hx
    by_cases hxv : x ∈ tsupport v
    · simp [image_eq_zero_of_notMem_tsupport hxu, (hu hxv).unique <| .of_notMem_tsupport hxu]
    · simp [image_eq_zero_of_notMem_tsupport hxu, image_eq_zero_of_notMem_tsupport hxv]

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

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedCommRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasStrictDerivAt f f' x
n : ℕ
⊢ HasStrictDerivAt (fun x ↦ f x ^ n) (↑n * f x ^ (n - 1) * f') x

Tactic:
by
  simpa using h.hasStrictFDerivAt.pow n |>.hasStrictDerivAt

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

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

Tactic:
convert! ContinuousLinearMap.comp_cpolynomialOn ?g IH.fderiv

Goal state after:
case e'_9
𝕜 : 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 : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm = ⇑?g✝

case g
𝕜 : 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 : CPolynomialOn 𝕜 f s
n : ℕ
IH : CPolynomialOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] E [×n]→L[𝕜] F) →L[𝕜] E [×n + 1]→L[𝕜] F
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:
by
  ext x y; exact slope_neg f x y

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 : 𝕜
⊢ HasDerivAt f f' x ↔ Tendsto (fun t ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')

Tactic:
have : 𝓝[≠] x = Filter.map (fun t ↦ x + t) (𝓝[≠] 0) := by simp

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
this : 𝓝[≠] x = map (fun t ↦ x + t) (𝓝[≠] 0)
⊢ HasDerivAt f f' x ↔ Tendsto (fun t ↦ t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: case refine_2.h
𝕜 : 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))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ ContinuousWithinAt f (s ∩ t) x

pp: case refine_2.hx
𝕜 : 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))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)

Tactic:
· apply H'.continuousWithinAt.mono inter_subset_left

Goal state after:
case refine_2.hx
𝕜 : 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))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t y
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
rw [hy] at hh; exact hh.comp_hasFDerivWithinAt x hf hst

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

Goal state before:
pp: case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ deriv (fun x ↦ x ^ m) x = ↑m * x ^ (m - 1)

Tactic:
· rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_zpow.1 H)]
    push Not at H
    rcases H with ⟨rfl, hm⟩
    rw [zero_zpow _ ((sub_one_lt _).trans hm).ne, mul_zero]

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

Goal state before:
pp: case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

Tactic:
Int.ofNat_sub hkn

Goal state after:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k)