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:
mul_pow,

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) ^ (j + 1 + 1) * (X ^ (n + 2)) ^ (j + 1 + 1) * B ^ (i + 2 - (j + 1 + 1)) * ↑((i + 2).choose (j + 1 + 1))) =
    0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
h✝ : ∀ (s : Finset ι), (∏ b ∈ s, f b).IsMultiplicative
key : ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, (∏ b ∈ i, f b) 1 = (∏' (b : ι), f b) 1
h : ∀ (x : Finset ι), (∏ b ∈ x, f b) 1 = 1
⊢ (eulerProduct f) 1 = 1

Tactic:
h

Goal state after:
case pos.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
h✝ : ∀ (s : Finset ι), (∏ b ∈ s, f b).IsMultiplicative
h : ∀ (x : Finset ι), (∏ b ∈ x, f b) 1 = 1
key : ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, 1 = (∏' (b : ι), f b) 1
⊢ (eulerProduct f) 1 = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
h✝ : ∀ (s : Finset ι), (∏ b ∈ s, f b).IsMultiplicative
key : ∀ (n : ℕ), ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, (∏ b ∈ i, f b) n = (∏' (b : ι), f b) n
m n : ℕ
hmn : m.Coprime n
h : ∀ (s : Finset ι), (∏ b ∈ s, f b) (m * n) = (∏ b ∈ s, f b) m * (∏ b ∈ s, f b) n
h2 : ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, (∏ b ∈ i, f b) (m * n) = (∏' (b : ι), f b) (m * n)
⊢ (eulerProduct f) (m * n) = (eulerProduct f) m * (eulerProduct f) n

Tactic:
h

Goal state after:
case pos.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (i : ι), (f i).IsMultiplicative
hf' : Multipliable f
h✝ : ∀ (s : Finset ι), (∏ b ∈ s, f b).IsMultiplicative
key : ∀ (n : ℕ), ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter, (∏ b ∈ i, f b) n = (∏' (b : ι), f b) n
m n : ℕ
hmn : m.Coprime n
h : ∀ (s : Finset ι), (∏ b ∈ s, f b) (m * n) = (∏ b ∈ s, f b) m * (∏ b ∈ s, f b) n
h2 :
  ∀ᶠ (i : Finset ι) in (SummationFilter.unconditional ι).filter,
    (∏ b ∈ i, f b) m * (∏ b ∈ i, f b) n = (∏' (b : ι), f b) (m * n)
⊢ (eulerProduct f) (m * n) = (eulerProduct f) m * (eulerProduct f) n
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 : ClusterPt y (map (fun p ↦ p.1 • p.2) (⊤ ×ˢ 𝓝[(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)

Tactic:
ClusterPt,

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 ⊓ map (fun p ↦ p.1 • p.2) (⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∃ α 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.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
x : E
⊢ ‖x‖ₑ / ↑r ≤ egauge 𝕜 (closedBall 0 ↑r) x

Tactic:
rw [le_egauge_iff]

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
x : E
⊢ ∀ (c : 𝕜), x ∈ c • closedBall 0 ↑r → ‖x‖ₑ / ↑r ≤ ‖c‖ₑ
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c✝ : 𝕜
x : E
r : ℝ≥0
hc✝ : 1 < ‖c✝‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
hx' : ‖x‖ₑ = 0
c : 𝕜
hc : c ∉ {0}
⊢ x ∈ c • ball 0 ↑r

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀ hc, norm_smul, hx, hr]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ), (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (∏ x ∈ {PUnit.unit}, (X₀ + X₁) ^ d x) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f

Tactic:
prod_singleton,

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ), (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) ((X₀ + X₁) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f
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
y : E
hy : ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ ⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' t] 0

Tactic:
gcongr _ • ?_

Goal state after:
case h
𝕜 : 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
y : E
hy : ClusterPt y (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0 ≤ 𝓝[(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
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousConstSMul 𝕜 E
⊢ tangentConeAt 𝕜 (closure[inst✝²] s) x = tangentConeAt 𝕜 s x

Tactic:
refine Subset.antisymm ?_ (tangentConeAt_mono subset_closure)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : SMul 𝕜 E
inst✝² : TopologicalSpace E
s : Set E
x : E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousConstSMul 𝕜 E
⊢ tangentConeAt 𝕜 (closure[inst✝²] s) x ⊆ tangentConeAt 𝕜 s x
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ (fun x i ↦ f i x) =O[𝕜; l] g

Tactic:
simp only [this.isBigOTVS_iff (basis_sets _), forall_and, Prod.forall, id]

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ ∀ (a : Set ι) (b : (i : ι) → Set (E i)),
    (a.Finite ∧ (∀ x ∈ a, b x ∈ 𝓝 0) ∧ ∀ x ∈ a, Balanced 𝕜 (b x)) →
      ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, (egauge 𝕜 (a.pi fun i ↦ b i) fun i ↦ f i x) ≤ egauge 𝕜 j (g x)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : 𝓝[s \ {x}] x = ⊥
⊢ (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝[s \ {x}] x] fun x' ↦ x' - x

Tactic:
h

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : 𝓝[s \ {x}] x = ⊥
⊢ (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; ⊥] fun x' ↦ x' - x
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_6
c : 𝕜'
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : IsBoundedSMul 𝕜' F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖c‖ * (‖p n‖ * ↑r ^ n) ≤ ‖c‖ * C

Tactic:
h

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_6
c : 𝕜'
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : SMulCommClass 𝕜 𝕜' F
inst✝ : IsBoundedSMul 𝕜' F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖c‖ * C ≤ ‖c‖ * C
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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ AnalyticAt 𝕜 f y

Tactic:
rw [← analyticWithinAt_univ]

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f univ y
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
⊢ ofScalars E a₁✝ = ofScalars E a₂✝ → a₁✝ = a₂✝

Tactic:
h

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
inst✝ : Nontrivial E
a₁✝ a₂✝ : ℕ → 𝕜
h : ofScalars E a₁✝ = ofScalars E a₂✝
⊢ a₁✝ = a₂✝
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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y | g y = f y}
r' : ℝ≥0∞ := min r ε
⊢ HasFPowerSeriesWithinAt g p s x

Tactic:
refine ⟨r', ?_⟩

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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y | g y = f y}
r' : ℝ≥0∞ := min r ε
⊢ HasFPowerSeriesWithinOnBall g p s x r'
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
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
finsupp : (Function.support f).Finite
hfkl : ∀ (k l : ℕ), HasSum (fun x ↦ f ⟨k, ⟨l, x⟩⟩) (((p.changeOriginSeries k l) fun x_1 ↦ x) fun x ↦ y)
k m : ℕ
hm : n ≤ m
⊢ ((p.changeOriginSeries k m) fun x_1 ↦ x) = 0

Tactic:
rw [changeOriginSeries_finite_of_finite _ hn _ (le_add_of_le_right hm), _root_.zero_apply]

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 y : E
⊢ HasFPowerSeriesWithinAt f p (insert y s) x ↔ HasFPowerSeriesWithinAt f p s x

Tactic:
rcases eq_or_ne x y with rfl | hy

Goal state after:
case inl
𝕜 : 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
⊢ HasFPowerSeriesWithinAt f p (insert x s) x ↔ HasFPowerSeriesWithinAt f p s x

case inr
𝕜 : 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 y : E
hy : x ≠ y
⊢ HasFPowerSeriesWithinAt f p (insert y s) x ↔ HasFPowerSeriesWithinAt f p s x
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
⊢ p.applyComposition c (Function.update v j z) k =
    Function.update (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j))) (Function.update (v ∘ ⇑(c.embedding (c.index j))) (c.invEmbedding j) z)) k

Tactic:
h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
⊢ p.applyComposition c (Function.update v j z) (c.index j) =
    Function.update (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j))) (Function.update (v ∘ ⇑(c.embedding (c.index j))) (c.invEmbedding j) z))
      (c.index j)
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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n✝ : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
this : y ∈ Metric.eball 0 r
ya : a * (‖y‖ / ↑r') ≤ a
n : ℕ
⊢ C * a ^ n * (‖y‖ / ↑r') ^ n ≤ C * (a * (‖y‖ / ↑r')) ^ n

Tactic:
mul_pow,

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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n✝ : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
this : y ∈ Metric.eball 0 r
ya : a * (‖y‖ / ↑r') ≤ a
n : ℕ
⊢ C * a ^ n * (‖y‖ / ↑r') ^ n ≤ C * (a ^ n * (‖y‖ / ↑r') ^ n)
Module: Mathlib.Analysis.Analytic.Composition

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
x : E
n : ℕ
b : Composition n
a✝ : b ∈ Finset.univ
hb : b ≠ Composition.ones n
k : ℕ
hk : k ∈ b.blocks
lt_k : 1 < k
i : Fin b.blocks.length
hi : b.blocks[i] = k
j : Fin b.length := ⟨↑i, ⋯⟩
⊢ 1 < b.blocksFun j

Tactic:
convert! lt_k

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

Goal state before:
pp: m M N : ℕ
i : (n : ℕ) × (Fin n → ℕ)
⊢ i ∈ compPartialSumSource m M N ↔ (m ≤ i.fst ∧ i.fst < M) ∧ ∀ (a : Fin i.fst), 1 ≤ i.snd a ∧ i.snd a < N

Tactic:
simp only [compPartialSumSource, Finset.mem_Ico, Fintype.mem_piFinset, Finset.mem_sigma]

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_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
⊢ x + y ∈ insert x s ∩ Metric.eball x δ

Tactic:
have : y ∈ Metric.eball (0 : E) δ :=
      (Metric.eball_subset_eball (le_trans (min_le_left _ _) (min_le_right _ _))) hy

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
this : y ∈ Metric.eball 0 δ
⊢ x + y ∈ insert x s ∩ Metric.eball x δ
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ ∀ {y : E},
    e + y ∈ insert e t → y ∈ Metric.eball 0 (min r s) → HasSum (fun n ↦ (p.prod q n) fun x ↦ y) (f (e + y), g (e + y))

Tactic:
intro y h'y hy
    simp_rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.prod_apply]
    refine (hf.hasSum h'y ?_).prodMk (hg.hasSum h'y ?_)
    · exact Metric.mem_eball.mpr (lt_of_lt_of_le hy (min_le_left _ _))
    · exact Metric.mem_eball.mpr (lt_of_lt_of_le hy (min_le_right _ _))

Goal state after:
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
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) s e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e

Tactic:
by
  refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩
  obtain ⟨r, hr⟩ := h
  exact ⟨r, (hasFPowerSeriesWithinOnBall_pi_iff hr.r_pos).1 hr i⟩

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1

Tactic:
by
  convert! hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝
  exact Ring.inverse_eq_inv'.symm

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

Goal state before:
pp: 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
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
⊢ g =ᶠ[𝓝 z] (f⁻¹ • f) • g

Tactic:
filter_upwards [h₁f.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.2 h₂f)]

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
⊢ ∀ a ∈ f ⁻¹' {0}ᶜ, g a = ((f⁻¹ • f) • g) a
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x
⊢ DifferentiableWithinAt 𝕜 ((f ∘ ⇑iso) ∘ ⇑iso.symm) s (iso x)

Tactic:
← iso.symm_apply_apply x

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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
⊢ DifferentiableWithinAt 𝕜 ((f ∘ ⇑iso) ∘ ⇑iso.symm) s (iso x)