mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ max ‖p n‖ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
]

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 : ℕ
⊢ max ‖p n‖ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
j : ℕ
IHj :
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j
hj : j + 1 < b.blocksFun ⟨i, hi⟩
A : j < b.blocksFun ⟨i, hi⟩
B : j < (a.sigmaCompositionAux b ⟨i, ⋯⟩).length
C : b.sizeUpTo i + j < b.sizeUpTo (i + 1)
D : b.sizeUpTo i + j < a.length
this : b.sizeUpTo i + j.succ = (b.sizeUpTo i + j).succ
⊢ (a.gather b).sizeUpTo i +
      ({ blocks := (a.blocks.splitWrtComposition b)[i], blocks_pos := ⋯, blocks_sum := ⋯ }.sizeUpTo j +
        a.blocks[b.sizeUpTo i + j]) =
    (a.gather b).sizeUpTo i +
      ({ blocks := (a.blocks.splitWrtComposition b)[i], blocks_pos := ⋯, blocks_sum := ⋯ }.sizeUpTo j +
        a.blocks[b.sizeUpTo i + j])

Tactic:
]

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

Goal state before:
pp: 𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ min r s ≤ min p.radius q.radius

Tactic:
]

Goal state after:
𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ min r s ≤ min p.radius q.radius
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
y : E
⊢ e + y ∈ insert e t → y ∈ Metric.eball 0 (min r s) → HasSum (fun n ↦ (p.prod q n) fun x ↦ y) (f (e + y), g (e + y))

Tactic:
h'y

Goal state after:
𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
y : E
h'y : e + y ∈ insert e t
⊢ y ∈ Metric.eball 0 (min r s) → HasSum (fun n ↦ (p.prod q n) fun x ↦ y) (f (e + y), g (e + y))
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p Set.univ e r
hg : HasFPowerSeriesWithinOnBall g q Set.univ e s
⊢ HasFPowerSeriesWithinOnBall (fun x ↦ (f x, g x)) (p.prod q) Set.univ e (min r s)

Tactic:
]

Goal state after:
𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p Set.univ e r
hg : HasFPowerSeriesWithinOnBall g q Set.univ e s
⊢ HasFPowerSeriesWithinOnBall (fun x ↦ (f x, g x)) (p.prod q) Set.univ e (min r s)
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : 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 : ℕ
a : Composition n
b : Composition a.length
⊢ ((fun i ↦
              ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
                { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
            ((fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩) ⟨a, b⟩)).fst.blocks =
      ⟨a, b⟩.fst.blocks ∧
    ((fun i ↦
              ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
                { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
            ((fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩) ⟨a, b⟩)).snd.blocks =
      ⟨a, b⟩.snd.blocks

Tactic:
]

Goal state after:
𝕜 : 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 : ℕ
a : Composition n
b : Composition a.length
⊢ ((fun i ↦
              ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
                { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
            ((fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩) ⟨a, b⟩)).fst.blocks =
      ⟨a, b⟩.fst.blocks ∧
    ((fun i ↦
              ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
                { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
            ((fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩) ⟨a, b⟩)).snd.blocks =
      ⟨a, b⟩.snd.blocks
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case hbc
𝕜 : 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
C : ℝ
hC : ∀ (n : ℕ), ‖pi p n‖ * ↑r' ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ ≤ ‖fun i ↦ p i n‖

Tactic:
]

Goal state after:
case hbc
𝕜 : 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
C : ℝ
hC : ∀ (n : ℕ), ‖pi p n‖ * ↑r' ^ n ≤ C
n : ℕ
⊢ ‖p i n‖ ≤ ‖fun i ↦ p i n‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case right.e_3
𝕜 : 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 : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
i : Fin (a.gather b).length
⊢ b.blocks[↑i] = b.blocks[↑⟨↑i, ⋯⟩]

Tactic:
]

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
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
⊢ (ofFn fun i ↦
      (((fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩)
              ((fun i ↦
                  ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
                    { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
                ⟨c, d⟩)).snd
          i).blocks) =
    ofFn fun i ↦ (⟨c, d⟩.snd i).blocks

Tactic:
]

Goal state after:
𝕜 : 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
⊢ (ofFn fun i ↦
      (((fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩)
              ((fun i ↦
                  ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
                    { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
                ⟨c, d⟩)).snd
          i).blocks) =
    ofFn fun i ↦ (⟨c, d⟩.snd i).blocks
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case inr
𝕜 : 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
C : ι → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * ↑r' ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < ↑r' ^ n
⊢ ∀ (i : ι), ‖p i n‖ ≤ D / ↑r' ^ n

Tactic:
]

Goal state after:
case inr
𝕜 : 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
C : ι → ℝ
C_pos : ∀ (i : ι), C i > 0
hC : ∀ (i : ι) (n : ℕ), ‖p i n‖ * ↑r' ^ n ≤ C i
D : ℝ
D_nonneg : D ≥ 0
hD : ∀ (i : ι), C i ≤ D
n : ℕ
hr' : 0 < ↑r' ^ n
⊢ ∀ (i : ι), ‖p i n‖ ≤ D / ↑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) = c.blocks

pp: 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

Tactic:
]

Goal state after:
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) = c.blocks

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_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticWithinAt 𝕜 f Set.univ z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (f ^ n) Set.univ z

Tactic:
]

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticWithinAt 𝕜 f Set.univ z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (f ^ n) Set.univ z
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : 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
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf Set.univ (u x) r
⊢ HasFPowerSeriesWithinOnBall (f ∘ ⇑u) (pf.compContinuousLinearMap u) Set.univ x (r / ‖u‖ₑ)

Tactic:
]

Goal state after:
𝕜 : 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
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf Set.univ (u x) r
⊢ HasFPowerSeriesWithinOnBall (f ∘ ⇑u) (pf.compContinuousLinearMap u) Set.univ x (r / ‖u‖ₑ)
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : 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
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c ↦ (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c ↦ (r c.fst.length) fun i ↦ (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
⊢ ∑ c, f c = ∑ i, g ((sigmaEquivSigmaPi n) i)

Tactic:
]

Goal state after:
𝕜 : 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
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c ↦ (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c ↦ (r c.fst.length) fun i ↦ (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
⊢ ∑ c, f c = ∑ i, g ((sigmaEquivSigmaPi n) i)
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E)) (FormalMultilinearSeries.id 𝕜 E a) a

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E)) (FormalMultilinearSeries.id 𝕜 E a) a
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
inst✝ : Nontrivial A
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 + x)⁻¹ʳ)
    ((formalMultilinearSeries_geometric 𝕜 A).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 A)) 0 1

Tactic:
]

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : HasSummableGeomSeries A
inst✝ : Nontrivial A
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 + x)⁻¹ʳ)
    ((formalMultilinearSeries_geometric 𝕜 A).compContinuousLinearMap (-ContinuousLinearMap.id 𝕜 A)) 0 1
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:
]

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: 𝕜 : 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)
⊢ (↑(Units.oneSub (1 - ↑z⁻¹ * y) ⋯))⁻¹ʳ = (↑z⁻¹ * y)⁻¹ʳ

Tactic:
]

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)
⊢ (↑(Units.oneSub (1 - ↑z⁻¹ * y) ⋯))⁻¹ʳ = (↑z⁻¹ * y)⁻¹ʳ
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)

Tactic:
have A : HasFPowerSeriesAt (f.symm ∘ f) ((p.leftInv i a).comp p) a := by
    have : HasFPowerSeriesAt (ContinuousLinearMap.id 𝕜 E) ((p.leftInv i a).comp p) a := by
      rw [leftInv_comp _ _ _ hp]
      exact (ContinuousLinearMap.id 𝕜 E).hasFPowerSeriesAt a
    apply this.congr
    filter_upwards [f.open_source.mem_nhds h0] with x hx using by simp [hx]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
⊢ HasFPowerSeriesAt (↑f.symm) (p.leftInv i a) (↑f a)
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case hf
𝕜 : 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 := ⋯
f2 : A → A := ⋯
f3 : A → A := ⋯
feq : ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
⊢ AnalyticAt 𝕜 f3 ↑z

Tactic:
· exact analyticAt_const.sub (analyticAt_const.mul analyticAt_id)

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

Goal state before:
pp: case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ (- -n)) s z

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
s : Set E
n : ℤ
h₁f : AnalyticWithinAt 𝕜 f s z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticWithinAt 𝕜 (f ^ (- -n)) s z