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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) 0 = ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)

Tactic:
update_self

Goal state after:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ) = ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.addX P Q / addZ P Q ^ 2 =
    W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
rw [addX_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
    toAffine_addX_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : DivisionRing K
inst✝ : ValuativeRel K
a : K
⊢ 0 =ᵥ a ↔ 0 = a

Tactic:
by
  rw [veq_comm, eq_comm, zero_veq_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑(a * (b + c)) = ↑(a * b + a * c)

Tactic:
mul_add

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑(a * b + a * c) = ↑(a * b + a * c)
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ {0}ᶜ ⊆ {y | y.hatInv = y⁻¹}

Tactic:
intro y y_ne
          rw [mem_compl_singleton_iff] at y_ne
          dsimp [Inv.inv]
          rw [if_neg y_ne]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
⊢ UniformContinuous ⇑(equiv v).symm

Tactic:
refine uniformContinuous_of_continuousAt_zero _ ?_
  simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]
  intro γ
  obtain ⟨r, s, hr₀, hs₀, hr⟩ := exists_div_eq_of_unit Valued.v γ
  have h' : w.restrict.IsEquiv v.restrict := h.restrict
  use .mk0 ((Valued.v.restrict ((WithVal.equiv v) r)) /
    (Valued.v.restrict ((WithVal.equiv v) s))) (by
    simp only [equiv_apply, restrict_def, ne_eq, div_eq_zero_iff, restrict₀_eq_zero_iff, hv,
      MonoidWithZeroHom.coe_ofClass, not_or, (eq_zero h (r := r.ofVal)).ne,
      (eq_zero h (r := s.ofVal)).ne]
    exact ⟨hr₀.ne', hs₀.ne'⟩)
  intro x hx
  simp only [equiv_symm_apply, Set.mem_ofPred_eq]
  simp only [equiv_apply, Units.val_mk0, Set.mem_ofPred_eq] at hx
  rw [lt_div_iff₀, ← map_mul, restrict_lt_iff, hv, h.lt_iff_lt, map_mul] at hx
  · rw [← hr, lt_div_iff₀ ((restrict_pos_iff Valued.v s).mpr hs₀), ← map_mul, ← lt_def,
      ← h.orderRingIso_apply]
    simp only [orderRingIso_apply, toVal_mul, lt_def, ofVal_mul, restrict_lt_iff]
    rw [map_mul]
    exact hx
  · rw [restrict_pos_iff, hv, h.pos_iff]
    exact hs₀

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 0)) (𝓝 c)

pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)

Tactic:
· refine ⟨0, ?_⟩
    rw [← Completion.coe_zero, ← Completion.isDenseInducing_coe.isInducing.nhds_eq_comap]
    exact Valued.continuous_valuation.tendsto' 0 0 (map_zero v.restrict)

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ v 1 ≠ 0

Tactic:
rw [Valuation.map_one]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ 1 ≠ 0
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∃ x, IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

pp: case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Tactic:
· obtain ⟨x, hx⟩ := H
    exact Or.inl ⟨(int_orderAddMonoidIso_of_isLeast_pos hx)⟩

Goal state after:
case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
H : ∀ (x : G), ¬IsLeast {y | 0 < y} x
⊢ Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
m : ℕ
a : R
n : ℕ
⊢ (monomial m) a ^ n = (monomial (n * m)) (a ^ n)

Tactic:
by
  simpa [monomial] using MvPowerSeries.monomial_pow (Finsupp.single () m) a n

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Injective ⇑valueGroup₀_hom_extensionValuation

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑valueGroup₀_hom_extensionValuation

Tactic:
· intro a b hab
    set x := (restrict₀_surjective (.ofClass hv.v) a).choose with hx_def
    have hx := (restrict₀_surjective (.ofClass hv.v) a).choose_spec
    set y := (restrict₀_surjective (.ofClass hv.v) b).choose with hy_def
    have hy := (restrict₀_surjective (.ofClass hv.v) b).choose_spec
    apply_fun embedding using embedding_injective
    apply_fun embedding at hx
    apply_fun embedding at hy
    simp only [← hx_def, embedding_restrict₀, coe_ofClass, ← hy_def] at hx hy
    simp only [valueGroup₀_hom_extensionValuation, coe_mk, ZeroHom.coe_mk] at hab
    have : hv.extensionValuation.restrict (algebraMap K _ x) =
       hv.extensionValuation.restrict (algebraMap _ _ y) := hab
    simp only [Valuation.restrict_def, restrict₀_apply, extensionValuation_coe_apply, map_eq_zero,
      extension_eq_zero_iff] at this
    by_cases ha0 : a = 0
    · have h0 : extension ((algebraMap K (hat K)) x) = 0 := by
        simpa [ha0, extension_eq_zero_iff, map_eq_zero] using hx
      simp [h0, reduceDIte, extension_eq_zero_iff, map_eq_zero,
        left_eq_dite_iff, WithZero.zero_ne_coe, imp_false, not_not] at this
      simp [ha0, ← hy, this]
    · apply_fun embedding at ha0 using embedding_injective (f := (.ofClass hv.v))
      have h0 : extension ((algebraMap K (hat K)) x) ≠ 0 := by
        simp only [ne_eq, extension_eq_zero_iff, map_eq_zero]
        intro h
        simp [h, ← hx] at ha0
      have h0' : extension ((algebraMap K (hat K)) y) ≠ 0 := by
        have hb0 : b ≠ 0 := by
          apply_fun embedding at hab using embedding_injective (f := (.ofClass hv.v))
          simp only [← hx_def, Valuation.embedding_restrict, extensionValuation_apply_coe,
            ← hy_def] at hab
          simpa [← hx, hab, hy] using ha0
        apply_fun embedding at hb0 using embedding_injective (f := (.ofClass hv.v))
        simp only [ne_eq, extension_eq_zero_iff, map_eq_zero]
        intro h
        simp [h, ← hy] at hb0
      simp only [map_eq_zero, h0, reduceDIte, h0', WithZero.coe_inj, Subtype.mk.injEq,
        Units.mk0_inj, embedding_inj] at this
      simp only [Completion.algebraMap_def, Algebra.algebraMap_self, RingHom.id_apply,
        extension_extends, Valuation.restrict_inj] at this
      rwa [← hx, ← hy]

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ Function.Surjective ⇑valueGroup₀_hom_extensionValuation
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ v.intValuation r ≤ exp (-↑n) ↔ r ∈ v.asIdeal ^ n

Tactic:
rw [intValuation_le_pow_iff_dvd, Ideal.dvd_span_singleton]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ ∃ π, v.intValuation π = exp (-1)

Tactic:
have hlt : v.asIdeal ^ 2 < v.asIdeal := by
    rw [← Ideal.dvdNotUnit_iff_lt]
    exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
⊢ ∃ π, v.intValuation π = exp (-1)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ.inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : n' = 0
⊢ constantCoeff φ ^ n' * (coeff 1) φ + (coeff 1) (φ ^ n') * constantCoeff φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
by_contra h''
          rw [h'] at h''
          simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero,
            mul_one] at h''
          norm_num at h''

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = ↑1

Tactic:
Int.natCast_inj

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
⊢ v.intValuation x = 1 ↔ x ∉ v.asIdeal

Tactic:
refine ⟨fun h ↦ by simp [← (intValuation_lt_one_iff_mem _ _).not, h], fun h ↦ ?_⟩
  exact le_antisymm (v.intValuation_le_one x) <| by
    simp [← not_lt, (v.intValuation_lt_one_iff_mem _).not, h]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1) * constantCoeff φ * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
enter [

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1) * constantCoeff φ * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1 + 1) * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'

Tactic:
enter [

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + constantCoeff φ ^ (n' - 1 + 1) * ↑n' * (coeff 1) φ =
    (↑n' + 1) * (coeff 1) φ * constantCoeff φ ^ n'
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
this : ∀ (a : A) (f : MvPowerSeries σ R), a • f = MvPowerSeries.C ((algebraMap A R) a) * f
⊢ (e.prod fun a_1 b ↦ MvPowerSeries.C ((algebraMap A R) (a a_1 ^ b))) * (MvPowerSeries.monomial e) 1 =
    MvPowerSeries.C ((algebraMap A R) (e.prod fun s n ↦ a s ^ n)) * (MvPowerSeries.monomial e) 1

Tactic:
simp only [map_finsuppProd, map_pow]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = e.prod fun s e ↦ (r s • MvPowerSeries.X s) ^ e

Tactic:
MvPowerSeries.prod_smul_X_eq_smul_monomial_one,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : σ → R
⊢ (MvPowerSeries.monomial e) (e.prod fun s n ↦ r s ^ n) = (e.prod fun s n ↦ r s ^ n) • (MvPowerSeries.monomial e) 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = e.prod fun s e ↦ (r • MvPowerSeries.X s) ^ e

Tactic:
MvPowerSeries.prod_smul_X_eq_smul_monomial_one,

Goal state after:
σ : Type u_4
R : Type u_5
inst✝ : CommSemiring R
e : σ →₀ ℕ
r : R
⊢ (MvPowerSeries.monomial e) (r ^ e.sum fun x n ↦ n) = (e.prod fun s n ↦ r ^ n) • (MvPowerSeries.monomial e) 1
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) → ∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f

Tactic:
refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x ↦ f i) = f
Module: Mathlib.Data.Finset.Finsupp

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι →₀ Finset α
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i ↦ ↑(#(f i))

Tactic:
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
s : Finset (σ →₀ ℕ)
inst✝ : DecidableEq σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
⊢ MvPolynomial.coeff x ((truncFinset R s) p) = if x ∈ s then (coeff x) p else 0

Tactic:
by
  simp [truncFinset_apply, MvPolynomial.coeff_sum]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ Finset.antidiagonal d
hi : weightedOrder w f ≤ ↑((weight w) i)
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0

Tactic:
· by_cases! hj : weight w j < g.weightedOrder w
    · rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
    · simp only [Finset.mem_antidiagonal] at hij
      exfalso
      apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
      rw [← hij, map_add, Nat.cast_add]

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih : (truncFinset R s) (↑((truncFinset R s) p) ^ n) = (truncFinset R s) (p ^ n)
x : σ →₀ ℕ
hx : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) (p ^ n) * (truncFinset R s) p) = (coeff x) (p ^ n * p)

Tactic:
coeff_truncFinset_mul_truncFinset_eq_coeff_mul hs _ _ hx

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
k : ℕ
p : MvPowerSeries σ R
n : ℕ
hmn : 1 ≤ n
ih : (truncFinset R s) (↑((truncFinset R s) p) ^ n) = (truncFinset R s) (p ^ n)
x : σ →₀ ℕ
hx : x ∈ s
⊢ (coeff x) (p ^ n * p) = (coeff x) (p ^ n * p)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.1 < p
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0

pp: case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.2 < q
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0

Tactic:
· rw [if_neg (ne_of_lt h), zero_mul]
      rw [← ENat.natCast_lt_natCast] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]

Goal state after:
case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.2 < q
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: 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
inst✝⁴ : Algebra S K
S₀ : Type u_4
inst✝³ : CommSemiring S₀
inst✝² : Algebra S₀ S
inst✝¹ : Algebra S₀ K
inst✝ : IsScalarTower S₀ S K
x : S₀
⊢ (algebraMap S₀ (adicCompletion K v)) x = (algebraMap S (adicCompletion K v)) ((algebraMap S₀ S) x)

Tactic:
apply adicCompletion.ext
    rw [algebraMap_adicCompletion_toCompletion, algebraMap_adicCompletion_toCompletion,
      IsScalarTower.algebraMap_apply S₀ S ((v.valuation K).Completion)]

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I

Tactic:
have hRR : uR * uR ⊆ uR := subset_univ _

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hφ : φ ≠ 0
⊢ φ.order = ↑n ↔ (coeff n) φ ≠ 0 ∧ ∀ i < n, (coeff i) φ = 0

Tactic:
simp [order, dif_neg hφ, Nat.find_eq_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i ↦ (MvPowerSeries.coeff d) (f i)) u (𝓝 ((MvPowerSeries.coeff d) g)) ↔
    Tendsto (fun i ↦ (MvPowerSeries.coeff (Finsupp.single () (d ()))) (f i)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () (d ()))) g))

Tactic:
apply iff_of_eq

Goal state after:
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (fun i ↦ (MvPowerSeries.coeff d) (f i)) u (𝓝 ((MvPowerSeries.coeff d) g)) =
    Tendsto (fun i ↦ (MvPowerSeries.coeff (Finsupp.single () (d ()))) (f i)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () (d ()))) g))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ ↑φ.order.toNat + ↑ψ.order.toNat

Tactic:
← ENat.natCast_add

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ ↑(φ.order.toNat + ψ.order.toNat)
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
⊢ ⇑(substAlgHom ha) = ⇑(aeval ⋯)

Tactic:
simp only [substAlgHom, coe_aeval ha.hasEval]
  convert! coe_aeval (R := R) (hasSubst_iff_hasEval_of_discreteTopology.mp ha) <;>
  exact DiscreteUniformity.eq_bot.symm

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : ¬1 < q
⊢ (ofPowerSeries (q ^ k)) f = (ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)

Tactic:
simp [ofPowerSeries, hq, hk]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)

Tactic:
have hn' : 0 < n := Nat.pos_of_ne_zero hn₀

Goal state after:
case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ ‖f n‖ ≤ C' * ↑n ^ (x - 1)