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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
a b c : ValueGroupWithZero R
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
induction a using ValueGroupWithZero.ind with

Goal state after:
case mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
b c : ValueGroupWithZero R
hbc : b ≤ c
a₁ : R
a₂ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk a₁ a₂ ≤ b
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ c
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x✝ : R
h : x✝ ∈ {x | x ≤ᵥ 0}
⊢ x • x✝ ∈ {x | x ≤ᵥ 0}

Tactic:
simpa using mul_vle_mul_right h _

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
hx' : x ≠ 0
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
exact Filter.Tendsto.cauchy_map <|
      calc
        map (fun x => x⁻¹) F ≤ map (fun x => x⁻¹) (𝓝 x) := map_mono hx
        _ ≤ 𝓝 x⁻¹ := continuousAt_inv₀ hx'

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

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ v π ≠ 0

Tactic:
by_contra h0

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : v π = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).negY (⇑f ∘ P) = f (W'.negY P)

Tactic:
simp only [negY]
  map_simp

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

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A)) ((algebraMap A K) ↑u) *
      (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n) * ((algebraMap A K) (π ^ m) * (algebraMap A K) ↑w)⁻¹) ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
Integers.one_of_isUnit' u.isUnit (valuation_le_one _),

Goal state after:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  1 * (valuation K (maximalIdeal A)) ((algebraMap A K) (π ^ n) * ((algebraMap A K) (π ^ m) * (algebraMap A K) ↑w)⁻¹) ≤ 1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithTop X)
he : StrictAnti ⇑(WithTop.toDual.image s)
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
rw [denselyOrdered_iff_of_strictAnti _ he, WithBot.denselyOrdered_set_iff_subsingleton,
    WithTop.toDual.injective.subsingleton_image_iff]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: 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
⊢ ↥(closure {x}) ≃*o ↥(closure {y})

Tactic:
refine ⟨⟨⟨fun _ ↦ ⟨1, by simp [hxy.mp hx]⟩, fun _ ↦ ⟨1, by simp [hx]⟩, ?_, ?_⟩, ?_⟩, ?_⟩

Goal state after:
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
⊢ Function.LeftInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

case refine_2
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
⊢ Function.RightInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

case refine_3
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_1 y_1 : ↥(closure {x})),
    { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2 }.toFun
        (x_1 * y_1) =
      { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2 }.toFun
          x_1 *
        { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2 }.toFun
          y_1

case refine_4
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
⊢ ∀ {a b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          a ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          b ↔
      a ≤ b
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
⊢ Function.LeftInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

Tactic:
intro ⟨a, ha⟩
      simpa [hx, closure_singleton_one, eq_comm] using ha

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

Goal state before:
pp: case inr
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
⊢ Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 (v.restrict z₀))

Tactic:
rw [WithZeroTopology.tendsto_of_ne_zero vz₀_ne, eventually_comap]

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
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
⊢ ∀ᶠ (b : hat K) in 𝓝 x₀, ∀ (a : K), ↑a = b → v.restrict a = v.restrict z₀
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
h : γ₀ ≠ 0
h' : γ₀' ≠ 0
hγ₀ : extension ⁻¹' {γ₀'} ∈ 𝓝 x
hx : γ₀ < ↑γ
s : Set (hat K)
hs : s ∈ 𝓝 x
⊢ ∃ y, ↑y ∈ s

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := Completion.denseRange_coe.mem_nhds (inter_mem hγ₀ hs)
    replace hy₁ : v y = γ₀ := by
      simp only [mem_preimage, extension_extends, mem_singleton_iff, v.restrict_def] at hy₁
      apply_fun embedding at hy₁
      simpa [heq] using hy₁
    rw [← hy₁] at hx
    exact ⟨⟨y, ⟨y, hx, rfl⟩⟩, hy₂⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ (MvPowerSeries.coeff n) φ = (MvPowerSeries.coeff n) ψ

Tactic:
rw [← coeff_def]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ (coeff ?m.21) φ = (coeff ?m.21) ψ

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.21

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ ℕ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff b.1) (X ^ n) * (coeff b.2) p = 0

Tactic:
rintro ⟨i, j⟩ h1 h2
    rw [coeff_X_pow, if_neg, zero_mul]
    rintro rfl
    apply h2
    rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1
    subst h1
    rfl

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = (monomial (single s n)) 1
⊢ X s ^ (n + 1) = (monomial (single s (n + 1))) 1

Tactic:
pow_succ,

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = (monomial (single s n)) 1
⊢ X s ^ n * X s = (monomial (single s (n + 1))) 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : (coeff (single s 1)) (X s) = (coeff (single s 1)) (X t)
⊢ s = t

Tactic:
rw [coeff_X, if_pos rfl, coeff_X] at h

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = if single s 1 = single t 1 then 1 else 0
⊢ s = t
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 Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h0' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding a = embedding b

Tactic:
simp only [map_eq_zero, h0, reduceDIte, h0', WithZero.coe_inj, Subtype.mk.injEq,
        Units.mk0_inj, embedding_inj] at this

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h0' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding a = embedding b
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)
⊢ DvdNotUnit v.asIdeal (v.asIdeal ^ 2)

Tactic:
exact ⟨v.ne_bot, v.asIdeal, Ideal.isUnit_iff.not.mpr v.isPrime.ne_top, sq v.asIdeal⟩

Goal state after:
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) (∏ x ∈ range n, f) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f

Tactic:
coeff_prod

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
⊢ ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f =
    ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f
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
⊢ ∃ π, (valuation K v) ↑π = exp (-1)

Tactic:
by
  have ⟨π, hπ⟩ := intValuation_exists_uniformizer v
  use π
  grind [valuation_of_algebraMap]

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
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ k i = 0

Tactic:
hi.2

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
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ 0 = 0
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
⊢ (coeff x) (↑((truncFinset R s) p) ^ (n + 1)) = (coeff x) (p ^ (n + 1))

Tactic:
pow_succ,

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) (↑((truncFinset R s) p) ^ n * ↑((truncFinset R s) p)) = (coeff x) (p ^ (n + 1))
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)
hj : weightedOrder w g ≤ ↑((weight w) j)
⊢ (coeff (i, j).1) f * (coeff (i, j).2) g = 0

Tactic:
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 + 1))

Tactic:
pow_succ,

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
⊢ MvPolynomial.coeff x ((truncFinset R s) (p ^ n) * (truncFinset R s) p) = (coeff x) (p ^ n * p)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
⊢ n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))

Tactic:
pow_succ,

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
⊢ n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
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 : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff d) ((f * ∏ x ∈ s, (1 - g x)) * (1 - g a)) = (coeff d) f

Tactic:
coeff_mul_left_one_sub_of_lt_weightedOrder w h.1,

Goal state after:
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 : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff d) (f * ∏ x ∈ s, (1 - g x)) = (coeff d) f
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
⊢ ↑(ofClass (valuation K v)).valueGroup = ↑(ofClass Valued.v).valueGroup

Tactic:
by rw [valueGroup_eq K v]

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

Goal state before:
pp: ⊢ Tendsto Nat.cast atTop (𝓝 ⊤)

Tactic:
by
  rw [tendsto_nhds_top_iff_natCast_lt]
  intro n
  filter_upwards [eventually_ge_atTop (n + 1)] with a ha using by simpa

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
r : R
⊢ { toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) r)) } ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers]
  change Valued.v (↑((algebraMap R K) r) : adicCompletion K v).toCompletion ≤ 1
  rw [Valued.valuedCompletion_apply]
  simpa using v.valuation_le_one _

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : ¬φ = 0
⊢ ↑n ≤ ↑(Nat.find ⋯)

Tactic:
· simpa [Nat.le_find_iff]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ n • φ.order + φ.order ≤ (φ ^ (n + 1)).order

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
ih : n • φ.order ≤ (φ ^ n).order
⊢ n • φ.order + φ.order ≤ (φ ^ n * φ).order
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r < 1 ↔ r ∈ v.asIdeal

Tactic:
by
  simpa [intAdicAbv, intAdicAbvDef, toNNReal_lt_one_iff hb] using intValuation_lt_one_iff_mem v r

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
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r = 1 ↔ r ∉ v.asIdeal

Tactic:
by
  contrapose
  rw [← v.intAdicAbv_lt_one_iff hb, ne_iff_lt_iff_le]
  exact intAdicAbv_le_one v hb r

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

Goal state before:
pp: S : Type u_3
inst✝ : CommRing S
a : S
t u : TopologicalSpace S
h : t ≤ u
ha : HasEval a
⊢ HasEval a

Tactic:
simp only [hasEval_iff] at ha ⊢

Goal state after:
S : Type u_3
inst✝ : CommRing S
a : S
t u : TopologicalSpace S
h : t ≤ u
ha : MvPowerSeries.HasEval fun x ↦ a
⊢ MvPowerSeries.HasEval fun x ↦ a
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
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
hφ : Continuous ⇑φ
a : R
ha : HasEval a
⊢ HasEval (φ a)

Tactic:
simp only [hasEval_iff] at ha ⊢

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
hφ : Continuous ⇑φ
a : R
ha : MvPowerSeries.HasEval fun x ↦ a
⊢ MvPowerSeries.HasEval fun x ↦ φ a
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
f : MvPowerSeries σ R
⊢ Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] ⇑(eval₂Hom hφ ha)

Tactic:
rw [coe_eval₂Hom]; exact continuous_eval₂ hφ ha

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
f g : MvPowerSeries σ R
⊢ subst a (f + g) = subst a f + subst a g

Tactic:
simp only [← substAlgHom_apply ha, map_add]

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

Goal state before:
pp: case pos
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : n = 0
⊢ 0 = f n * ↑n ^ (-s)

Tactic:
simp [h, hf, cpow_neg, div_eq_inv_mul, mul_comm]

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

Goal state before:
pp: case neg
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : ¬n = 0
⊢ f n / ↑n ^ s = f n * ↑n ^ (-s)

Tactic:
simp [h, hf, cpow_neg, div_eq_inv_mul, mul_comm]

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

Goal state before:
pp: f g : ℕ → ℂ
s a : ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
⊢ LSeriesHasSum f s a ↔ LSeriesHasSum g s a

Tactic:
simp [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr h s]

Goal state after: