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

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
inst✝³ : LinearOrderedCommGroupWithZero Γ
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
inst✝ : DecidablePred fun x ↦ x = 0
x : ↥(posSubmonoid R)
⊢ ↑x ≠ 0

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
⊢ (match 1 with
    | ⟨a, ha⟩ => ⟨(algebraMap A B) a, ⋯⟩) =
    1

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : ValuativeRel A
inst✝² : ValuativeRel B
inst✝¹ : Algebra A B
inst✝ : ValuativeExtension A B
⊢ ∀ (x y : ↥(posSubmonoid A)),
    (match x * y with
      | ⟨a, ha⟩ => ⟨(algebraMap A B) a, ⋯⟩) =
      (match x with
        | ⟨a, ha⟩ => ⟨(algebraMap A B) a, ⋯⟩) *
        match y with
        | ⟨a, ha⟩ => ⟨(algebraMap A B) a, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negY ![W'.addX P P, W'.negAddY P P, addZ P P] = 0

Tactic:
negY_eq,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -W'.negAddY P P - W'.a₁ * W'.addX P P * addZ P P - W'.a₃ * addZ P P ^ 3 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negY ![W'.addX P Q, W'.negAddY P Q, addZ P Q] = (P x * Q z) ^ 3 * Q y

Tactic:
negY_eq,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3 = (P x * Q z) ^ 3 * Q y
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst✝¹ : Field K
w : Valuation K Γ
inst✝ : w.IsRankOneDiscrete
⊢ generator w ∈ ↑(zpowers (generator w)) ∧ ↑(generator w) = ↑(generator w)

Tactic:
by simp

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 Γ
inst✝ : v.IsRankOneDiscrete
⊢ ↑(generator v) ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.negY ![W'.addX P Q, W'.negAddY P Q, addZ P Q] = (-(Q x * P z)) ^ 3 * P y

Tactic:
negY_eq,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3 = (-(Q x * P z)) ^ 3 * P y
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 Γ
inst✝ : v✝.IsRankOneDiscrete
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
⊢ exp (-1) ≠ 0

Tactic:
by simp

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

Goal state before:
pp: A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
⊢ exp (-1) ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.negY ![W'.addX P Q, W'.negAddY P Q, addZ P Q] * (P z * Q z) ^ 3 + W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    0

Tactic:
negY_eq,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3) * (P z * Q z) ^ 3 +
        W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    0
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 Γ
inst✝ : v✝.IsRankOneDiscrete
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
⊢ exp (-1) ≠ 0

Tactic:
by simp

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 ↑(π₁ * ↑u) = ↑(generator v)

Tactic:
Subring.coe_mul,

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 (↑π₁ * ↑↑u) = ↑(generator v)
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
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
⊢ 0 ≤ m

Tactic:
rw [← zpow_le_one_iff_right_of_lt_one₀ π.2.val_pos π.2.val_lt_one, hm']

Goal state after:
Γ : 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
⊢ v ↑r ≤ 1
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : Ring S
Λ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R ≃+* S
x✝ : WithVal v
⊢ (map w v f.symm.toRingHom) ((↑↑(map v w f.toRingHom)).toFun x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝¹ : Ring S
Λ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
f : R ≃+* S
x✝ : WithVal w
⊢ (↑↑(map v w f.toRingHom)).toFun ((map w v f.symm.toRingHom) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
inst✝³ : Ring R
v : Valuation R Γ₀
S : Type u_3
inst✝² : Ring S
Λ₀ : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Λ₀
w : Valuation S Λ₀
inst✝ : CharZero R
⊢ (equiv v).symm.toAddMonoidHom 1 = 1

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Ring R
Γ'₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation R Γ₀
w : Valuation R Γ'₀
x : WithVal v
⊢ (congr v w (RingEquiv.refl R)) x = (equiv w).symm ((equiv v) x)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Ring R
Γ'₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation R Γ₀
w : Valuation R Γ'₀
x : WithVal w
⊢ (congr v w (RingEquiv.refl R)).symm x = (equiv v).symm ((equiv w) x)

Tactic:
by simp

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

Goal state before:
pp: R✝ : Type u_1
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
⊢ ∀ (x y : (ofClass Valued.v).ValueGroup₀),
    (WithZero.map' ↑(valueGroupEquiv v)) (x * y) =
      (WithZero.map' ↑(valueGroupEquiv v)) x * (WithZero.map' ↑(valueGroupEquiv v)) y

Tactic:
by simp

Goal state after:
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 Q : Fin 3 → R
⊢ (W'.map f).addX (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)

Tactic:
simp only [addX]
  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_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : x = π.val ^ n * ↑u
hn : ¬n = 0
⊢ Submodule.IsPrincipal P

Tactic:
rw [hu, Ideal.mul_unit_mem_iff_mem P u.isUnit,
        IsPrime.pow_mem_iff_mem hP _ (pos_iff_ne_zero.mpr hn),
        ← Ideal.span_singleton_le_iff_mem] at 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)ˣ
hx_mem : span {π.val} ≤ P
hu : x = π.val ^ n * ↑u
hn : ¬n = 0
⊢ Submodule.IsPrincipal P
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ s.Subsingleton

Tactic:
rw [← Set.subsingleton_coe, ← not_nontrivial_iff_subsingleton, nontrivial_iff_lt]

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ ¬∃ x y, x < y
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: 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

Tactic:
by simp

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

Goal state before:
pp: 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
⊢ Subring.map (algebraMap A K) ⊤ = (valuation K (maximalIdeal A)).valuationSubring.toSubring

Tactic:
by
  ext
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨_, _, rfl⟩ := Subring.mem_map.mp h
    apply valuation_le_one
  · obtain ⟨y, rfl⟩ := exists_lift_of_le_one h
    rw [Subring.mem_map]
    exact ⟨y, mem_top _, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: ⊢ AddEquiv.neg ℤ ∉ {AddEquiv.refl ℤ}

Tactic:
by simp [AddEquiv.ext_int_iff]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: ⊢ ∀ {a b : ℤ},
    ((AddEquiv.neg ℤ).trans { toEquiv := toDual, map_add' := ⋯ }).toFun a ≤
        ((AddEquiv.neg ℤ).trans { toEquiv := toDual, map_add' := ⋯ }).toFun b ↔
      a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
g : ↥⊤ ≃+o ℤ := { toAddEquiv := AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
⊢ (AddSubgroup.closure {1}).toAddSubsemigroup = ⊤.toAddSubsemigroup

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

Tactic:
simp_all [← Units.val_le_val]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝

Tactic:
simp_all [← Units.val_le_val]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

Tactic:
simp_all [← Units.val_le_val]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝

Tactic:
simp_all [← Units.val_le_val]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : MulArchimedean G
X : Type u_2
inst✝¹ : Preorder X
inst✝ : LocallyFiniteOrder X
⊢ ∀ {a b : Multiplicative X}, Multiplicative.toAdd a ≤ Multiplicative.toAdd b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : MulArchimedean G
X : Type u_2
inst✝¹ : Preorder X
inst✝ : LocallyFiniteOrder X
⊢ ∀ {a b : Additive X}, Additive.toMul a ≤ Additive.toMul b ↔ a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝⁶ : CommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedMonoid G
inst✝³ : MulArchimedean G
X : Type u_2
inst✝² : Preorder X
inst✝¹ : LocallyFiniteOrder X
inst✝ : Monoid X
⊢ ∀ {a b : Xˣ}, { toFun := Units.val, inj' := ⋯ } a ≤ { toFun := Units.val, inj' := ⋯ } b ↔ a ≤ b

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ (monomial 0) a = C a

Tactic:
by simp

Goal state after:
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:
rw [one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff 0) (φ * X) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff 0) (X * φ) = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ = (X * mk fun p ↦ (coeff (p + 1)) φ) + C (constantCoeff φ)

Tactic:
ext (_ | n)
  · simp
  · simp only [coeff_succ_X_mul, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
a b : R
⊢ (monomial 0).toFun (a * b) = (monomial (0 + 0)) (a * b)

Tactic:
by simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
· rw [intValuationDef, if_pos hxy]; exact zero_le

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
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) ((map T.subtype) (p.toSubring T hp)) = (coeff n) p

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ f ((coeff n) (φ * ψ)) = (coeff n) ((fun n ↦ f ((coeff n) φ)) * fun n ↦ f ((coeff n) ψ))

Tactic:
rw [coeff_mul, map_sum, coeff_mul]

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x ∈ antidiagonal n, f ((coeff x.1) φ * (coeff x.2) ψ) =
    ∑ p ∈ antidiagonal n, ((coeff p.1) fun n ↦ f ((coeff n) φ)) * (coeff p.2) fun n ↦ f ((coeff n) ψ)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ (rescale 0) f = C (constantCoeff f)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ (coeff n) ((rescale b) ((rescale a) f)) = (coeff n) ((rescale (a * b)) f)

Tactic:
simp_rw [coeff_rescale]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ b ^ n * (a ^ n * (coeff n) f) = (a * b) ^ n * (coeff n) f
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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)) ≤ exp 0

Tactic:
exp_le_exp,

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)) ≤ exp (-↑n) ↔
    v.asIdeal ^ n ∣ Ideal.span {r}

Tactic:
exp_le_exp,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : ¬r = 0
⊢ -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors) ≤ -↑n ↔ v.asIdeal ^ n ∣ Ideal.span {r}
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 : ℕ
⊢ 0 < exp 1

Tactic:
by simp

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 ∣ Ideal.span {π}
notMem : ¬v.asIdeal ^ 2 ∣ Ideal.span {π}
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Tactic:
← Associates.mk_le_mk_iff_dvd

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 : Associates.mk v.asIdeal ≤ Associates.mk (Ideal.span {π})
notMem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
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: 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
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 : Prime v
hv' : Irreducible (Associates.mk v)
h :
  exp
      (-↑((Associates.mk v).count (Associates.mk (Ideal.span {n})).factors) -
        -↑((Associates.mk v).count (Associates.mk (Ideal.span {d})).factors)) ≤
    exp 0
⊢ Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {d})) ≤
    Multiset.count ⟨Associates.mk v, hv✝⟩ (Associates.factors' (Ideal.span {n}))

Tactic:
exp_le_exp,

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
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 : Prime v
hv' : Irreducible (Associates.mk v)
h :
  -↑((Associates.mk v).count (Associates.mk (Ideal.span {n})).factors) -
      -↑((Associates.mk v).count (Associates.mk (Ideal.span {d})).factors) ≤
    0
⊢ 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.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
e : σ →₀ ℕ
p : ℕ
r : R
⊢ ∀ i ∈ e.support, MvPowerSeries.X i ^ 0 = 1

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
⊢ 0 ∈ Iic n

Tactic:
by simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
⊢ 0 ∈ Iic n

Tactic:
by 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
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ∀ (x y : (ofClass (valuation K v)).ValueGroup₀),
    (map' ↑(valueGroupEquiv K v)) (x * y) = (map' ↑(valueGroupEquiv K v)) x * (map' ↑(valueGroupEquiv K v)) y

Tactic:
by simp

Goal state after: