mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e_a.succ.succ.h₀.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i j : ℕ
hj : j + 1 + 1 ∈ Finset.range (i + 2 + 1)
hj' : j + 1 + 1 ≠ 0
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ (j + 1 + 1) * B ^ (i + 2 - (j + 1 + 1)) * ↑((i + 2).choose (j + 1 + 1))) = 0

Tactic:
← neg_mul,

Goal state after:
case e_a.succ.succ.h₀.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i j : ℕ
hj : j + 1 + 1 ∈ Finset.range (i + 2 + 1)
hj' : j + 1 + 1 ≠ 0
⊢ (coeff (n + 2)) ((-C k * X ^ (n + 2)) ^ (j + 1 + 1) * B ^ (i + 2 - (j + 1 + 1)) * ↑((i + 2).choose (j + 1 + 1))) = 0
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : y ∈ tangentConeAt R s x
⊢ ∃ α l,
    ∃ (_ : l.NeBot), ∃ c d, Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) l (𝓝 y)

Tactic:
tangentConeAt,

Goal state after:
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : y ∈ {y | ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)}
⊢ ∃ α l,
    ∃ (_ : l.NeBot), ∃ c d, Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) l (𝓝 y)
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : s ⊆ t
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Tactic:
simp only [tangentConeAt_def, ofPred_subset_ofPred]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : s ⊆ t
⊢ ∀ (a : E), ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) → ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' t] 0)
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : SMul 𝕜 E
inst✝⁴ : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst✝³ : Monoid 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x

Tactic:
simp only [tangentConeAt_def, ofPred_subset_ofPred]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : SMul 𝕜 E
inst✝⁴ : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst✝³ : Monoid 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
⊢ ∀ (a : E), ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) → ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : SMul 𝕜 E
inst✝⁴ : TopologicalSpace E
s : Set E
x : E
𝕜' : Type u_3
inst✝³ : Monoid 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x

Tactic:
by
  simp only [tangentConeAt_def, ofPred_subset_ofPred]
  refine fun y hy ↦ hy.mono ?_
  rw [← smul_one_smul (Filter 𝕜')]
  grw [le_top (a := ⊤ • 1)]

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul 𝕜 E
inst✝¹ : TopologicalSpace E
s t : Set E
x : E
inst✝ : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
⊢ tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜 t x

Tactic:
simp only [tangentConeAt_def, ofPred_subset_ofPred]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : SMul 𝕜 E
inst✝¹ : TopologicalSpace E
s t : Set E
x : E
inst✝ : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
⊢ ∀ (a : E), ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0) → ClusterPt a (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' t] 0)
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Semiring 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
s : Set E
x : E
hx : x ∈ closure[inst✝¹] s
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
mem_closure_iff_frequently

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Semiring 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ 0 ∈ tangentConeAt 𝕜 s x
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂

Tactic:
by
  simp only [isLittleOTVS_iff_tendsto_div]
  peel with U hU V hV
  exact tendsto_congr' (hf.comp₂ (egauge _ _ · / egauge _ _ ·) hg)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
⊢ egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x) →
    egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x) → egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ ↑ε * egauge 𝕜 (id W) (k x)

Tactic:
hfx

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hfx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x) → egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ ↑ε * egauge 𝕜 (id W) (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
x : α
⊢ egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x) →
    egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)

Tactic:
hfx

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
x : α
hfx : egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x) → egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ᶠ (x : ℝ≥0) in 𝓝 0, ↑x * ↑‖c‖₊ / ↑r < 1

Tactic:
refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ Continuous fun x ↦ ↑x * ↑‖c‖₊ / ↑r
Module: Mathlib.Analysis.Analytic.ChangeOrigin

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
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ HasSum (fun s ↦ ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) (‖p n‖₊ * (r + r') ^ n)

Tactic:
convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _

Goal state after:
case e'_5
𝕜 : 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
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ (fun s ↦ ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) = fun s ↦
    ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))

case convert_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
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ HasSum (fun s ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ n)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j✝ : Option ι
x y : G × ((i : ι) → E i)
j : ι
⊢ ((B (update v (some j) (x + y) none).1) fun i ↦ (update v (some j) (x + y) (some i)).2 i) =
    ((B (update v (some j) x none).1) fun i ↦ (update v (some j) x (some i)).2 i) +
      (B (update v (some j) y none).1) fun i ↦ (update v (some j) y (some i)).2 i

Tactic:
classical
        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
        simp [B]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G✝ : Type wG
G' : Type wG'
inst✝¹⁴ : Fintype ι
inst✝¹³ : Fintype ι'
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁹ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝⁸ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝⁷ : NormedAddCommGroup G✝
inst✝⁶ : NormedSpace 𝕜 G✝
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : Option ι → G × ((i : ι) → E i)
j✝ : Option ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
⊢ ((B (update v (some j) (c • x) none).1) fun i ↦ (update v (some j) (c • x) (some i)).2 i) =
    c • (B (update v (some j) x none).1) fun i ↦ (update v (some j) x (some i)).2 i

Tactic:
classical
        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
        simp [B]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) ↑r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y

Tactic:
set A : ℕ → F := fun n => (p n fun _ => y.1 - x) - p n fun _ => y.2 - x

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
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
y : E × E
hy' : y ∈ Metric.eball (x, x) ↑r'
ys : y ∈ insert x s ×ˢ insert x s
hy : y ∈ Metric.eball x r ×ˢ Metric.eball x r
A : ℕ → F := fun n ↦ ((p n) fun x_1 ↦ y.1 - x) - (p n) fun x_1 ↦ y.2 - x
⊢ ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
n✝ n : ℕ
v : Fin (n + 2) → E
A : univ = {c | c.length < n + 2}.toFinset ∪ {Composition.ones (n + 2)}
B : Disjoint {c | c.length < n + 2}.toFinset {Composition.ones (n + 2)}
j : ℕ
hj1 : j < (Composition.ones (n + 2)).length
hj2 : j < n + 2
⊢ ((p 1) fun x ↦ v (Fin.castLE ⋯ ⟨j, hj1⟩)) = (p 1) fun x ↦ v ⟨j, hj2⟩

Tactic:
exact FormalMultilinearSeries.congr _ rfl fun k _ _ => by congr

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n : ℕ
v : Fin (n + 2) → F
N : 0 < n + 2
c : Composition (n + 2)
j : ℕ
hj1 hj2 : j < c.length
hc : 1 < c.length
⊢ ∀ (k : Fin c.length), c.blocksFun k < n + 2

Tactic:
simp [← Composition.ne_single_iff N, Composition.eq_single_iff_length, ne_of_gt hc]

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
m M N n : ℕ
f : Fin n → ℕ
hi : ⟨n, f⟩ ∈ compPartialSumSource m M N
⊢ (n : ℕ) × Composition n

Tactic:
mem_compPartialSumSource_iff

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
m M N n : ℕ
f : Fin n → ℕ
hi : (m ≤ ⟨n, f⟩.fst ∧ ⟨n, f⟩.fst < M) ∧ ∀ (a : Fin ⟨n, f⟩.fst), 1 ≤ ⟨n, f⟩.snd a ∧ ⟨n, f⟩.snd a < N
⊢ (n : ℕ) × Composition n
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
hi : i ∈ compPartialSumSource m M N
⊢ (compChangeOfVariables m M N i hi).snd.length = i.fst

Tactic:
rcases i with ⟨k, blocks_fun⟩
  dsimp [compChangeOfVariables]
  simp only [Composition.length, length_ofFn]

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

Goal state before:
pp: case refine_2
m M N n : ℕ
c : Composition n
hi : ⟨n, c⟩ ∈ compPartialSumTargetSet m M N
⊢ compChangeOfVariables m M N ⟨c.length, c.blocksFun⟩ ⋯ = ⟨n, c⟩

Tactic:
dsimp [compChangeOfVariables]
    rw [Composition.sigma_eq_iff_blocks_eq]
    simp only [Composition.blocksFun]
    conv_rhs => rw [← List.ofFn_get c.blocks]

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

Goal state before:
pp: case hi
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
⊢ compChangeOfVariables m M N ⟨k, blocks_fun⟩ H ∈ compPartialSumTarget m M N

Tactic:
mem_compPartialSumSource_iff

Goal state after:
case hi
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H✝ : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
H :
  (m ≤ ⟨k, blocks_fun⟩.fst ∧ ⟨k, blocks_fun⟩.fst < M) ∧
    ∀ (a : Fin ⟨k, blocks_fun⟩.fst), 1 ≤ ⟨k, blocks_fun⟩.snd a ∧ ⟨k, blocks_fun⟩.snd a < N
⊢ compChangeOfVariables m M N ⟨k, blocks_fun⟩ H✝ ∈ compPartialSumTarget m M N
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ 0 < (p.leftInv i x).radius

Tactic:
by
  rw [leftInv_eq_rightInv _ _ _ h]
  exact radius_rightInv_pos_of_radius_pos 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
x : E
q : FormalMultilinearSeries 𝕜 F G
m : ℕ
hm : HasFiniteFPowerSeriesAt g q (f x) m
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : HasFiniteFPowerSeriesAt f p x n
⊢ HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * (n + 1))

Tactic:
exact hm.comp (hn.of_le (Nat.le_succ n)) (Nat.zero_lt_succ n)

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 : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ (ofFn fun j ↦ (i.snd j).blocks).flatten.sum = n

Tactic:
simp [sum_ofFn, Composition.blocks_sum, Composition.sum_blocksFun]

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
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‖ₑ)
⊢ HasSum (fun n ↦ (pf.compContinuousLinearMap u n) fun x ↦ y✝) ((f ∘ ⇑u) (x + y✝))

Tactic:
convert! hf.hasSum _ _

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✝)

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

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