mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹⁵ : CommRing 𝕜
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : AddCommGroup F
inst✝¹² : AddCommGroup G
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul 𝕜 E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
v : Fin 0 → E
v' : Fin 0 → F
c : Composition 0 := Composition.ones 0
⊢ {c} = Finset.univ

Tactic:
apply Finset.eq_of_subset_of_card_le <;> simp [Finset.card_univ, composition_card 0]

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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
⊢ (fun y ↦ f (x + y) - p.partialSum n y) =O[𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s] 0] fun y ↦ ‖y‖ ^ n

Tactic:
obtain ⟨a, -, C, -, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
      x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
    hf.uniform_geometric_approx' h

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
n : ℕ
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
r'0 : 0 < ↑r'
h : ↑r' < r
a C : ℝ
hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n
⊢ (fun y ↦ f (x + y) - p.partialSum n y) =O[𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s] 0] fun y ↦ ‖y‖ ^ n
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 ∞
⊢ ((f.toFormalMultilinearSeriesOfMultilinear (Fintype.card (Option ι))) fun x ↦ y) = (f y.1) y.2

Tactic:
rw [toFormalMultilinearSeriesOfMultilinear, 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.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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
n : ℕ
⊢ ‖q.comp p n‖₊ * r ^ n ≤ ∑' (c : Composition n), ‖q.compAlongComposition p c‖₊ * r ^ n

Tactic:
tsum_fintype,

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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
n : ℕ
⊢ ‖q.comp p n‖₊ * r ^ n ≤ ∑ b, ‖q.compAlongComposition p b‖₊ * r ^ n
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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
v : Fin (n + 2) → F
⊢ ∑ c ∈ {c | 1 < c.length}.toFinset,
      (p c.length) (applyComposition (fun k ↦ if k < n + 2 then p.rightInv i x k else 0) c v) =
    ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) ((p.rightInv i x).applyComposition c v)

Tactic:
have N : 0 < n + 2 := by simp
  refine sum_congr rfl fun c hc => p.congr rfl fun j hj1 hj2 => ?_
  have : ∀ k, c.blocksFun k < n + 2 := by
    simp only [Set.mem_toFinset (s := {c : Composition (n + 2) | 1 < c.length}),
      Set.mem_ofPred_eq] at hc
    simp [← Composition.ne_single_iff N, Composition.eq_single_iff_length, ne_of_gt hc]
  simp [applyComposition, this]

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

Goal state before:
pp: α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
blocks_fun' : Fin k → ℕ
H' : ⟨k, blocks_fun'⟩ ∈ compPartialSumSource m M N
heq : compChangeOfVariables m M N ⟨k, blocks_fun⟩ H = compChangeOfVariables m M N ⟨k, blocks_fun'⟩ H'
i : Fin k
⊢ (compChangeOfVariables m M N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨↑i, ⋯⟩ =
    (compChangeOfVariables m M N ⟨k, blocks_fun'⟩ H').snd.blocksFun ⟨↑i, ⋯⟩

Tactic:
by
        grind

Goal state after:
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
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
H :
  (∑ n ∈ Finset.range M, ∑ r ∈ Fintype.piFinset fun i ↦ Finset.Ico 1 N, (q n) fun i ↦ (p (r i)) fun _j ↦ z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j ↦ z
⊢ q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i) fun _j ↦ z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j ↦ z

Tactic:
simpa only [FormalMultilinearSeries.partialSum, ContinuousMultilinearMap.map_sum_finset] using H

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

Goal state before:
pp: case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
n : ℕ
one_le_n : 1 ≤ n
hn : S n ≤ (I + 1) * a
In : 2 ≤ n + 1
rSn : r * S n ≤ 1 / 2
⊢ S (n + 1) ≤ (I + 1) * a

Tactic:
calc
        S (n + 1) ≤ I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * S n) ^ k :=
          radius_rightInv_pos_of_radius_pos_aux2 In p i rpos.le apos.le Cpos.le ple
        _ = I * a + I * C * (((r * S n) ^ 2 - (r * S n) ^ (n + 1)) / (1 - r * S n)) := by
          rw [geom_sum_Ico' _ In]; exact ne_of_lt (rSn.trans_lt (by norm_num))
        _ ≤ I * a + I * C * ((r * S n) ^ 2 / (1 / 2)) := by
          gcongr
          · simp only [sub_le_self_iff]
            positivity
          · linarith only [rSn]
        _ = I * a + 2 * I * C * (r * S n) ^ 2 := by ring
        _ ≤ I * a + 2 * I * C * (r * ((I + 1) * a)) ^ 2 := by gcongr
        _ = (I + 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) * a := by ring
        _ ≤ (I + 1) * a := by gcongr

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

Goal state before:
pp: case mp.refine_1.refine_1
𝕜 : 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
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
ys : y ∈ insert x s
yb : ‖y - x‖ₑ < r
⊢ ‖y - x‖ₑ < p.radius

Tactic:
exact lt_of_lt_of_le yb h.r_le

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

Goal state before:
pp: n : ℕ
i j : (a : Composition n) × Composition a.length
⊢ i = j ↔ i.fst.blocks = j.fst.blocks ∧ i.snd.blocks = j.snd.blocks

Tactic:
refine ⟨by rintro rfl; exact ⟨rfl, rfl⟩, ?_⟩
  rcases i with ⟨a, b⟩
  rcases j with ⟨a', b'⟩
  rintro ⟨h, h'⟩
  obtain rfl : a = a' := by ext1; exact h
  obtain rfl : b = b' := by ext1; exact h'
  rfl

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
i : ι
⊢ (pi p).radius ≤ (p i).radius

Tactic:
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Goal state after:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
i : ι
r' : ℝ≥0
hr' : ↑r' < (pi p).radius
⊢ ↑r' ≤ (p i).radius
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
⊢ r ≤ (pi p).radius

Tactic:
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Goal state after:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
r' : ℝ≥0
hr' : ↑r' < r
⊢ ↑r' ≤ (pi p).radius
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ ⨅ i, (p i).radius ≤ (pi p).radius

Tactic:
apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Goal state after:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
r' : ℝ≥0
hr' : ↑r' < ⨅ i, (p i).radius
⊢ ↑r' ≤ (pi p).radius
Module: Mathlib.Analysis.Analytic.Constructions

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

Tactic:
convert! N.analyticAt_fun_prod h
  simp

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 : E → F
x : E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
⊢ DifferentiableWithinAt 𝕜 (c • f) Set.univ x ↔ DifferentiableAt 𝕜 f x

Tactic:
differentiableWithinAt_smul_iff,

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
x : E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
⊢ DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃L[𝕜] F
f : F → G
x : E
f' : E →L[𝕜] G
⊢ HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (f' ∘SL ↑iso.symm) (iso x)

Tactic:
by
  simp only [← hasFDerivWithinAt_univ, ← iso.comp_right_hasFDerivWithinAt_iff', preimage_univ]

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

Goal state before:
pp: case hbc
𝕜 : 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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ∏ i_1 ∈ {i}ᶜ, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤ ∏ x ∈ {i}ᶜ, ‖g‖ * ‖v x‖

Tactic:
gcongr with j hj

Goal state after:
case h1
𝕜 : 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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i j : ι
hj : j ∈ {i}ᶜ
⊢ ‖(Function.update (fun x ↦ g) i dg j) (v j)‖ ≤ ‖g‖ * ‖v j‖
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:
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.Analysis.Calculus.FDeriv.CompCLM

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
x : E
ι : Type u_5
M : ι → Type u_6
inst✝⁴ : (i : ι) → NormedAddCommGroup (M i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (M i)
H : Type u_7
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
inst✝ : Finite ι
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
m : E
⊢ (fderiv 𝕜 (fun y ↦ (c y) u) x) m = ((fderiv 𝕜 c x) m) u

Tactic:
by
  have := Fintype.ofFinite ι
  simp [fderiv_continuousMultilinear_apply_const hc]

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
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
⊢ AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s

Tactic:
by
  induction n with
  | zero =>
    rw [iteratedFDerivWithin_zero_eq_comp]
    exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E [×0]→L[𝕜] F)
      |>.comp_analyticOn h
  | succ n IH =>
    rw [iteratedFDerivWithin_succ_eq_comp_left]
    apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
    apply LinearIsometryEquiv.analyticOnNhd

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
⊢ AnalyticOnNhd 𝕜 (deriv^[n] f) s

Tactic:
induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
n : ℕ
⊢ AnalyticAt 𝕜 (deriv^[n] f) x

Tactic:
induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fun z ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries
    x n r

Tactic:
refine continuousMultilinearCurryFin1 𝕜 E F
      |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall ?_

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
⊢ HasFiniteFPowerSeriesOnBall (fun z ↦ p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) x n r
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 : 𝕜
⊢ DifferentiableAt 𝕜 (fun x ↦ f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.comp a differentiable_neg.differentiableAt⟩

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt 𝕜 (fun x ↦ f (-x)) a
⊢ DifferentiableAt 𝕜 f (-a)
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
h : CPolynomialOn 𝕜 f s
n : ℕ
⊢ CPolynomialOn 𝕜 (deriv^[n] f) s

Tactic:
induction n with
  | zero => exact h
  | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

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
n : ℕ
p : E [×n]→L[𝕜] F
h : (fun y ↦ p fun x ↦ y) =O[𝓝 0] fun y ↦ ‖y‖ ^ (n + 1)
y : E
c : ℝ
c_pos : c > 0
hc : IsBigOWith c (𝓝 0) (fun y ↦ p fun x ↦ y) fun y ↦ ‖y‖ ^ (n + 1)
t : Set E
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
z_mem : 0 ∈ t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
⊢ (p fun x ↦ y) = 0

Tactic:
clear h hc z_mem

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
n : ℕ
p : E [×n]→L[𝕜] F
y : E
c : ℝ
c_pos : c > 0
t : Set E
ht : ∀ y ∈ t, ‖p fun x ↦ y‖ ≤ c * ‖‖y‖ ^ (n + 1)‖
t_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
⊢ (p fun x ↦ y) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Finite ι
l : List ι
x : ι → 𝔸
⊢ HasStrictFDerivAt (fun x ↦ (List.map x l).prod)
    (∑ i, (List.map x (List.take (↑i) l)).prod •> (proj l[i] <• (List.map x (List.drop (↑i).succ l)).prod)) x

Tactic:
have := Fintype.ofFinite ι
  induction l with
  | nil => simp [hasStrictFDerivAt_const]
  | cons a l IH =>
    simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
    exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
      (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x ↦ x⁻¹) s x = toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)

Tactic:
rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs]

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
⊢ 0 = ↑m * 0 ^ (m - 1)

Tactic:
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 neg
𝕜 : 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
this : deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z = deriv (fun x ↦ (c * x) ^ (-1 - ↑k)) (z + d / c)
h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - ↑k)) = fun x ↦ (c * x + d) ^ (-1 - ↑k)
⊢ (-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:
deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)

Goal state after:
case neg
𝕜 : 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
this : deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z = c • deriv (fun x ↦ x ^ (-1 - ↑k)) (c * (z + d / c))
h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - ↑k)) = fun x ↦ (c * x + d) ^ (-1 - ↑k)
⊢ (-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))