mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simp

Goal state after:
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:
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:
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
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
⊢ exp (-1) ≠ 0

Tactic:
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:
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
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hsurj : Function.Surjective ⇑v
⊢ exp (-1) ≠ 0

Tactic:
simp

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

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

Tactic:
← addY_of_X_eq' hP hQ hx,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addY P Q = W.addY P Q * (P z * Q z) ^ 3 / (P z * Q z) ^ 3
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:
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:
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:
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:
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:
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 : (ofClass Valued.v).ValueGroup₀
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) ((WithZero.map' ↑(valueGroupEquiv v)) 0) = 0

Tactic:
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 : (ofClass Valued.v).ValueGroup₀
a : ↥(ofClass Valued.v).valueGroup
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) ((WithZero.map' ↑(valueGroupEquiv v)) ↑a) = ↑a

Tactic:
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 Γ₀
y : (ofClass v).ValueGroup₀
⊢ (WithZero.map' ↑(valueGroupEquiv v)) ((WithZero.map' ↑(valueGroupEquiv v).symm) 0) = 0

Tactic:
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 Γ₀
y : (ofClass v).ValueGroup₀
b : ↥(ofClass v).valueGroup
⊢ (WithZero.map' ↑(valueGroupEquiv v)) ((WithZero.map' ↑(valueGroupEquiv v).symm) ↑b) = ↑b

Tactic:
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:
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 Γ₀
a b : (ofClass Valued.v).ValueGroup₀
⊢ (WithZero.map' ↑(valueGroupEquiv v)) 0 ≤ (WithZero.map' ↑(valueGroupEquiv v)) 0 ↔ 0 ≤ 0

Tactic:
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 Γ₀
a b : (ofClass Valued.v).ValueGroup₀
val✝ : ↥(ofClass Valued.v).valueGroup
⊢ (WithZero.map' ↑(valueGroupEquiv v)) 0 ≤ (WithZero.map' ↑(valueGroupEquiv v)) ↑val✝ ↔ 0 ≤ ↑val✝

Tactic:
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 Γ₀
a b : (ofClass Valued.v).ValueGroup₀
val✝ : ↥(ofClass Valued.v).valueGroup
⊢ (WithZero.map' ↑(valueGroupEquiv v)) ↑val✝ ≤ (WithZero.map' ↑(valueGroupEquiv v)) 0 ↔ ↑val✝ ≤ 0

Tactic:
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 Γ₀
a✝ b✝ : (ofClass Valued.v).ValueGroup₀
a b : ↥(ofClass Valued.v).valueGroup
⊢ (WithZero.map' ↑(valueGroupEquiv v)) ↑a ≤ (WithZero.map' ↑(valueGroupEquiv v)) ↑b ↔ ↑a ≤ ↑b

Tactic:
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 Γ
inst✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
h : ∃ b, π * b = 1
this : ¬π = 0
⊢ False

Tactic:
rw [← isUnit_iff_exists_inv] at h

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
h : IsUnit π
this : ¬π = 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
⊢ -f (W'.dblU P) * (f (W'.dblX P) - (⇑f ∘ P) x * ((⇑f ∘ P) y - f (W'.negY P)) ^ 2) +
      (⇑f ∘ P) y * ((⇑f ∘ P) y - f (W'.negY P)) ^ 3 =
    f (-W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3)

Tactic:
simp

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

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblU (⇑↑f ∘ P) = ↑f ((W'⁄A).dblU P)

Tactic:
← map_dblU,

Goal state after:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (W'⁄B).dblU (⇑↑f ∘ P) = ((W'⁄A).map ↑f).dblU (⇑↑f ∘ P)
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
x : WithVal v
hx :
  x ∈
    {x |
      Valued.v.restrict x <
        ↑(Units.mk0 (Valued.v.restrict ((equiv v).symm r) / Valued.v.restrict ((equiv v).symm s)) ⋯)}
y : R := (equiv v) x
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
h' : v.restrict.IsEquiv w.restrict
⊢ v (y * s) < v r

Tactic:
simp only [equiv_symm_apply, Units.val_mk0, Set.mem_ofPred_eq, lt_div_iff₀ hs0'] at hx

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : v.IsEquiv w
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : R
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
x : WithVal v
y : R := (equiv v) x
hy : toVal v y = x
hs0' : 0 < Valued.v.restrict (toVal v s)
h' : v.restrict.IsEquiv w.restrict
hx : Valued.v.restrict x * Valued.v.restrict (toVal v s) < Valued.v.restrict (toVal v r)
⊢ v (y * s) < v r
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑γ}

Tactic:
have h' : w.restrict.IsEquiv v.restrict := h.restrict

Goal state after:
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
hval : Valued R Γ₀'
hv : Valued.v = w
h : w.IsEquiv v
γ : (ofClass Valued.v).ValueGroup₀ˣ
r s : WithVal v
hr₀ : 0 < Valued.v r
hs₀ : 0 < Valued.v s
hr : Valued.v.restrict r / Valued.v.restrict s = ↑γ
h' : w.restrict.IsEquiv v.restrict
⊢ ∃ ia, ∀ x ∈ {x | Valued.v.restrict x < ↑ia}, (equiv v).symm x ∈ {x | Valued.v.restrict x < ↑γ}
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz'✝ : z < y
hz0 : ⊥ < ↑z
hz' : (↑z).unbot ⋯ < (↑y).unbot ⋯
⊢ (↑z).unbot ⋯ ∈ some ⁻¹' s

Tactic:
simp

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
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz'✝ : z < y
hz0 : ⊥ < ↑z
hz' : (↑z).unbot ⋯ < (↑y).unbot ⋯
⊢ (↑y).unbot ⋯ ∈ some ⁻¹' s

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: case refine_1
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 ⋯) ∈ s

Tactic:
simp

Goal state after:
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:
· rw [← WithBot.coe_lt_coe]
    simp [hz'.trans_le']

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : IsDiscreteValuationRing A
x : A
⊢ (maximalIdeal A).intValuation x = (ENat.recTopCoe 0 (fun x ↦ ↑(ofAdd ↑x)) ((addVal A) x))⁻¹

Tactic:
by_cases hx : x = 0
  · simp [hx]
  obtain ⟨ϖ, hϖ⟩ := exists_irreducible A
  obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible hx hϖ
  have : (maximalIdeal A).intValuation ↑u = 1 := by simp [maximalIdeal]
  simp [(maximalIdeal A).intValuation_singleton hϖ.ne_zero
    hϖ.maximalIdeal_eq, hϖ, this, WithZero.exp_eq_coe_ofAdd (n : ℤ)]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
b : Gˣ
ha : 0 < 1
⊢ 0 ^ 1 < ↑b

Tactic:
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
a : G
ha : a ≠ 1
this : Function.Injective fun x ↦ a ^ x
m : ℤ
⊢ ∃! k, a ^ k = a ^ m

Tactic:
exact ⟨m, rfl, fun k hk ↦ this hk⟩

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inl
⊢ AddEquiv.refl ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inr
⊢ AddEquiv.neg ℤ ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤ
H : e 1 = -1
⊢ 0 < 1

Tactic:
simp

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:
simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+o ℤᵒᵈ
H : e 1 = 1
⊢ 0 < 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: 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✝ y✝ : ↥(closure {x})
⊢ { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x✝ * y✝) =
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun x✝ *
      { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun y✝

Tactic:
simp

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 Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
h✝ : 0 ∉ U
γ : (ofClass v).ValueGroup₀ˣ
h : U ⊆ {a | ↑γ ≤ v.restrict a}
a✝ : K
⊢ a✝ ∈ {a | ↑γ ≤ v.restrict a} → a✝ ∈ ⇑v.restrict ⁻¹' Ici ↑γ

Tactic:
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
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
x✝ : G
⊢ x✝ ∈ closure {a} ↔ x✝ ∈ closure {a⁻¹}

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ IsLeast {y | y ∈ closure {a} ∧ 1 < y} b

Tactic:
convert! @this (a⁻¹) ?_ (by simpa using le_of_not_ge ha) using 4
      · simp
      · rwa [mabs_inv]

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:
simp

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
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
h : ∀ (a b : (ofClass v).ValueGroup₀), embedding a = embedding b ↔ a = b
x✝ : hat K
⊢ x✝ ∈ {b | ∃ r, v.restrict r = extension b} ↔ x✝ ∈ extension ⁻¹' range ⇑v.restrict

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: 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.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a✝) ≤
      ↑((MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b✝) ↔
    a✝ ≤ b✝

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
⊢ ∀ ⦃j : VariableChange K⦄,
    (fun C_1 ↦ IsIntegral R (C_1 • C • W)) j →
      (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1 ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j →
        (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1

Tactic:
intro j

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
j : VariableChange K
⊢ (fun C_1 ↦ IsIntegral R (C_1 • C • W)) j →
    (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1 ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j →
      (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1
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:
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:
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:
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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
a : R
n✝ : ℕ
⊢ (coeff n✝) (a • f) = (coeff n✝) (C a * f)

Tactic:
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:
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:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff (d - n)) p = (coeff (d - n + n - n)) p

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after: