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

Goal state before:
pp: case hab
𝕜 : 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 : edist y 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))))
n : ℕ
c : Composition n
⊢ ‖y‖ ≤ ↑r

Tactic:
edist_zero_right

Goal state after:
case hab
𝕜 : 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‖ₑ < 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))))
n : ℕ
c : Composition n
⊢ ‖y‖ ≤ ↑r
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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ HasFPowerSeriesWithinOnBall f p s x r ↔ ∃ g, EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ HasFPowerSeriesWithinOnBall f p s x r → ∃ g, EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r

case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ (∃ g, EqOn f g (insert x s ∩ eball x r) ∧ HasFPowerSeriesOnBall g p x r) → HasFPowerSeriesWithinOnBall f p s x r
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : y ∈ eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (g (x + y))

Tactic:
exact hg.hasSum lt

Goal state after:
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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
⊢ HasFPowerSeriesWithinAt f p s x ↔ ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
⊢ HasFPowerSeriesWithinAt f p s x → ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

case mpr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
⊢ (∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) → HasFPowerSeriesWithinAt f p s x
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case hab
𝕜 : 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
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : edist y 0 < r
hy0 : y ∈ Metric.eball 0 r0
n : ℕ
c : Composition n
⊢ ‖y‖ ≤ ↑r1

Tactic:
edist_zero_right

Goal state after:
case hab
𝕜 : 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
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : ‖y‖ₑ < r
hy0 : y ∈ Metric.eball 0 r0
n : ℕ
c : Composition n
⊢ ‖y‖ ≤ ↑r1
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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ (-pf).radius

Tactic:
pf.radius_neg

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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius
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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ (-pf).radius

Tactic:
pf.radius_neg

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
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius
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
this : (fun n ↦ ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x ↦ 1
⊢ ↑r ≤ p.radius ∧ ↑r ≤ q.radius

Tactic:
constructor

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
⊢ ↑r ≤ p.radius

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
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

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
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ (fun p ↦ (g ∘ f) p.1 - (g ∘ f) p.2 - (g' ∘SL f') (p.1 - p.2)) = fun p ↦
    g (f p.1) - g (f p.2) - g' (f p.1 - f p.2) + g' (f p.1 - f p.2 - f' (p.1 - p.2))

Tactic:
ext

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
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
x✝ : E × E
⊢ (g ∘ f) x✝.1 - (g ∘ f) x✝.2 - (g' ∘SL f') (x✝.1 - x✝.2) =
    g (f x✝.1) - g (f x✝.2) - g' (f x✝.1 - f x✝.2) + g' (f x✝.1 - f x✝.2 - f' (x✝.1 - x✝.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
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
⊢ (ofFn fun j ↦ (a.sigmaCompositionAux b j).blocks).flatten = a.blocks ∧
    (ofFn fun j ↦ (a.sigmaCompositionAux b j).length) = b.blocks

Tactic:
constructor

Goal state after:
case left
𝕜 : 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
⊢ (ofFn fun j ↦ (a.sigmaCompositionAux b j).blocks).flatten = a.blocks

case right
𝕜 : 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
⊢ (ofFn fun j ↦ (a.sigmaCompositionAux b j).length) = b.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
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hr : 0 < r
hf : ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r
⊢ HasFPowerSeriesWithinOnBall (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e r

Tactic:
exact HasFPowerSeriesWithinOnBall.pi hf hr

Goal state after:
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
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 - x)⁻¹ʳ) (formalMultilinearSeries_geometric 𝕜 A) 0 1

Tactic:
constructor

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

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

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)

Tactic:
ext

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : HasSummableGeomSeries A
inst✝ : Nontrivial A
x✝ : A
⊢ (1 + x✝)⁻¹ʳ = ((fun x ↦ (1 - x)⁻¹ʳ) ∘ ⇑(-ContinuousLinearMap.id 𝕜 A)) x✝
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
f2 : A → A := fun b ↦ (1 - b)⁻¹ʳ
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
let f3 : A → A := fun c ↦ 1 - z.inv * c

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)⁻¹ʳ
f3 : A → A := fun c ↦ 1 - z.inv * c
⊢ 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
⊢ ∀ᶠ (y : A) in 𝓝 ↑z, (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ

Tactic:
have : Metric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by
        apply Metric.ball_mem_nhds
        simp

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) in 𝓝 ↑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
⊢ AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (fun z ↦ f z • g z) z

Tactic:
constructor

Goal state after:
case mp
𝕜 : 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
⊢ AnalyticAt 𝕜 g z → AnalyticAt 𝕜 (fun z ↦ f z • g z) z

case mpr
𝕜 : 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
⊢ AnalyticAt 𝕜 (fun z ↦ f z • g z) z → AnalyticAt 𝕜 g z
Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
s : Set G'
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun y ↦ (B (f y)) (g y)) (((precompR G' B) (f x)) g' + ((precompL G' B) f') (g x)) s x

Tactic:
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prodMk hg)

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y ↦ -f y) s x = -fderivWithin 𝕜 f s x

Tactic:
exact h.hasFDerivWithinAt.neg.fderivWithin hxs

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M [⋀^ι]→L[R] N
⊢ (fun f ↦ f.compContinuousLinearMap ↑e) ((fun f ↦ f.compContinuousLinearMap ↑e.symm) f) = f

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M [⋀^ι]→L[R] N
x✝ : ι → M
⊢ ((fun f ↦ f.compContinuousLinearMap ↑e) ((fun f ↦ f.compContinuousLinearMap ↑e.symm) f)) x✝ = f x✝
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M' [⋀^ι]→L[R] N
⊢ (fun f ↦ f.compContinuousLinearMap ↑e.symm) ((fun f ↦ f.compContinuousLinearMap ↑e) f) = f

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M' [⋀^ι]→L[R] N
x✝ : ι → M'
⊢ ((fun f ↦ f.compContinuousLinearMap ↑e.symm) ((fun f ↦ f.compContinuousLinearMap ↑e) f)) x✝ = f x✝
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N
⊢ (↑e.symm).compContinuousAlternatingMap ((↑e).compContinuousAlternatingMap f) = f

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N
x✝ : ι → M
⊢ ((↑e.symm).compContinuousAlternatingMap ((↑e).compContinuousAlternatingMap f)) x✝ = f x✝
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N'
⊢ (↑e).compContinuousAlternatingMap ((↑e.symm).compContinuousAlternatingMap f) = f

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N'
x✝ : ι → M
⊢ ((↑e).compContinuousAlternatingMap ((↑e.symm).compContinuousAlternatingMap f)) x✝ = f x✝