mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : ι → 𝕜
hr₀ : 0 < r
hI : ∅.Finite
hU : ∀ i ∈ ∅, Balanced 𝕜 (U i)
hI₀ : ∅ = univ ∨ (∃ i ∈ ∅, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
hr : ⨆ i ∈ ∅, egauge 𝕜 (U i) (x i) < r
hc : ∀ i ∈ ∅, x i ∈ c i • U i
hcr : ∀ i ∈ ∅, ‖c i‖ₑ < r
hbot : (𝓝[≠] 0).NeBot
c₀ : 𝕜
hc₀ : c₀ ≠ 0
hc₀r : ‖c₀‖ₑ < r
⊢ ∀ i ∈ ∅, ‖c i‖ ≤ ‖c₀‖

Tactic:
simp

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

Goal state before:
pp: case e_a.succ.succ.h₁
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 : ℕ
⊢ 0 ∉ Finset.range (i + 2 + 1) →
    (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ 0 * B ^ (i + 2 - 0) * ↑((i + 2).choose 0)) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case zero
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n : ℕ
i : ι
hi : 0 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) 0 = 1 0

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : Finite ι
U : (i : ι) → Set (E i)
hU : ∀ (i : ι), Balanced 𝕜 (U i)
x : (i : ι) → E i
⊢ ⨆ i ∈ univ, egauge 𝕜 (U i) (x i) = ⨆ i, egauge 𝕜 (U i) (x i)

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ x - x = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
this : Invertible ((coeff 1) P.substInv)
Q : R⟦X⟧ := P.substInv.substInv
hQ : HasSubst Q
eq_aux : subst Q P.substInv = X
⊢ subst Q (subst P.substInv P) = P

Tactic:
simp [subst_comp_subst_apply (HasSubst.substInv P) hQ, eq_aux]

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 →₀ ℕ
x✝ : Unit
⊢ MvPowerSeries.constantCoeff (X₀ + X₁) = 0

Tactic:
simp

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 →₀ ℕ
b : (Fin 2 →₀ ℕ) × (Fin 2 →₀ ℕ)
hb : b ∈ antidiagonal e
hb' : b ≠ (single 0 (e 0), single 1 (e 1))
hmul_ne_zero : ¬(MvPowerSeries.coeff b.1) (subst X₀ f) * (MvPowerSeries.coeff b.2) (subst X₁ f) = 0
h0 : b.1 = single 0 (b.1 0) ∧ ¬(coeff (b.1 0)) f = 0
h1 : b.2 = single 1 (b.2 1) ∧ ¬(coeff (b.2 1)) f = 0
⊢ single 0 (b.1 0) =
      (single 0 ((single 0 (b.1 0) + single 1 (b.2 1)) 0), single 1 ((single 0 (b.1 0) + single 1 (b.2 1)) 1)).1 ∧
    single 1 (b.2 1) =
      (single 0 ((single 0 (b.1 0) + single 1 (b.2 1)) 0), single 1 ((single 0 (b.1 0) + single 1 (b.2 1)) 1)).2

Tactic:
simp

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

Goal state before:
pp: case «0»
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
⊢ (single 0 (e 0) + single 1 (e 1)) ((fun i ↦ i) ⟨0, ⋯⟩) = e ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1»
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
⊢ (single 0 (e 0) + single 1 (e 1)) ((fun i ↦ i) ⟨1, ⋯⟩) = e ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

Goal state after:
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 : E) in 𝓝 x, x ∈ s
⊢ x + -x = 0

Tactic:
simp

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

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
x : E
s t : Set E
h : s =ᶠ[𝓝[≠] x] t
⊢ fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x

Tactic:
by
  classical
  simp only [fderivWithin, differentiableWithinAt_congr_set_nhdsNE h,
    hasFDerivWithinAt_congr_set_nhdsNE h]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DivisionSemiring 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : ContinuousSMul 𝕜 E
x : E
⊢ Dense ↑(Submodule.span 𝕜 univ) ∧ x ∈ closure[inst✝³] univ

Tactic:
simp

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

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
c : F
L : Filter (E × E)
x✝ : E × E
⊢ 0 x✝ = c - c - 0 (x✝.1 - x✝.2)

Tactic:
simp

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

Goal state before:
pp: a : ℝ
⊢ (interior (Ioi a)).Nonempty

Tactic:
simp

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

Goal state before:
pp: a : ℝ
⊢ a ∈ closure (Ioi a)

Tactic:
simp

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

Goal state before:
pp: a : ℝ
⊢ (interior (Iio a)).Nonempty

Tactic:
simp

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

Goal state before:
pp: a : ℝ
⊢ a ∈ closure (Iio a)

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : 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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 ∅ x

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
unfold derivWithin

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ (fderivWithin 𝕜 f s x) 1 = 0
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 1 = 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ 0 1 = 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ derivWithin f (s ∩ t) x = derivWithin f s x

Tactic:
unfold derivWithin

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s t : Set 𝕜
ht : t ∈ 𝓝 x
⊢ (fderivWithin 𝕜 f (s ∩ t) x) 1 = (fderivWithin 𝕜 f s x) 1
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
unfold derivWithin

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
unfold derivWithin

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s t : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ derivWithin f₁ t =ᶠ[𝓝[s] x] derivWithin f t

Tactic:
unfold derivWithin

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s t : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ (fun x ↦ (fderivWithin 𝕜 f₁ t x) 1) =ᶠ[𝓝[s] x] fun x ↦ (fderivWithin 𝕜 f t x) 1
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : f₁ =ᶠ[𝓝[≠] x] f
⊢ deriv f₁ =ᶠ[𝓝[≠] x] deriv f

Tactic:
rw [Filter.EventuallyEq, ← eventually_nhdsNE_eventually_nhds_iff] at *

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: case inr
𝕜 : 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
inst✝ : T1Space E
y : E
h : x ≠ y
hf : HasFDerivWithinAt f f' s x
⊢ s ∈ 𝓝[s] x

Tactic:
self_mem_nhdsWithin

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

Goal state before:
pp: case inr
𝕜 : 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
inst✝ : T1Space E
y : E
h : x ≠ y
hf : HasFDerivWithinAt f f' s x
⊢ s ∈ 𝓝[insert y s] x

Tactic:
simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin]

Goal state after:
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‖
⊢ ↑0 * ↑‖c‖₊ / ↑r = 0

Tactic:
simp

Goal state after:
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‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : ↑ε * ↑‖c‖₊ / ↑r < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
⊢ r ≠ 0 ∨ ‖1‖ ≠ 0

Tactic:
simp

Goal state after:
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
L : Filter (E × E)
⊢ ∀ (x : E × E), 0 x = id x.1 - id x.2 - (ContinuousLinearMap.id 𝕜 E) (x.1 - x.2)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v ⟨i, him⟩ = w ⟨i, hin⟩
⊢ (p m) v = (p m) w

Tactic:
congr with ⟨i, hi⟩

Goal state after:
case e_6
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
m : ℕ
v w : Fin m → E
h2 : ∀ (i : ℕ) (him hin : i < m), v ⟨i, him⟩ = w ⟨i, hin⟩
i : ℕ
hi : i < m
⊢ v ⟨i, hi⟩ = w ⟨i, hi⟩
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
z : 𝕜
⊢ ((p n) fun x ↦ z) = z ^ n • p.coeff n

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: case zero
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
x✝ : Fin 0 → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 0) x✝ = (0 0) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: case succ
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
a✝ : ∀ (x : Fin n✝ → E), (constFormalMultilinearSeries 𝕜 E 0 n✝) x = (0 n✝) x
x✝ : Fin (n✝ + 1) → E
⊢ (constFormalMultilinearSeries 𝕜 E 0 (n✝ + 1)) x✝ = (0 (n✝ + 1)) x✝

Tactic:
simp

Goal state after:
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
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)
⊢ (fun x ↦ f x • 1 x) =ᶠ[l] f

Tactic:
simp

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
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
⊢ 1 * 1 * ↑‖g x‖₊ = ↑‖g x‖₊

Tactic:
simp

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

Goal state before:
pp: case h₂
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ ↑‖f x‖₊ ≤ ↑(ε * δ / ‖c‖₊) * ↑‖g x‖₊

Tactic:
exact_mod_cast hx

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
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ 1 * 1 * ↑δ * ↑‖g x‖₊ = ↑δ * ↑‖g x‖₊

Tactic:
simp

Goal state after:
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
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ∀ (k' l' : ℕ),
    k' = k →
      l' = l →
        ∀ (hkl : k + l = k' + l') (hs' : (Finset.map (finCongr hkl).toEmbedding s).card = l'),
          ⟨k', ⟨l', ⟨Finset.map (finCongr hkl).toEmbedding s, hs'⟩⟩⟩ = ⟨k, ⟨l, ⟨s, hs⟩⟩⟩

Tactic:
simp

Goal state after:
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
x : E
hx : ‖x‖ₑ < p.radius
n : ℕ
⊢ ‖p n‖ * ∏ i, ‖x‖ = ‖p n‖ * ↑‖x‖₊ ^ n

Tactic:
simp

Goal state after:
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
n : ℕ
⊢ ∀ (x : E [×1]→L[𝕜] F), ‖↑↑(continuousMultilinearCurryFin1 𝕜 E F) x‖ ≤ 1 * ‖x‖

Tactic:
simp

Goal state after:
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
⊢ p.radius ≤ (c • p).radius

Tactic:
simp only [radius, smul_apply]

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, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖c • p n‖ * ↑r ^ n ≤ C), ↑r
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ ‖p n‖ * ∏ i, ‖u‖ ≤ ‖p n‖ * ‖u‖ ^ n

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ 0 ≤ ‖u‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ 0 ≤ ‖p n‖

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
⊢ p.radius / ‖0‖ₑ ≤ (p.compContinuousLinearMap 0).radius

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ ‖u‖ₑ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : ↑r < p.radius
⊢ ‖u‖ₑ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Nontrivial F
p : FormalMultilinearSeries 𝕜 F G
u : E ≃L[𝕜] F
this : (p.compContinuousLinearMap ↑u).radius / ‖↑u.symm‖ₑ ≤ p.radius
⊢ ‖↑u.symm‖ₑ ≠ ∞

Tactic:
simp

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

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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
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
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin x k)
s : (b : ℕ) × { s // s.card = b }
⊢ ‖p.changeOriginSeriesTerm k s.fst ↑s.snd ⋯‖₊ * ∏ i, ‖x‖₊ = ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst

Tactic:
simp

Goal state after: