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

Goal state before:
pp: case 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 : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
⊢ (fun i ↦
      ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.sigmaCompositionAux
          { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } i).blocks) ≍
    fun i ↦ (d i).blocks

Tactic:
·

Goal state after:
case 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 : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
⊢ (fun i ↦
      ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.sigmaCompositionAux
          { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } i).blocks) ≍
    fun i ↦ (d i).blocks
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case 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 : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
i :
  Fin
    ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length
⊢ (ofFn fun j ↦ (d j).blocks)[↑i] = (d ⟨↑i, ⋯⟩).blocks

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
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
i :
  Fin
    ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length
⊢ 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'_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 : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
i :
  Fin
    ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length
⊢ (ofFn fun j ↦ (d j).blocks)[↑i] = (d ⟨↑i, ⋯⟩).blocks
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
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
i :
  Fin
    ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length
⊢ 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:
𝕜 : 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
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
i :
  Fin
    ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length
⊢ 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: case e'_6
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ (f ∘ ⇑u) (x + y✝) = f (u x + ↑u y✝)

pp: case convert_2
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ u x + ↑u y✝ ∈ insert (u x) s

pp: case convert_3
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ ↑u y✝ ∈ Metric.eball 0 r

Tactic:
·

Goal state after:
case e'_6
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ (f ∘ ⇑u) (x + y✝) = f (u x + ↑u y✝)
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case convert_2
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ u x + ↑u y✝ ∈ insert (u x) s

pp: case convert_3
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ ↑u y✝ ∈ Metric.eball 0 r

Tactic:
·

Goal state after:
case convert_2
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ u x + ↑u y✝ ∈ insert (u x) s
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case convert_3
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ ↑u y✝ ∈ Metric.eball 0 r

Tactic:
·

Goal state after:
case convert_3
𝕜 : 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
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
y✝ : E
hy1 : x + y✝ ∈ insert x (⇑u ⁻¹' s)
hy2 : y✝ ∈ Metric.eball 0 (r / ‖u‖ₑ)
⊢ ↑u y✝ ∈ Metric.eball 0 r
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case e'_3.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
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
⊢ ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length

Tactic:
·

Goal state after:
case e'_3.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
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
⊢ ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case r_le
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius

pp: case r_pos
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 0 < 1

pp: case hasSum
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ ∀ {y : A},
    y ∈ Metric.eball 0 1 → HasSum (fun n ↦ (formalMultilinearSeries_geometric 𝕜 A n) fun x ↦ y) (1 - (0 + y))⁻¹ʳ

Tactic:
·

Goal state after:
case r_le
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case r_pos
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 0 < 1

pp: case hasSum
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ ∀ {y : A},
    y ∈ Metric.eball 0 1 → HasSum (fun n ↦ (formalMultilinearSeries_geometric 𝕜 A n) fun x ↦ y) (1 - (0 + y))⁻¹ʳ

Tactic:
·

Goal state after:
case r_pos
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ 0 < 1
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case hasSum
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ ∀ {y : A},
    y ∈ Metric.eball 0 1 → HasSum (fun n ↦ (formalMultilinearSeries_geometric 𝕜 A n) fun x ↦ y) (1 - (0 + y))⁻¹ʳ

Tactic:
·

Goal state after:
case hasSum
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
⊢ ∀ {y : A},
    y ∈ Metric.eball 0 1 → HasSum (fun n ↦ (formalMultilinearSeries_geometric 𝕜 A n) fun x ↦ y) (1 - (0 + y))⁻¹ʳ
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
⊢ (fun x ↦ (1 + x)⁻¹ʳ) = (fun x ↦ (1 - x)⁻¹ʳ) ∘ ⇑(-ContinuousLinearMap.id 𝕜 A)

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)⁻¹ʳ) ∘ ⇑(-ContinuousLinearMap.id 𝕜 A))
    ((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
⊢ (fun x ↦ (1 + x)⁻¹ʳ) = (fun x ↦ (1 - x)⁻¹ʳ) ∘ ⇑(-ContinuousLinearMap.id 𝕜 A)
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case e'_12
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : HasSummableGeomSeries A
inst✝ : Nontrivial A
⊢ 1 = 1 / ‖-ContinuousLinearMap.id 𝕜 A‖ₑ

pp: case convert_16
𝕜 : 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) ((-ContinuousLinearMap.id 𝕜 A) 0) 1

Tactic:
·

Goal state after:
case e'_12
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : HasSummableGeomSeries A
inst✝ : Nontrivial A
⊢ 1 = 1 / ‖-ContinuousLinearMap.id 𝕜 A‖ₑ
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case convert_16
𝕜 : 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) ((-ContinuousLinearMap.id 𝕜 A) 0) 1

Tactic:
·

Goal state after:
case convert_16
𝕜 : 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) ((-ContinuousLinearMap.id 𝕜 A) 0) 1
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case inl
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Subsingleton A
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

pp: case inr
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Subsingleton A
⊢ AnalyticAt 𝕜 Ring.inverse ↑z
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case inr
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
hA : Nontrivial A
⊢ AnalyticAt 𝕜 Ring.inverse ↑z
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case hg
𝕜 : 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 𝕜 f2 (f3 ↑z)

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

Goal state after:
case hg
𝕜 : 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 𝕜 f2 (f3 ↑z)
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:
·

Goal state after:
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
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case pos
𝕜 : 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

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 pos
𝕜 : 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
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
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case pos
𝕜 : 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
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z

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
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z

Tactic:
·

Goal state after:
case pos
𝕜 : 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
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : 0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ n) z