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

Goal state before:
pp: case refine_2
𝕜 : 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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ ∀ {y : E}, y ∈ Metric.eball 0 r → HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))

Tactic:
intro y hy

Goal state after:
case refine_2
𝕜 : 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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (f (x + y))
Module: Mathlib.Analysis.Analytic.CPolynomialDef

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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
⊢ ∀ y ∈ Metric.eball x r, f y = f x

Tactic:
intro y hy

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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ f y = f x
Module: Mathlib.Analysis.Analytic.CPolynomialDef

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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
⊢ (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)

Tactic:
ext x
  rw [partialSum, FormalMultilinearSeries.sum,
    tsum_eq_sum (f := fun m => p.changeOriginSeries k m (fun _ => x)) (s := Finset.range (n - k))]
  intro m hm
  rw [Finset.mem_range, not_lt] at hm
  rw [p.changeOriginSeries_finite_of_finite hn k (by rw [add_comm]; exact Nat.le_add_of_sub_le hm),
    _root_.zero_apply]

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

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
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : ↑‖y‖₊ + ‖z‖ₑ < r
⊢ f (x + y + z) = (p.changeOrigin y).sum z

Tactic:
p.changeOrigin_eval_of_finite hf.finite,

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
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : ↑‖y‖₊ + ‖z‖ₑ < r
⊢ f (x + y + z) = p.sum (y + z)
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x ≤ x_1), c x_1 = 0
ti : ℕ
hti : ∀ (b : ℕ), ti ≤ b → ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : ti ≤ zi
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a : ofScalars E c n = 0
a✝ : Nontrivial E
⊢ ofScalars E c (n + 1) = 0

Tactic:
simp only [ofScalars_eq_zero] at a ⊢

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x ≤ x_1), c x_1 = 0
ti : ℕ
hti : ∀ (b : ℕ), ti ≤ b → ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞
zi : ℕ
hzi : ti ≤ zi
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a✝ : Nontrivial E
a : c n = 0
⊢ c (n + 1) = 0
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
⊢ ‖(∑ i ∈ Finset.range n, (p i) fun x ↦ z) - ∑ i ∈ Finset.range n, (p i) fun x ↦ y‖ =
    ‖((∑ i ∈ Finset.range k, (p i) fun x ↦ z) + ∑ i ∈ Finset.Ico k n, (p i) fun x ↦ z) -
        ((∑ i ∈ Finset.range k, (p i) fun x ↦ y) + ∑ i ∈ Finset.Ico k n, (p i) fun x ↦ y)‖

Tactic:
simp [sum_range_add_sum_Ico _ hkn]

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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ a * I +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          ‖(↑i.symm).compContinuousMultilinearMap
              (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c)‖ ≤
    a * ‖↑i.symm‖ +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k * (I * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖)

Tactic:
by
      gcongr with j
      apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans
      gcongr
      apply (norm_sum_le _ _).trans
      gcongr
      apply (compAlongComposition_norm _ _ _).trans
      gcongr
      apply hp

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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
⊢ HasSum (fun n ↦ (q.comp p n) fun x ↦ y) ((g ∘ f) (x + y))

Tactic:
have C :
    Tendsto
      (fun n => ∑ i ∈ compPartialSumTarget 0 n n, q.compAlongComposition p i.2 fun _j => y)
      atTop (𝓝 (g (f (x + y)))) := by
    simpa [comp_partialSum] using! B

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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
⊢ HasSum (fun n ↦ (q.comp p n) fun x ↦ y) ((g ∘ f) (x + y))
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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
D : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (g (f (x + y)))
⊢ HasSum (fun n ↦ (q.comp p n) fun x ↦ y) ((g ∘ f) (x + y))

Tactic:
have E : HasSum (fun n => (q.comp p) n fun _j => y) (g (f (x + y))) := by
    apply D.sigma
    intro n
    simp only [compAlongComposition_apply, FormalMultilinearSeries.comp, sum_apply]
    exact hasSum_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
g : F → G
f : E✝ → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E✝ F
x : E✝
t : Set F
s : Set E✝
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
δ : ℝ≥0∞
δpos : 0 < δ
hδ : ∀ {z : E✝}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
rf' : ℝ≥0∞ := min rf δ
min_pos : 0 < min rf' ↑r
y : E✝
h'y : x + y ∈ insert x s
hy : y ∈ Metric.eball 0 (min rf' ↑r)
y_mem : y ∈ Metric.eball 0 rf
fy_mem : f (x + y) ∈ insert (f x) t ∩ Metric.eball (f x) rg
A : Tendsto (fun n ↦ (n, ∑ a ∈ Finset.Ico 1 n, (p a) fun x ↦ y)) atTop (atTop ×ˢ 𝓝 (f (x + y) - f x))
B : Tendsto (fun n ↦ q.partialSum n (∑ a ∈ Finset.Ico 1 n, (p a) fun _b ↦ y)) atTop (𝓝 (g (f (x + y))))
C :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n n, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (g (f (x + y))))
D : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (g (f (x + y)))
E : HasSum (fun n ↦ (q.comp p n) fun _j ↦ y) (g (f (x + y)))
⊢ HasSum (fun n ↦ (q.comp p n) fun x ↦ y) ((g ∘ f) (x + y))
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case refine_1.refine_2
𝕜 : 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
⊢ EqOn f g' (insert x s)

Tactic:
intro y hy

Goal state after:
case refine_1.refine_2
𝕜 : 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 ∈ insert x s
⊢ f y = g' y
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:
by rintro rfl; exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case refine_2
𝕜 : 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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
⊢ AnalyticOn 𝕜 f u

Tactic:
intro y hy

Goal state after:
case refine_2
𝕜 : 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
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
⊢ AnalyticWithinAt 𝕜 f u y
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.prod q).radius
⊢ ↑r ≤ min p.radius q.radius

Tactic:
le_min_iff

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.prod q).radius
⊢ ↑r ≤ p.radius ∧ ↑r ≤ q.radius
Module: Mathlib.Analysis.Analytic.Constructions

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

Tactic:
apply FormalMultilinearSeries.le_radius_of_isBigO
      refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
      rw [norm_mul, norm_norm, norm_mul, norm_norm]
      refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

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

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

Tactic:
apply FormalMultilinearSeries.le_radius_of_isBigO
      refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO
      rw [norm_mul, norm_norm, norm_mul, norm_norm]
      refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
      rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

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

Goal state before:
pp: case zero
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
hi : i < b.length
hj : 0 < b.blocksFun ⟨i, hi⟩
⊢ a.sizeUpTo (b.sizeUpTo i + 0) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo 0

Tactic:
change
      sum (take (b.blocks.take i).sum a.blocks) =
        sum (take i (map sum (splitWrtComposition a.blocks b)))
    induction i with
    | zero => rfl
    | succ i IH =>
      have A : i < b.length := Nat.lt_of_succ_lt hi
      have B : i < List.length (map List.sum (splitWrtComposition a.blocks b)) := by simp [A]
      have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
      rw [sum_take_succ _ _ B, ← IH A C]
      have :
        take (sum (take i b.blocks)) a.blocks =
          take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) := by
        rw [take_take, min_eq_left]
        apply monotone_sum_take _ (Nat.le_succ _)
      rw [this, getElem_map, getElem_splitWrtComposition, ←
        take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks),
        sum_append]
      congr
      rw [take_append_drop]

Goal state after:
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✝‖ₑ < r / ‖u‖ₑ
⊢ ‖↑u y✝‖ₑ < r

Tactic:
exact lt_of_le_of_lt (ContinuousLinearMap.le_opENorm _ _) (mul_lt_of_lt_div' hy2)

Goal state after:
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:
intro y hy

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
hy : 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: 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
f1 : A → A := fun a ↦ a * z.inv
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
let f2 : A → A := fun b ↦ (1 - b)⁻¹ʳ

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
f1 : A → A := fun a ↦ a * z.inv
f2 : A → A := fun b ↦ (1 - b)⁻¹ʳ
⊢ AnalyticAt 𝕜 Ring.inverse ↑z
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 ∈ Metric.ball ↑z ‖↑z⁻¹‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ

Tactic:
simp only [Metric.mem_ball, dist_eq_norm] at hy

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⁻¹‖⁻¹
⊢ (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
⊢ ∀ a ∈ f ⁻¹' {0}ᶜ, g a = ((f⁻¹ • f) • g) a

Tactic:
intro y hy

Goal state after:
𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
y : E
hy : y ∈ f ⁻¹' {0}ᶜ
⊢ g y = ((f⁻¹ • f) • g) y