mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
⊢ φ = X s ^ n * fun m ↦ (coeff (m + single s n)) φ

Tactic:
ext m

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
⊢ (coeff m) φ = (coeff m) (X s ^ n * fun m ↦ (coeff (m + single s n)) φ)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ (coeff d) (∏ j ∈ insert a s, f j) = ∑ l ∈ (insert a s).finsuppAntidiag d, ∏ i ∈ insert a s, (coeff (l i)) (f i)

Tactic:
| insert a s ha ih =>

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ constantCoeff f ^ #s = 0

Tactic:
suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ m ≤ #s
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
hs'' : ∀ i ∈ s, k i = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)

Tactic:
simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
    intro i hi hi'
    rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
    exact hi' hi

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

Goal state before:
pp: case neg.left
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ d_1, (coeff d_1) ((monomial d) a) ≠ 0 ∧ (weight w) d_1 = (weight w) d

Tactic:
use d
      simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]

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

Goal state before:
pp: case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) d
⊢ ¬b = d

Tactic:
rintro rfl

Goal state after:
case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) b
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
⊢ (trunc R n) (C a * p) = MvPolynomial.C a * (trunc R n) p

Tactic:
ext m

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) (C a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc R n) p)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
⊢ (trunc' R n) (C a * p) = MvPolynomial.C a * (trunc' R n) p

Tactic:
ext m

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
p : MvPowerSeries σ R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) (C a * p)) = MvPolynomial.coeff m (MvPolynomial.C a * (trunc' R n) p)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case insert
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff d) (f * ∏ i ∈ s, (1 - g i)) = (coeff d) f
h : ∀ i ∈ insert a s, ↑((weight w) d) < weightedOrder w (g i)
⊢ (coeff d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff d) f

Tactic:
| insert a s ha ih =>

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: case inr
a : ℕ∞
ha : 0 < a
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 * x2) (a, ⊤)

Tactic:
simp only [ContinuousAt, Function.uncurry, mul_top ha.ne']
        refine tendsto_nhds_top_mono continuousAt_snd ?_
        filter_upwards [continuousAt_fst (lt_mem_nhds ha)] with (x, y) (hx : 0 < x)
        exact le_mul_of_one_le_left' (Order.one_le_iff_pos.2 hx)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), degree d < n → (coeff d) f = 0
⊢ ↑n ≤ f.order

Tactic:
simp_rw [degree_eq_weight_one] at h

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight fun x ↦ 1) d < n → (coeff d) f = 0
⊢ ↑n ≤ f.order
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑(degree d) < n → (coeff d) f = 0
⊢ n ≤ f.order

Tactic:
simp_rw [degree_eq_weight_one] at h

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight fun x ↦ 1) d) < n → (coeff d) f = 0
⊢ n ≤ f.order
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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ (valuation K v) b * ↑n = (valuation K v) y

Tactic:
rw [hb, hy]; exact hx

Goal state after:
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
a : adicCompletion K v
ha : 1 < Valued.v a
ϖ : R
hϖ : v.intValuation ϖ = exp (-1)
this : Valued.v ((algebraMap R (adicCompletion K v)) ϖ) = (exp 1)⁻¹
⊢ ϖ ≠ 0

Tactic:
rintro rfl

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
a : adicCompletion K v
ha : 1 < Valued.v a
hϖ : v.intValuation 0 = exp (-1)
this : Valued.v ((algebraMap R (adicCompletion K v)) 0) = (exp 1)⁻¹
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
i : ℕ
hi : ↑(Finsupp.degree (single () i)) < MvPowerSeries.order φ
⊢ (coeff i) φ = 0

Tactic:
exact MvPowerSeries.coeff_of_lt_order hi

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ (trunc n) (↑((trunc n) f) * g) = (trunc n) (f * g)

Tactic:
ext m

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ ((trunc n) (↑((trunc n) f) * g)).coeff m = ((trunc n) (f * g)).coeff m
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case insert
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
k : ℕ
φ : R⟦X⟧
f : ι → R⟦X⟧
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff k) φ
⊢ (∀ i ∈ insert a s, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ insert a s, (1 - f i)) = (coeff k) φ

Tactic:
| insert a s ha ih =>

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
⊢ ↑((trunc n) ↑f) = ↑f

Tactic:
ext m

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
⊢ (coeff m) ↑((trunc n) ↑f) = (coeff m) ↑f
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R⟦X⟧
n : ℕ
⊢ (trunc n) ((map f) p) = Polynomial.map f ((trunc n) p)

Tactic:
ext m

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R⟦X⟧
n m : ℕ
⊢ ((trunc n) ((map f) p)).coeff m = (Polynomial.map f ((trunc n) p)).coeff m
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
apply X_pow_mul_cancel (k := f.order.toNat + g.order.toNat)

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)
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
inst✝¹³ : IsUniformAddGroup R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : IsUniformAddGroup S
inst✝¹⁰ : T2Space S
inst✝⁹ : CompleteSpace S
inst✝⁸ : IsTopologicalRing S
inst✝⁷ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
T : Type u_3
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous ⇑ε
p : Polynomial R
⊢ (⇑ε ∘ eval₂ φ a) ↑p = Polynomial.eval₂ (ε.comp φ) (ε a) p

Tactic:
simpa [Function.comp_apply, eval₂_coe] using p.hom_eval₂ φ ε a

Goal state after:
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
a : σ → MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⇑(aeval ⋯) = eval₂ (algebraMap R (MvPowerSeries τ S)) a

Tactic:
convert! coe_aeval (R := R) (hasSubst_iff_hasEval_of_discreteTopology.mp ha) <;>
  exact DiscreteUniformity.eq_bot.symm

Goal state after:
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
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e) = 0

Tactic:
finsum_eq_zero_of_forall_eq_zero

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ 0 = 0

σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
⊢ ∀ (x : σ →₀ ℕ), (coeff x) f • constantCoeff (x.prod fun s e ↦ a s ^ e) = 0
Module: Mathlib.Analysis.Real.Cardinality

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

Tactic:
have h2 : (fun x => a + a - x) '' Ioi a = Iio a := by
    convert! @image_const_sub_Ioi ℝ _ _ _
    simp

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
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
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
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd : ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d
⊢ ∑ᶠ (d_1 : σ →₀ ℕ), (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e) = 0

Tactic:
finsum_eq_zero_of_forall_eq_zero

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd : ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d
⊢ 0 = 0

σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd : ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d
⊢ ∀ (x : σ →₀ ℕ), (coeff x) f • (coeff d) (x.prod fun s e ↦ a s ^ e) = 0
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s

Tactic:
refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually ?_

Goal state after:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖

Tactic:
exact this.symm.mono fun n hn ↦ by simp [hn]

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

Goal state before:
pp: case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff n) ((X ^ k) ^ d) = 0

Tactic:
finsum_eq_zero_of_forall_eq_zero

Goal state after:
case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
⊢ 0 = 0

case neg
R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
⊢ ∀ (x : ℕ), (coeff x) f • (coeff n) ((X ^ k) ^ x) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
hφ : constantCoeff φ = 0
⊢ f.order ≤ order (subst f φ)

Tactic:
simp_rw [order_eq_order]

Goal state after:
R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
hφ : constantCoeff φ = 0
⊢ MvPowerSeries.order f ≤ (subst f φ).order
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a b : σ → R
⊢ rescaleAlgHom (a * b) = (rescaleAlgHom b).comp (rescaleAlgHom a)

Tactic:
by
  ext1 f
  simp [rescaleAlgHom_apply, rescale_rescale]

Goal state after:
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
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ tangentConeAt R s x

Tactic:
frequently_iff_neBot

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
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds✝ : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 | x + d x_1 ∈ s}).NeBot
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
this : Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0)
⊢ y ∈ tangentConeAt R s x
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 f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Tactic:
classical
  simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff 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✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
⊢ c ≠ 0

Tactic:
rintro rfl

Goal state after:
α : 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
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
hc : C < ‖0‖₊
⊢ False
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
l : Filter α
f : α → E
g : E →L[𝕜] F
hg : Topology.IsInducing ⇑g
⊢ comap (⇑↑g) (𝓝 0) ≤ 𝓝 0

Tactic:
by simp [hg.nhds_eq_comap]

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
⊢ (fun x ↦ (f x, g x)) =O[𝕜; l] k

Tactic:
by
  rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isBigOTVS_iff (basis_sets _)]
  rintro ⟨U, V⟩ ⟨⟨hU, hUb⟩, hV, hVb⟩
  rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets
    with ⟨W, hW, hWf, hWg⟩
  refine ⟨W, hW, ?_⟩
  filter_upwards [hWf, hWg] with x hfx hgx
  simp [egauge_prod_mk, *]

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✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousNeg E
h : (-f) =O[𝕜; l] g
⊢ f =O[𝕜; l] g

Tactic:
by simpa using h.neg_left

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✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousNeg E
h : (-f) =o[𝕜; l] g
⊢ f =o[𝕜; l] g

Tactic:
by simpa using h.neg_left

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
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun a ↦ ↑(‖p a‖₊ * r ^ a)

Tactic:
push_cast

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
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun a ↦ ‖p a‖ * ↑r ^ a
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ f.curryRight.uncurryRight = f

Tactic:
ext m

Goal state after:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n.succ) → Ei i
⊢ f.curryRight.uncurryRight m = f m
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : G [×0]→L[𝕜] G'
x : Fin 0 → G
⊢ uncurry0 𝕜 G (f x) = f

Tactic:
ext m

Goal state after:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : G [×0]→L[𝕜] G'
x m : Fin 0 → G
⊢ (uncurry0 𝕜 G (f x)) m = f m
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 : ContinuousMultilinearMap 𝕜 (fun x ↦ G) G'
⊢ f.currySum.uncurrySum = f

Tactic:
ext m

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 : ContinuousMultilinearMap 𝕜 (fun x ↦ G) G'
m : ι ⊕ ι' → G
⊢ f.currySum.uncurrySum m = f m