mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3
        · simp only [add_of_Y_eq hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]
        · simp only [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            nonsingular_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, nonsingular_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
⊢ ↑x ≠ 0

Tactic:
by
  have := x.prop
  rw [posSubmonoid_def] at this
  contrapose this
  simp [this]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : ValuativeRel R
⊢ supp R = (valuation R).supp

Tactic:
by
  ext
  simpa using valuation_eq_zero_iff.symm

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ ↑x + ↑y = ↑y + ↑x

Tactic:
rw [← coe_add, ← coe_add, add_comm]

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

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

Tactic:
one_mul

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ ↑a = ↑a
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH.negSucc
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n = n✝
⊢ ∃ a,
    ¬(MonoidWithZeroHom.ofClass v) a = 0 ∧
      ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.negSucc n) = (MonoidWithZeroHom.ofClass v) x

Tactic:
refine ⟨π ^ (n + 1), ?_, 1, ?_⟩ <;> simp [hπ, Int.negSucc_eq, mul_assoc]

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

Goal state before:
pp: case h
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = 1 * ↑r

Tactic:
one_mul

Goal state after:
case h
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = ↑r
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ - 1 * y⁻¹

Tactic:
one_mul

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ - y⁻¹
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: K : Type u_7
inst✝¹ : DivisionRing K
Γ₀ : Type u_8
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
γ : (ofClass v).ValueGroup₀ˣ
r : K
hr : (restrict₀ (ofClass v)) r = ↑γ
⊢ 0 < v r ∧ 0 < v 1 ∧ v.restrict r / v.restrict 1 = ↑γ

Tactic:
by
    simp only [map_one, zero_lt_one, restrict_def, hr, div_one, and_self, and_true]
    rw [← map_zero v]
    simpa [← hr] using embedding_strictMono (WithZero.pos_iff_ne_zero.mpr (Units.ne_zero γ))

Goal state after:
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ x < (↑z).unbot ⋯

pp: case refine_3
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ (↑z).unbot ⋯ < y

Tactic:
· rw [← WithBot.coe_lt_coe]
    simp [hz.trans_le]

Goal state after:
case refine_3
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ (↑z).unbot ⋯ < y
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_3
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ ↑((↑z).unbot ⋯) < ↑y

Tactic:
simp [hz'.trans_le']

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤᵒᵈ
H : (↑e).trans { toEquiv := toDual, map_add' := ⋯ } = AddEquiv.refl ℤ
⊢ False

Tactic:
replace H : e 1 = 1 := congr($H 1)

Goal state after:
e : ℤ ≃+o ℤᵒᵈ
H : e 1 = 1
⊢ False
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
⊢ 1 * v.restrict z₀ = v.restrict z₀

Tactic:
one_mul

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
⊢ v.restrict z₀ = v.restrict z₀
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) → Nonempty (G ≃+o ℤ)

Tactic:
intro h
    replace h : WellFounded (α := {x : G | 0 ≤ x}) (· < ·) := h
    rw [WellFounded.wellFounded_iff_has_min] at h
    by_cases! H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y -- Archimedean
    · replace H : Archimedean G := ⟨H⟩
      rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]
      intro hd
      obtain ⟨y, hy⟩ := exists_ne (0 : G)
      wlog! hy' : 0 < y generalizing y
      · refine this (-y) ?_ ?_
        · simp [hy]
        · simp [lt_of_le_of_ne hy' hy]
      obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩
      obtain ⟨w, hw, hw'⟩ := exists_between hz'
      exact hz'' ⟨w, hw.le⟩ hw hw'
    · exfalso
      obtain ⟨x, y, hy0, H⟩ := H
      obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)
      refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_
      simp [add_smul, hy0]

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
⊢ extension x = 0 ↔ x = 0

Tactic:
by
  suffices extensionValuation x = 0 ↔ x = 0 by
    simpa only [extensionValuation_toFun, map_eq_zero]
  rw [Valuation.zero_iff]

Goal state after:
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
⊢ Nonempty (G₀ˣ ≃*o Multiplicative ℤ) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Tactic:
refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)

Goal state after:
case refine_1
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
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ G₀ ≃* WithZero (Multiplicative ℤ)

case refine_2
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
f : G₀ˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : G₀}, (MulEquiv.toEquiv ?refine_1).toFun a ≤ (MulEquiv.toEquiv ?refine_1).toFun b ↔ a ≤ b

case refine_3
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ G₀ˣ ≃* Multiplicative ℤ

case refine_4
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
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ}, (MulEquiv.toEquiv ?refine_3).toFun a ≤ (MulEquiv.toEquiv ?refine_3).toFun b ↔ a ≤ b
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 Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : v s / v r ≠ 0
⊢ closure (Completion.coe' '' {x | v x * v r < v s}) = {x | extensionValuation x * v r < v s}

Tactic:
convert! closure_coe_completion_v_lt (γ := .mk0 _ hrs) using 3

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : v s / v r ≠ 0
⊢ {x | v x * v r < v s} = {x | v x < ↑(Units.mk0 (v s / v r) hrs)}

case e'_3
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : v s / v r ≠ 0
x✝ : hat K
⊢ extensionValuation x✝ * v r < v s ↔ extensionValuation x✝ < ↑(Units.mk0 (v s / v r) hrs)
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
h : α → β
inst✝¹ : LinearOrder β
inst✝ : Northcott h
s : Set α
hs : s.Nonempty
⊢ ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'

Tactic:
obtain ⟨a₁, h₁⟩ := hs
  obtain ⟨a₂, h₂, h₃⟩ := Set.exists_min_image ({a | h a ≤ h a₁} ∩ s) h
    ((finite_le (h a₁)).inter_of_left s) ⟨a₁, le_rfl, h₁⟩
  grind

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (coeff m) ((monomial n) a) = if m = n then a else 0

Tactic:
dsimp only [coeff, MvPowerSeries]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
m n : σ →₀ ℕ
a : R
⊢ (LinearMap.proj m) ((monomial n) a) = if m = n then a else 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m = n then a else 0) = (coeff m) (mk fun m ↦ if m = n then a else 0)

Tactic:
coeff_mk

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (if m = n then a else 0) = if m = n then a else 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () n)) φ = 1 * (MvPowerSeries.coeff (single () n)) φ

Tactic:
one_mul

Goal state after:
case e'_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (MvPowerSeries.coeff (single () n)) φ = (MvPowerSeries.coeff (single () n)) φ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ 1 * (coeff (n, d).2) p = (coeff d) p

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

pp: case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff (n, d).2) p = (coeff d) p

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

case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff (n, d).1) (X ^ n) * (coeff (n, d).2) p = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ a * b = 0

Tactic:
rw [← h₂, tsub_add_cancel_of_le h₁] at h₃
    exact (h₃ rfl).elim

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
⊢ (monomial (single s n)) 1 * X s = (monomial (single s (n + 1))) 1

Tactic:
Finsupp.single_add,

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
⊢ (monomial (single s n)) 1 * X s = (monomial (single s n + single s 1)) 1
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
⊢ (monomial (single s n + single s 1)) (1 * 1) = (monomial (single s n + single s 1)) 1

Tactic:
one_mul

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
⊢ (monomial (single s n + single s 1)) 1 = (monomial (single s n + single s 1)) 1
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
n : ℕ
⊢ ↑((coeff n) (mk fun n ↦ ⟨(coeff n) p, ⋯⟩)) = (coeff n) p

Tactic:
coeff_mk

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
n : ℕ
⊢ ↑⟨(coeff n) p, ⋯⟩ = (coeff n) p
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ a ^ n✝ * f n✝ = (coeff n✝) (mk fun n ↦ a ^ n * f n)

Tactic:
coeff_mk

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → R
a : R
n✝ : ℕ
⊢ a ^ n✝ * f n✝ = a ^ n✝ * f n✝
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
⊢ (coeff m) φ = 1 * (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ

Tactic:
one_mul

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
⊢ (coeff m) φ = (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ v.intValuation x ≠ 0

Tactic:
v.intValuation_if_neg hx

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)) ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : d = 0
⊢ 1 = ↑(#{0})

pp: case neg
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ 0 = ↑(#∅)

Tactic:
· simp only [card_singleton, Nat.cast_one]

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ 0 = ↑(#∅)
Module: Mathlib.RingTheory.MvPowerSeries.Order

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

Tactic:
constructor
  · intro h
    obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by simp only [h, toNat_natCast])
    exact ⟨⟨d, by simpa [h, Nat.cast_inj, ne_eq] using hd⟩,
      fun e he ↦ f.coeff_eq_zero_of_lt_weightedOrder w (by simp only [h, Nat.cast_lt, he])⟩
  · rintro ⟨⟨d, hd', hd⟩, h⟩
    exact le_antisymm (hd.symm ▸ f.weightedOrder_le w hd') (nat_le_weightedOrder w h)

Goal state after:
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ f i = 0 ↔ ¬{f i} ≠ 0

Tactic:
not_ne_iff

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ f i = 0 ↔ {f i} = 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ f i = 0 ∧ g i = 0 ↔ ¬Icc (f i) (g i) ≠ 0

Tactic:
not_ne_iff

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Zero α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq ι
f✝ g✝ : ι →₀ α
i✝ : ι
a : α
f g : ι →₀ α
i : ι
⊢ f i = 0 ∧ g i = 0 ↔ Icc (f i) (g i) = 0
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsBotZeroClass α
inst✝³ : OrderBot α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f : ι →₀ α
⊢ #(Iic f) - 1 = ∏ i ∈ f.support, #(Iic (f i)) - 1

Tactic:
card_Iic

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsBotZeroClass α
inst✝³ : OrderBot α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f : ι →₀ α
⊢ ∏ i ∈ f.support, #(Iic (f i)) - 1 = ∏ i ∈ f.support, #(Iic (f i)) - 1
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)

Tactic:
apply le_weightedOrder
  intro d hd
  rw [coeff_mul, Finset.sum_eq_zero]
  rintro ⟨i, j⟩ hij
  by_cases! hi : weight w i < f.weightedOrder w
  · rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
  · 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.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n n✝ : ℕ
⊢ (coeff n✝) ((monomial n) r) = (coeff n✝) (C r * X ^ n)

Tactic:
simp [coeff_X_pow, coeff_monomial]

Goal state after:
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✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, (eval₂Hom φ a) x ∈ ↑I

Tactic:
have hn : Set.Finite (n.support) := by
    change n =ᶠ[cofinite] 0
    filter_upwards [ha.tendsto_zero.eventually_mem hI] with s has
    simpa [n, Pi.zero_apply, Nat.sInf_eq_zero, or_iff_left (hn_ne s).ne_empty] using has

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
⊢ ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, (eval₂Hom φ a) x ∈ ↑I
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
p : MvPolynomial σ R
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ subst a ↑p = (MvPolynomial.aeval a) p

Tactic:
subst_eq_eval₂,

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
p : MvPolynomial σ R
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ eval₂ (algebraMap R (MvPowerSeries τ S)) a ↑p = (MvPolynomial.aeval a) p
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ Summable fun n ↦ ‖↑C * (↑n ^ (s + (1 - ↑x)))⁻¹‖

Tactic:
norm_mul,

Goal state after:
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
⊢ Summable fun n ↦ ‖↑C‖ * ‖(↑n ^ (s + (1 - ↑x)))⁻¹‖