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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
this,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map ((fun y ↦ ↑y) ∘ fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y)))
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
⊢ ∃ π, v.IsUniformizer ↑π

Tactic:
by
  simp only [IsUniformizer.iff, Subtype.exists, mem_valuationSubring_iff, exists_prop]
  set g := (valueGroup (.ofClass v)).genLTOne with hg
  obtain ⟨⟨π, hπ⟩, hγ0⟩ : g.1 ∈ ((range (MonoidWithZeroHom.ofClass v)) \ {0}) := by
    rw [← valueGroup_eq_range, hg]
    exact mem_image_of_mem Units.val (valueGroup (.ofClass v)).genLTOne_mem
  use π
  simp only [MonoidWithZeroHom.coe_ofClass] at hπ
  rw [hπ, hg]
  exact ⟨le_of_lt (valueGroup (.ofClass v)).genLTOne_lt_one,
    by rw [valueGroup_genLTOne_eq_generator]⟩

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
this : v ↑↑u = 1
⊢ v ↑π₁ * v ↑↑u = ↑(generator v)

Tactic:
this,

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π₁ π₂ : ↥v.valuationSubring
h1 : v.IsUniformizer ↑π₁
u : (↥v.valuationSubring)ˣ
hu : π₁ * ↑u = π₂
this : v ↑↑u = 1
⊢ v ↑π₁ * 1 = ↑(generator v)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ addU (⇑f ∘ P) (⇑f ∘ Q) = f (addU P Q)

Tactic:
simp only [addU]
  map_simp

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

Goal state before:
pp: case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * ↑u
hn : ¬n = 0
hx_mem : maximalIdeal ↥v.valuationSubring ≤ P
⊢ Submodule.IsPrincipal P

Tactic:
← Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal K₀) hP.ne_top hx_mem

Goal state after:
case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * ↑u
hn : ¬n = 0
hx_mem : maximalIdeal ↥v.valuationSubring ≤ P
⊢ Submodule.IsPrincipal (maximalIdeal ↥v.valuationSubring)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha✝ : a ≠ 1
ha : 1 < a
⊢ Function.Injective fun x ↦ a ^ x

Tactic:
· exact (zpow_right_strictMono ha).injective

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : ¬x = 1
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : closure {x} = closure {x'}
hyc : closure {y} = closure {y'}
Hx : ∀ (z : ↥(closure {x})), z ∈ zpowers ⟨x', ⋯⟩
Hy : ∀ (z : ↥(closure {y})), z ∈ zpowers ⟨y', ⋯⟩
⊢ orderOf ⟨x', ⋯⟩ = orderOf ⟨y', ⋯⟩

Tactic:
rw [orderOf_mk, orderOf_mk]
      grind [orderOf_eq_one_iff, IsMulTorsionFree.orderOf_le_one]

Goal state after:
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
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ ↑a * ↑z₀⁻¹ ∈ V

Tactic:
this,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : ↑z₀⁻¹ = (↑z₀)⁻¹
⊢ ↑a * (↑z₀)⁻¹ ∈ V
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
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : v.restrict (a * z₀⁻¹) = 1
⊢ v.restrict (a * z₀⁻¹) * v.restrict z₀ = v.restrict z₀

Tactic:
this,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
nhds_right : (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
z₀ : K
y₀ : hat K
y₀_in : y₀ ∈ V'
hz₀ : ↑z₀ = y₀ * x₀
z₀_ne : z₀ ≠ 0
vz₀_ne : v.restrict z₀ ≠ 0
a : K
y : hat K
y_in : y ∈ V'
ha : ↑a = (fun x ↦ x * x₀) y
this : v.restrict (a * z₀⁻¹) = 1
⊢ 1 * v.restrict z₀ = v.restrict z₀
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
this,

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ({x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
this,

Goal state after:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ({x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < y
⊢ ∃ n, x ≤ y ^ n

Tactic:
replace hxy : 1 < e.symm y := by simp [← map_lt_map_iff e, hxy]

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CommMonoid β
inst✝¹ : PartialOrder β
e : α ≃*o β
inst✝ : MulArchimedean α
x y : β
hxy : 1 < e.symm y
⊢ ∃ n, x ≤ y ^ n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ (single s n, m - single s n) ∈ antidiagonal m

Tactic:
rwa [mem_antidiagonal, add_comm]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ ∑ p ∈ antidiagonal 1, (coeff p.1) φ * (coeff p.2) ψ = (coeff 1) φ * constantCoeff ψ + (coeff 1) ψ * constantCoeff φ

Tactic:
this,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ ψ : R⟦X⟧
this : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ ∑ p ∈ {(0, 1), (1, 0)}, (coeff p.1) φ * (coeff p.2) ψ = (coeff 1) φ * constantCoeff ψ + (coeff 1) ψ * constantCoeff φ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a✝ : σ
⊢ (single s n + (i, j).2 - single s n + single s n) a✝ = (single s n + (i, j).2) a✝

Tactic:
coe_add,

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a✝ : σ
⊢ (⇑(single s n + (i, j).2 - single s n) + ⇑(single s n)) a✝ = (single s n + (i, j).2) a✝
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a✝ : σ
⊢ (⇑(single s n + (i, j).2 - single s n) + ⇑(single s n)) a✝ = (single s n + (i, j).2) a✝

Tactic:
coe_add,

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a✝ : σ
⊢ (⇑(single s n + (i, j).2 - single s n) + ⇑(single s n)) a✝ = (⇑(single s n) + ⇑(i, j).2) a✝
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ v.intValuation r < 1 ↔ r ∈ v.asIdeal

Tactic:
intValuation_lt_one_iff_dvd,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
⊢ v.asIdeal ∣ Ideal.span {r} ↔ r ∈ v.asIdeal
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ (coeff d) (f ^ n) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f

Tactic:
this,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ (coeff d) (∏ x ∈ range n, f) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ (coeff d) (f ^ n) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f

Tactic:
by
    rw [this, coeff_prod]

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

Goal state before:
pp: case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv hv' : Irreducible (Associates.mk v)
⊢ Multiset.count ⟨Associates.mk v, hv⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv⟩ (Associates.factors' (Ideal.span {n}))

Tactic:
Associates.irreducible_mk,

Goal state after:
case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
v : Ideal R
hv✝ : Irreducible (Associates.mk v)
hv : Irreducible v
hv' : Irreducible (Associates.mk v)
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R := (MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f
this : f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g
⊢ ↑f = ↑g

Tactic:
this,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R := (MvPolynomial.uniqueAlgEquiv R PUnit.{1}).symm f
this : f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g
⊢ ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) g) = ↑g
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (MvPowerSeries.coeff m) ↑((monomial n) a) = (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a)

Tactic:
coeff_coe,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ coeff m ((monomial n) a) = (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case pos
σ : 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 : ↑((weight w) i) < weightedOrder w f
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0

Tactic:
coeff_eq_zero_of_lt_weightedOrder w hi,

Goal state after:
case pos
σ : 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 : ↑((weight w) i) < weightedOrder w f
⊢ 0 * (coeff (i, j).2) g = 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
this : ∀ {f' : MvPowerSeries σ R}, (coeff n) f' = MvPolynomial.coeff n ((trunc' R n) f')
⊢ (coeff n) f = (coeff n) g

Tactic:
this,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
this : ∀ {f' : MvPowerSeries σ R}, (coeff n) f' = MvPolynomial.coeff n ((trunc' R n) f')
⊢ MvPolynomial.coeff n ((trunc' R n) f) = MvPolynomial.coeff n ((trunc' R n) g)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
x✝¹ x✝ : σ →₀ ℕ
h : x✝ ≤ x✝¹
⊢ x✝¹ ∈ ↑⋯.toFinset → x✝ ∈ ↑⋯.toFinset

Tactic:
by simp; grind [degree_mono h]

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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 0) } = 0

Tactic:
by
  apply adicCompletion.ext; simp

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
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm 1) } = 1

Tactic:
by
  apply adicCompletion.ext; simp

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)ˣ
⊢ a ∈ (adicCompletionIntegers K v).units ↔ Valued.v ↑a = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦
     ⟨h.le, by simp [mem_adicCompletionIntegers, inv_le_one_iff₀, h.symm.le]⟩⟩

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)ˣ
h : a ∈ (adicCompletionIntegers K v).units
⊢ Valued.v ↑a = 1
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
this : (coeff n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0
⊢ (coeff n) (φ * ψ) = 0

Tactic:
this,

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
this : (coeff n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0
⊢ ∑ p ∈ antidiagonal n, 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
ha : x✝.1 < n
⊢ (coeff x✝.1) ↑((trunc n) f) * (coeff x✝.2) g = (coeff x✝.1) f * (coeff x✝.2) g

Tactic:
coeff_coe,

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
hab : x✝ ∈ antidiagonal m
ha : x✝.1 < n
⊢ ((trunc n) f).coeff x✝.1 * (coeff x✝.2) g = (coeff x✝.1) f * (coeff x✝.2) g
Module: Mathlib.RingTheory.PowerSeries.Trunc

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

Tactic:
coeff_coe,

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
h : n < m
⊢ (coeff n) ↑((trunc m) f) = (coeff n) f

Tactic:
coeff_coe,

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n m : ℕ
hm : n ≤ m
⊢ ↑n < (-X ^ (m + 1)).order

Tactic:
order_neg,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n m : ℕ
hm : n ≤ m
⊢ ↑n < (X ^ (m + 1)).order
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
φ : R →+* 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
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p
⊢ ε = ⇑(eval₂Hom hφ ha)

Tactic:
exact (toMvPowerSeries_isDenseInducing.extend_unique h hε).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
s : σ
⊢ (substAlgHom ha) (X s) = a s

Tactic:
by
  rw [← MvPolynomial.coe_X, substAlgHom_coe ha, MvPolynomial.aeval_X]

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

Goal state before:
pp: case neg
σ : 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 : σ →₀ ℕ
hd : ¬d = 0
this : constantCoeff (d.prod fun s e ↦ a s ^ e) = 0
⊢ (coeff d) f • constantCoeff (d.prod fun s e ↦ a s ^ e) = 0

Tactic:
this,

Goal state after:
case neg
σ : 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 : σ →₀ ℕ
hd : ¬d = 0
this : constantCoeff (d.prod fun s e ↦ a s ^ e) = 0
⊢ (coeff d) f • 0 = 0
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
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ {r : R}, h r = h.toAddMonoidHom r
⊢ h (∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff n) (d.prod fun s e ↦ a s ^ e)) =
    ∑ᶠ (d : σ →₀ ℕ), (coeff d) ((map h) f) • (coeff n) (d.prod fun s e ↦ (map h) (a s) ^ e)

Tactic:
this,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ {r : R}, h r = h.toAddMonoidHom r
⊢ h.toAddMonoidHom (∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff n) (d.prod fun s e ↦ a s ^ e)) =
    ∑ᶠ (d : σ →₀ ℕ), (coeff d) ((map h) f) • (coeff n) (d.prod fun s e ↦ (map h) (a s) ^ e)
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
n : τ →₀ ℕ
d : σ →₀ ℕ
hd : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ (coeff d) f • (coeff n) (d.prod fun s e ↦ 0 s ^ e) = 0

Tactic:
simp [Finsupp.prod, Finset.prod_eq_zero hi, coeff_zero, zero_pow <| d.mem_support_iff.mp hi]

Goal state after: