mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ (↑⟨Units.mk0 (embedding (extension x)) ⋯, ⋯⟩ <
      if h : (ofClass extensionValuation) ↑⋯.choose = 0 then 0
      else ↑⟨Units.mk0 ((ofClass extensionValuation) ↑⋯.choose) h, ⋯⟩) ↔
    extension x < ↑γ

Tactic:
← hy_def,

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ (↑⟨Units.mk0 (embedding (extension x)) ⋯, ⋯⟩ <
      if h : (ofClass extensionValuation) ↑y = 0 then 0 else ↑⟨Units.mk0 ((ofClass extensionValuation) ↑y) h, ⋯⟩) ↔
    extension x < ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = ↑n
d : σ →₀ ℕ
hd : (coeff d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
⊢ (coeff d) f ≠ 0 ∧ (weight w) d = n

Tactic:
simpa [h, Nat.cast_inj, ne_eq] using hd

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
⊢ ∑ x ∈ antidiagonal x, MvPolynomial.coeff x.1 ((truncFinset R s) f) * MvPolynomial.coeff x.2 ((truncFinset R t) g) =
    ∑ p ∈ antidiagonal x, (coeff p.1) f * (coeff p.2) g

Tactic:
apply sum_congr rfl

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
⊢ ∀ x_1 ∈ antidiagonal x,
    MvPolynomial.coeff x_1.1 ((truncFinset R s) f) * MvPolynomial.coeff x_1.2 ((truncFinset R t) g) =
      (coeff x_1.1) f * (coeff x_1.2) g
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ (valueGroupOrderIso K v) ((valuation K v).restrict x) < (valueGroupOrderIso K v) ↑γ

Tactic:
valueGroupOrderIso_restrict

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ Valued.v.restrict x.toCompletion < (valueGroupOrderIso K v) ↑γ
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_3
R : Type u_4
t u : TopologicalSpace R
htu : t ≤ u
⊢ instTopologicalSpace R ≤ instTopologicalSpace R

Tactic:
by
  change ⨅ i, _ ≤ ⨅ i, _
  gcongr

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
⊢ ∑ i ∈ range (n + 1), G (((trunc (n + 1)) f).coeff i) * s ^ i = ∑ i ∈ range (n + 1), G ((coeff i) f) * s ^ i

Tactic:
apply sum_congr rfl

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
⊢ ∀ x ∈ range (n + 1), G (((trunc (n + 1)) f).coeff x) * s ^ x = G ((coeff x) f) * s ^ x
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : K
⊢ v.adicAbvDef hb (x + y) ≤ max (v.adicAbvDef hb x) (v.adicAbvDef hb y)

Tactic:
simp only [adicAbvDef]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : K
⊢ (toNNReal ⋯) ((valuation K v) (x + y)) ≤ max ((toNNReal ⋯) ((valuation K v) x)) ((toNNReal ⋯) ((valuation K v) y))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ ((monomial n) a).order = ↑n

Tactic:
order_monomial,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ (if a = 0 then ⊤ else ↑n) = ↑n
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0

Tactic:
by_cases h : f = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0

case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
h : ¬f = 0
⊢ constantCoeff f.divXPowOrder = 0 ↔ f = 0
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f : MvPowerSeries σ R
hf : f ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (-f) ∈ Jd.1

Tactic:
by simp only [map_neg, neg_mem, hf e he]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
r : R
⊢ eval₂ φ a (C r) = φ r

Tactic:
rw [← Polynomial.coe_C, eval₂_coe, Polynomial.eval₂_C]

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
a : S
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformSpace S
inst✝⁸ : IsUniformAddGroup R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : T2Space S
inst✝⁴ : CompleteSpace S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
p : Polynomial R
⊢ (aeval ha) ↑p = (Polynomial.aeval a) p

Tactic:
rw [coe_aeval, Polynomial.aeval_def, eval₂_coe]

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
a : S
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformSpace S
inst✝⁸ : IsUniformAddGroup R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : T2Space S
inst✝⁴ : CompleteSpace S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
f : R⟦X⟧
⊢ HasSum (fun d ↦ (coeff d) f • a ^ d) (eval₂ (algebraMap R S) a f)

Tactic:
← algebraMap_smul (R := R) S,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
a : S
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformSpace S
inst✝⁸ : IsUniformAddGroup R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : T2Space S
inst✝⁴ : CompleteSpace S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
f : R⟦X⟧
⊢ HasSum (fun d ↦ (algebraMap R S) ((coeff d) f) • a ^ d) (eval₂ (algebraMap R S) a f)
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
a : σ → S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum (fun d ↦ (coeff d) f • d.prod fun s e ↦ a s ^ e) (eval₂ (algebraMap R S) a f)

Tactic:
← algebraMap_smul (R := R) S,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
a : σ → S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
f : MvPowerSeries σ R
⊢ HasSum (fun d ↦ (algebraMap R S) ((coeff d) f) • d.prod fun s e ↦ a s ^ e) (eval₂ (algebraMap R S) a f)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ #↑{a} < 𝔠

Tactic:
mk_singleton

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
⊢ subst 0 f = (map (algebraMap R S)) (C (constantCoeff f))

Tactic:
classical
  ext n
  rw [coeff_subst (by simp [hasSubst_def]), coeff_map, finsum_eq_single _ 0]
  · by_cases hn : n = 0
    · simp [hn, Algebra.algebraMap_eq_smul_one]
    simp [coeff_C_of_ne_zero hn, coeff_one, hn]
  intro d hd
  obtain ⟨i, hi⟩ : d.support.Nonempty := d.support_nonempty_iff.mpr hd
  simp [Finsupp.prod, Finset.prod_eq_zero hi, coeff_zero, zero_pow <| d.mem_support_iff.mp hi]

Goal state after:
Module: Mathlib.Analysis.Complex.Cardinality

Goal state before:
pp: ⊢ #↑Set.univ = 𝔠

Tactic:
rw [mk_univ, mk_complex]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
⊢ ∀ x ∈ n.divisorsAntidiagonal,
    Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 x.1 *
        Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 x.2 =
      0

Tactic:
intro (a, b) hk

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: τ : Type u_3
S : Type u_4
inst✝ : CommRing S
t : τ
⊢ HasSubst (MvPowerSeries.X t)

Tactic:
simp [HasSubst]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (n.prod fun s m ↦ a s ^ m) * (coeff n) f =
    ∑ i ∈ Set.Finite.toFinset ⋯, (coeff i) f • (coeff n) (i.prod fun s e ↦ (a • X) s ^ e)

Tactic:
simp only [Pi.smul_apply', smul_eq_mul]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (n.prod fun s m ↦ a s ^ m) * (coeff n) f =
    ∑ d ∈ ⋯.toFinset, (coeff d) f * (coeff n) (d.prod fun s e ↦ (a s • X s) ^ e)
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)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
⊢ ∑ᶠ (d : ℕ), (coeff d) P • (coeff n) (P.substInv ^ d) =
    ∑ᶠ (d : ℕ), (coeff d) P • (coeff n) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ d)

Tactic:
congr! 3 with m

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
m : ℕ
⊢ (coeff n) (P.substInv ^ m) = (coeff n) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ m)
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:
by
  simp only [tangentConeAt_def, ofPred_subset_ofPred]
  refine fun y hy ↦ hy.mono ?_
  gcongr

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
x : E
c : F
⊢ fderiv 𝕜 (fun x ↦ c) x = 0

Tactic:
by
  rw [fderiv, fderivWithin_const_apply]

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 : Set 𝕜
h : ¬AccPt x (𝓟 s)
⊢ derivWithin f s x = 0

Tactic:
rw [derivWithin, fderivWithin_zero_of_not_accPt h, zero_apply]

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₁ : 𝕜 → F
f₀' f₁' : F
L : Filter (𝕜 × 𝕜)
h₀ : Prod.map f₀ f₀ =ᶠ[L] Prod.map f₁ f₁
h₁ : f₀' = f₁'
⊢ ∀ (x : 𝕜), (toSpanSingleton 𝕜 f₀') x = (toSpanSingleton 𝕜 f₁') x

Tactic:
by simp [h₁]

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
f' : F
x₀ : 𝕜
hf : HasDerivAt f f' x₀
s : Set 𝕜
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C

Tactic:
by
  simpa using HasFDerivAt.le_of_lipschitzOn hf.hasFDerivAt hs hlip

Goal state after:
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.isLittleOTVS_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,
        ∀ (ε : ℝ≥0), ε ≠ 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✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
⊢ ∀ (x : E × E), ‖x.1 - x.2‖ = 0 → ‖f x.1 - f x.2 - f' (x.1 - x.2)‖ = 0

Tactic:
simp +contextual [sub_eq_zero]

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

Goal state before:
pp: case mp
α : 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ j, 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 ↑r) (g x)
hr₀ : 0 < r
⊢ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
refine ⟨(‖c‖₊ / r : ℝ≥0), hr.mono fun x hx ↦ ?_⟩

Goal state after:
case mp
α : 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ j, 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 ↑r) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 ↑r) (g x)
⊢ ‖f x‖ ≤ ↑(‖c‖₊ / r) * ‖g x‖
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
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
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩) (∑ s, (p n) (s.piecewise (fun x_1 ↦ x) fun x ↦ y))

Tactic:
simp_rw [← changeOriginSeriesTerm_changeOriginIndexEquiv_symm]

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
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
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
⊢ HasSum (fun c ↦ (f ∘ ⇑changeOriginIndexEquiv.symm) ⟨n, c⟩)
    (∑ x_1,
      ((p.changeOriginSeriesTerm (changeOriginIndexEquiv.symm ⟨n, x_1⟩).fst
            (changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.fst ↑(changeOriginIndexEquiv.symm ⟨n, x_1⟩).snd.snd ⋯)
          fun x_2 ↦ x)
        fun x ↦ y)
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 : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
⊢ ‖{ toFun := curryRight, map_add' := ⋯, map_smul' := ⋯, invFun := uncurryRight, left_inv := ⋯, right_inv := ⋯ }.symm
        f‖ ≤
    ‖f‖

Tactic:
simp only [uncurryRight, LinearEquiv.coe_symm_mk]

Goal state after:
𝕜 : 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 : Ei i.castSucc [×n]→L[𝕜] Ei (last n) →L[𝕜] G
⊢ ‖((ContinuousLinearMap.coeLM 𝕜).compMultilinearMap f.toMultilinearMap).uncurryRight.mkContinuous ‖f‖ ⋯‖ ≤ ‖f‖
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
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s (x + (y - x)) (r - ‖y - x‖ₑ)
⊢ AnalyticWithinAt 𝕜 f s y

Tactic:
rw [add_sub_cancel] at this

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
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : y ∈ insert x s ∩ Metric.eball x r
this✝ : ↑‖y - x‖₊ < r
this : HasFPowerSeriesWithinOnBall f (p.changeOrigin (y - x)) s y (r - ‖y - x‖ₑ)
⊢ AnalyticWithinAt 𝕜 f s y
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
y z : E
hz1 : x + y + z ∈ insert (x + y) (s + {y})
hz2 : z ∈ Metric.eball 0 r
⊢ HasSum (fun n ↦ (p n) fun x ↦ z) (f (x + y + z - y))

Tactic:
have : x + z ∈ insert x s := by
      simp only [add_singleton, image_add_right, mem_insert_iff, add_eq_left, mem_preimage] at hz1 ⊢
      abel_nf at hz1
      assumption
    convert hf.hasSum this hz2
    abel

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
x : E
hf : AnalyticAt 𝕜 f x
y : E
⊢ AnalyticAt 𝕜 (fun z ↦ f (z - y)) (x + y)

Tactic:
obtain ⟨p, hf⟩ := hf
  exact ⟨p, hf.comp_sub _⟩

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
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
y : E
⊢ AnalyticWithinAt 𝕜 (fun z ↦ f (z - y)) (s + {y}) (x + y)

Tactic:
obtain ⟨p, hf⟩ := hf
  exact ⟨p, hf.comp_sub _⟩

Goal state after: