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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c c' : ℕ → 𝕜
⊢ ofScalars E (c - c') = ofScalars E c - ofScalars E c'

Tactic:
by
  ext; simp [ofScalars, sub_smul]

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

Tactic:
apply (hf (x - y) (by convert hx; abel)).comp_sub

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

Tactic:
apply (hf (x - y) (by convert hx; abel)).comp_sub

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

Goal state before:
pp: case hs
𝕜 : 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
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
⊢ (Sigma.fst ⁻¹' ⋃ i, {↑i}).Finite

Tactic:
preimage_iUnion,

Goal state after:
case hs
𝕜 : 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
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
⊢ (⋃ i, Sigma.fst ⁻¹' {↑i}).Finite
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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
⊢ ∃ k, ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4

Tactic:
have : Tendsto (fun k ↦ ∑' n, ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0) := by
      apply _root_.tendsto_sum_nat_add (f := fun n ↦ ‖p n‖ * ↑r' ^ n)
    exact ((tendsto_order.1 this).2 _ (by linarith)).exists

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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
I : ∀ (w : E), ‖w‖₊ < r' → ‖∑ i ∈ Finset.Ico k n, (p i) fun x ↦ w‖ ≤ ε / 4
⊢ ‖p.partialSum n z - p.partialSum n y‖ < ε

Tactic:
calc
  ‖p.partialSum n z - p.partialSum n y‖
  _ = ‖∑ i ∈ range n, p i (fun _ ↦ z) - ∑ i ∈ range n, p i (fun _ ↦ y)‖ := rfl
  _ = ‖(∑ i ∈ range k, p i (fun _ ↦ z) + ∑ i ∈ Ico k n, p i (fun _ ↦ z))
        - (∑ i ∈ range k, p i (fun _ ↦ y) + ∑ i ∈ Ico k n, p i (fun _ ↦ y))‖ := by
    simp [sum_range_add_sum_Ico _ hkn]
  _ = ‖(p.partialSum k z - p.partialSum k y) + (∑ i ∈ Ico k n, p i (fun _ ↦ z))
        + (- ∑ i ∈ Ico k n, p i (fun _ ↦ y))‖ := by
    congr 1
    simp only [FormalMultilinearSeries.partialSum]
    abel
  _ ≤ ‖p.partialSum k z - p.partialSum k y‖ + ‖∑ i ∈ Ico k n, p i (fun _ ↦ z)‖
      + ‖- ∑ i ∈ Ico k n, p i (fun _ ↦ y)‖ := norm_add₃_le
  _ ≤ ε / 4 + ε / 4 + ε / 4 := by
    gcongr
    · exact I _ h'z
    · simp only [norm_neg]; exact I _ yr'
  _ < ε := by linarith

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
q : FormalMultilinearSeries 𝕜 E F
p : FormalMultilinearSeries 𝕜 E E
⊢ q.comp p 0 = q 0

Tactic:
ext 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
q : FormalMultilinearSeries 𝕜 E F
p : FormalMultilinearSeries 𝕜 E E
v : Fin 0 → E
⊢ (q.comp p 0) v = (q 0) v
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
n : ℕ
hn : 0 < n
⊢ q.removeZero.comp p n = q.comp p n

Tactic:
ext v

Goal state after:
𝕜 : 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
n : ℕ
hn : 0 < n
v : Fin n → E
⊢ (q.removeZero.comp p n) v = (q.comp p n) v
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 : ℕ
⊢ p.compAlongComposition (id 𝕜 E x) (Composition.ones n) = p n

Tactic:
ext 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
⊢ (p.compAlongComposition (id 𝕜 E x) (Composition.ones n)) v = (p n) v
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case h₀
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
⊢ p.compAlongComposition (id 𝕜 E x) b = 0

Tactic:
ext v

Goal state after:
case h₀
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
A : 1 < b.blocksFun j
v : Fin n → E
⊢ (p.compAlongComposition (id 𝕜 E x) b) v = 0 v
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
x : (i : ι) → Em i
⊢ x ∈ Metric.eball 0 ∞

Tactic:
simp only [Metric.eball_top, Set.mem_univ]

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
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
⊢ (id 𝕜 F ((p 0) v0)).comp p 0 = p 0

Tactic:
ext v

Goal state after:
case inl
𝕜 : 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
v0 v : Fin 0 → E
⊢ ((id 𝕜 F ((p 0) v0)).comp p 0) v = (p 0) v
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case inr
𝕜 : 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ (id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos) = p n

Tactic:
ext v

Goal state after:
case inr
𝕜 : 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
v : Fin n → E
⊢ ((id 𝕜 F ((p 0) v0)).compAlongComposition p (Composition.single n n_pos)) v = (p n) v
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case inr.h₀
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
⊢ (id 𝕜 F ((p 0) v0)).compAlongComposition p b = 0

Tactic:
ext v

Goal state after:
case inr.h₀
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.single n n_pos
A : 1 < b.length
v : Fin n → E
⊢ ((id 𝕜 F ((p 0) v0)).compAlongComposition p b) v = 0 v
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case inr
𝕜 : 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
v0 : Fin 0 → E
n : ℕ
n_pos : n > 0
⊢ (id 𝕜 F ((p 0) v0)).comp p n = p n

Tactic:
dsimp [FormalMultilinearSeries.comp]
    rw [Finset.sum_eq_single (Composition.single n n_pos)]
    · show compAlongComposition (id 𝕜 F (p 0 v0)) p (Composition.single n n_pos) = p n
      ext v
      rw [compAlongComposition_apply, id_apply_one' _ _ _ (Composition.single_length n_pos)]
      dsimp [applyComposition]
      refine p.congr rfl fun i him hin => congr_arg v <| ?_
      ext; simp
    · change
      ∀ b : Composition n, b ∈ Finset.univ → b ≠ Composition.single n n_pos →
        compAlongComposition (id 𝕜 F (p 0 v0)) p b = 0
      intro b _ hb
      have A : 1 < b.length := by
        have : b.length ≠ 1 := by simpa [Composition.eq_single_iff_length] using hb
        have : 0 < b.length := Composition.length_pos_of_pos b n_pos
        lia
      ext v
      rw [compAlongComposition_apply, id_apply_of_one_lt _ _ _ A, _root_.zero_apply,
        _root_.zero_apply]
    · simp

Goal state after:
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
x : G × ((i : ι) → Em i)
⊢ x ∈ Metric.eball 0 ∞

Tactic:
simp only [Metric.eball_top, Set.mem_univ]

Goal state after:
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✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : Composition (n + 2)
hc : c.length < n + 2
cuniv : ⟨c, hc⟩ ∈ univ
⊢ ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
      (p.removeZero.leftInv i x (↑⟨c, hc⟩).length) =
    ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
      (p.leftInv i x (↑⟨c, hc⟩).length)

Tactic:
ext v

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
IH : ∀ m < n + 2, p.removeZero.leftInv i x m = p.leftInv i x m
c : Composition (n + 2)
hc : c.length < n + 2
cuniv : ⟨c, hc⟩ ∈ univ
v : Fin (n + 2) → F
⊢ (ContinuousMultilinearMap.compAlongComposition (p.removeZero.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
        (p.removeZero.leftInv i x (↑⟨c, hc⟩).length))
      v =
    (ContinuousMultilinearMap.compAlongComposition (p.compContinuousLinearMap ↑i.symm) (↑⟨c, hc⟩)
        (p.leftInv i x (↑⟨c, hc⟩).length))
      v
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case e_f
𝕜 : 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✝ n : ℕ
hn : 2 ≤ n + 2
⊢ p.comp (fun k ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2) =
    ∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c

Tactic:
ext v

Goal state after:
case e_f
𝕜 : 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✝ n : ℕ
hn : 2 ≤ n + 2
v : Fin (n + 2) → F
⊢ (p.comp (fun k ↦ if k < n + 2 then p.rightInv i x k else 0) (n + 2)) v =
    (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c) v
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case e'_6
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
⊢ f = (fun y ↦ f (x + y)) ∘ fun y ↦ y - x

pp: case e'_8
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
⊢ insert x s ∩ Metric.ball x ↑r' = (fun y ↦ y - x) ⁻¹' ((fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')

Tactic:
· simp [Function.comp_def]

Goal state after:
case e'_8
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
⊢ insert x s ∩ Metric.ball x ↑r' = (fun y ↦ y - x) ⁻¹' ((fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 ↑r')
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
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
⊢ r * ((I + 1) * a) ≤ 1 / 2

Tactic:
← mul_assoc

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
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
⊢ r * (I + 1) * a ≤ 1 / 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
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
⊢ q.compAlongComposition p c = 0

Tactic:
ext v

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
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
⊢ (q.compAlongComposition p c) v = 0 v
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x | (fun x ↦ f x = g x) x}
g' : E → F := u.piecewise g f
y : E
hy : y ∈ u
⊢ g y = g' y

Tactic:
simp [g', hy]

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
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:
by
  convert! N.analyticAt_fun_prod h
  simp

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
R : Type u_4
inst✝³ : DivisionSemiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
s : Set 𝕜
f : 𝕜 → F
x : 𝕜
c : R
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x

Tactic:
· simp [fderivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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
f' : E →L[𝕜] F
L : Filter (E × E)
c : F
⊢ HasFDerivAtFilter (fun x ↦ f x + c) f' L ↔ HasFDerivAtFilter f f' L

Tactic:
simp [hasFDerivAtFilter_iff_isLittleOTVS]

Goal state after:
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
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm
⊢ HasFDerivWithinAt f f' s (iso x)

Tactic:
rw [A, B]

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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H : HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm
B : f' = (f' ∘SL ↑iso) ∘SL ↑iso.symm
⊢ HasFDerivWithinAt ((f ∘ ⇑iso) ∘ ⇑iso.symm) ((f' ∘SL ↑iso) ∘SL ↑iso.symm) s (iso x)
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x ↦ M) N
⊢ (alternatization f).toAlternatingMap = MultilinearMap.alternatization f.toMultilinearMap

Tactic:
ext v

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : ContinuousMultilinearMap R (fun x ↦ M) N
v : ι → M
⊢ (alternatization f).toAlternatingMap v = (MultilinearMap.alternatization f.toMultilinearMap) v