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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * W'.negY P * P z * W'.neg P z + P x ^ 2 * P x * W'.neg P z ^ 2 -
                        W'.a₁ * P x * W'.negY P * P z ^ 2 * W'.neg P z -
                      W'.a₁ * P y * P x * P z * W'.neg P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * W'.neg P z ^ 2 -
                  W'.a₃ * W'.negY P * P z ^ 4 * W'.neg P z -
                W'.a₃ * P y * P z * W'.neg P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * W'.neg P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * W'.neg P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * W'.neg P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      (W'.dblZ P ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
neg_Z,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * W'.negY P * P z * P z + P x ^ 2 * P x * P z ^ 2 -
                        W'.a₁ * P x * W'.negY P * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * W'.negY P * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      (W'.dblZ P ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
g : ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).pt
x✝ : I
⊢ (((Over.forget S).mapCone c.unop).π ≫ { app := fun x ↦ (D.obj x).hom, naturality := ⋯ }).app x✝ =
    ((Functor.const I).map (Over.Hom.left g ≫ X.hom)).app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case zero
e : ℝ≥0
he : 1 < e
x : WithZero (Multiplicative ℤ)
⊢ x < 0 → (toNNReal ⋯) x < (toNNReal ⋯) 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : NonarchimedeanGroup G
U : Set (G × G)
hU : U ∈ 𝓝 1
V W : OpenSubgroup G
h : ↑V ×ˢ ↑W ⊆ U
⊢ ↑(V ⊓ W) ⊆ ↑V

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : NonarchimedeanGroup G
U : Set (G × G)
hU : U ∈ 𝓝 1
V W : OpenSubgroup G
h : ↑V ×ˢ ↑W ⊆ U
⊢ ↑(V ⊓ W) ⊆ ↑W

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ + x + -x₀) ⁻¹' ↑(B i)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} = (fun x ↦ x - a) ⁻¹' ↑(B i)

Tactic:
ext b

Goal state after:
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
b : A
⊢ b ∈ {b | b - a ∈ B i} ↔ b ∈ (fun x ↦ x - a) ⁻¹' ↑(B i)
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y ↦ a + y) '' ↑(B i) ⊆ s
b : A
⊢ b ∈ {b | b - a ∈ B i} ↔ b ∈ (fun x ↦ x - a) ⁻¹' ↑(B i)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ⊆ (fun x ↦ x₀ + x + -x₀) ⁻¹' ↑(B i)

Tactic:
simp

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

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ addU P Q = 0

Tactic:
by
  rw [addU, hQz, mul_zero, div_zero, neg_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 : R
⊢ ¬x <ᵥ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : x * y ≤ᵥ 0
⊢ 0 = x * 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
u : ↥(posSubmonoid R)
⊢ x * ↑u ≤ᵥ y * ↑u ↔ x ≤ᵥ y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
u : ↥(posSubmonoid R)
⊢ ↑u * x ≤ᵥ ↑u * y ↔ x ≤ᵥ y

Tactic:
simp

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

Goal state before:
pp: case right
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this : t * ↑v * ↑u ≤ᵥ s * ↑w * ↑u
⊢ t * ↑u ≤ᵥ r * ↑w

Tactic:
grw [veq_mul_right_comm s] at this

Goal state after:
case right
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this : t * ↑v * ↑u ≤ᵥ s * ↑u * ↑w
⊢ t * ↑u ≤ᵥ r * ↑w
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : R
y : ↥(posSubmonoid R)
h : x ≤ᵥ 0
⊢ 0 * ↑y ≤ᵥ x * ↑1

Tactic:
simp

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 * ↑1 ≤ᵥ 1 * ↑x

Tactic:
simp

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)
⊢ 1 * ↑x ≤ᵥ ↑x * ↑1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ 1 * ↑1 ≤ᵥ 1 * ↑1

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
⊢ ValueGroupWithZero.mk (x ^ 0) (s ^ 0) = ValueGroupWithZero.mk (y ^ 0) (t ^ 0)

Tactic:
simp

Goal state after:
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
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.lift (fun a b ↦ ValueGroupWithZero.mk (a ^ 0) (b ^ 0)) ⋯ (ValueGroupWithZero.mk x y) = 1

Tactic:
simp

Goal state after:
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 x✝¹ : R
x✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk (0 * x✝¹) (1 * x✝) = ValueGroupWithZero.mk 0 1

Tactic:
simp

Goal state after:
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 x✝¹ : R
x✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk (x✝¹ * 0) (x✝ * 1) = ValueGroupWithZero.mk 0 1

Tactic:
simp

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

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ 0 * ↑s * ↑t * ↑u ≤ᵥ 0 * (↑s * ↑v)

Tactic:
simp

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

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : y * ↑u ≤ᵥ w * ↑t
⊢ 0 * ↑t * ↑s * ↑v ≤ᵥ 0 * (↑t * ↑u)

Tactic:
simp

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀ˣ
⊢ {↑γ} ∈ 𝓝 ↑γ

Tactic:
simp

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

Goal state before:
pp: case e'_5
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x✝ : (ofClass v).ValueGroup₀ˣ
⊢ {p | v (p.2 + -p.1) < embedding ↑x✝} = (fun p ↦ p.2 + -p.1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) x✝))

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ _i.toUniformSpace = IsTopologicalAddGroup.rightUniformSpace R

Tactic:
by
  refine UniformSpace.ext ((hasBasis_uniformity R Γ₀).eq_of_same_basis ?_)
  convert! v.subgroups_basis.hasBasis_nhds_zero.comap _
  simp_rw [restrict_lt_iff_lt_embedding, sub_eq_add_neg]
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
r : (ofClass v).ValueGroup₀ˣ
hr : {z | v.restrict (z - x) < ↑r} ⊆ s
x✝ : R
⊢ (valuation R) (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r) ↔ v.restrict (x✝ - x) < ↑r

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
x✝¹ : ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s
r : (ValueGroupWithZero R)ˣ
hr : {a | (valuation R) (a - x) < ↑r} ⊆ s
x✝ : R
⊢ v.restrict (x✝ - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r) ↔ (valuation R) (x✝ - x) < ↑r

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : TopologicalSpace R
v : Valuation R Γ₀
inst✝ : v.Compatible
H : ∀ {s : Set R} {x : R}, s ∈ 𝓝 x ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
s : Set R
x : R
x✝ : ∃ γ, (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑γ} ⊆ s
γ : (ValueGroupWithZero R)ˣ
hγ : (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑γ} ⊆ s
⊢ (orderMonoidIso v) ↑γ ≠ 0

Tactic:
simp

Goal state after:
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 x : R
y : ↥(posSubmonoid R)
⊢ 0 * ↑y ≤ᵥ x * ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : TopologicalSpace R
v : Valuation R Γ₀
inst✝ : v.Compatible
H : ∀ {s : Set R} {x : R}, s ∈ 𝓝 x ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s
s : Set R
x : R
h_mem : s ∈ 𝓝 x
γ : (ofClass v).ValueGroup₀ˣ
hγ : {z | v.restrict (z - x) < ↑γ} ⊆ s
⊢ (orderMonoidIso v).symm ↑γ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
x : R
γ : (ValueGroupWithZero R)ˣ
x✝ : True
⊢ ↑γ ≠ 0 ∧ {y | (valuation R) (y - x) < ↑γ} ⊆ {z | (valuation R) (z - x) < ↑γ}

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
x : R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
⊢ True ∧ {z | (valuation R) (z - x) < ↑(Units.mk0 γ hγ)} ⊆ {y | (valuation R) (y - x) < γ}

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
γ : (ValueGroupWithZero R)ˣ
x✝ : True
⊢ ↑γ ≠ 0 ∧ {x | (valuation R) x < ↑γ} ⊆ {x | (valuation R) x < ↑γ}

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
γ : ValueGroupWithZero R
hγ : γ ≠ 0
⊢ True ∧ {x | (valuation R) x < ↑(Units.mk0 γ hγ)} ⊆ {x | (valuation R) x < γ}

Tactic:
simp

Goal state after:
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 x : R
y : ↥(posSubmonoid R)
h : ¬x ≤ᵥ 0
⊢ ↑y * x * ↑1 ≤ᵥ 1 * ↑(y * ⟨x, h⟩) ∧ 1 * ↑(y * ⟨x, h⟩) ≤ᵥ ↑y * x * ↑1

Tactic:
simp

Goal state after:
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✝
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
x x✝¹ x✝ : R
⊢ ValueGroupWithZero.mk (x✝¹ * x✝) 1 = ValueGroupWithZero.mk x✝¹ 1 * ValueGroupWithZero.mk x✝ 1

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ ∀ x ∈ {x | v.restrict x < 0}, {x | v.restrict x < 0} ∈ 𝓝 x

Tactic:
simp

Goal state after:
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✝
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
x : R
S : Type u_3
Γ : Type u_4
inst✝¹ : Ring S
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation S Γ
⊢ ¬v 1 ≤ v 0

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace] {x | v.restrict x < 0}

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a b : R
hab : a ≤ᵥ b
⊢ a ^ 0 ≤ᵥ b ^ 0

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
a b : R
hab : a ≤ᵥ b
n✝ : ℕ
hn : a ^ n✝ ≤ᵥ b ^ n✝
⊢ a ^ (n✝ + 1) ≤ᵥ b ^ (n✝ + 1)

Tactic:
| succ _ hn =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
s : (ValueGroupWithZero R)ˣ
h : 1 ≠ s
⊢ ↑s ≠ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
r s : (ValueGroupWithZero R)ˣ
h : r ≠ s
hr : r ≠ 1
⊢ ↑r ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁷ : Ring R
inst✝⁶ : ValuativeRel R
K : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : ValuativeRel K
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
cts_add : ContinuousConstVAdd R R
basis : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R).restrict x < ↑γ}
x₀ x✝ : R
⊢ ((fun x ↦ x₀ + x) ∘ fun x ↦ -x₀ + x) x✝ = _root_.id x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsOpen[_i.toTopologicalSpace] ↑v.integer

Tactic:
simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]
  exact isOpen_closedBall _ one_ne_zero

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : v r = 1
⊢ v ↑s ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ ∀ x ∈ {x | v.restrict x < 0}, {x | v.restrict x < 0} ∈ 𝓝 x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsClosed[_t] {x | v.restrict x < 0}

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
x✝ : R
⊢ v.restrict x✝ = 0 ↔ v.restrict x✝ ≤ 0

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
⊢ ∀ (b : 0 <ᵥ w),
    ((if h : (ofClass v) y = 0 then 0
        else
          if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩) /
        if h : (ofClass v) w = 0 then 0
        else
          if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
      ((if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) h, ⋯⟩) /
          if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩) *
        ((if h : (ofClass v) y = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) y) h, ⋯⟩) /
          if h : (ofClass v) w = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

Tactic:
hw

Goal state after:
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
⊢ ((if h : (ofClass v) y = 0 then 0
      else if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩) /
      if h : (ofClass v) w = 0 then 0
      else if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    ((if h : (ofClass v) x = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) x) h, ⋯⟩) /
        if h : (ofClass v) z = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩) *
      ((if h : (ofClass v) y = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) y) h, ⋯⟩) /
        if h : (ofClass v) w = 0 then 0 else ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if 0 = 0 then 0 else hatInv 0) = 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x : R
⊢ (restrict₀ (ofClass v)) x = (restrict₀ (ofClass v)) x / (restrict₀ (ofClass v)) ↑1

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x : ValueGroupWithZero R
⊢ (fun x ↦ embedding (⋯.orderMonoidIso x)) ((↑(embed v)).toFun x) = x

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x : ValueGroupWithZero R
⊢ embedding (⋯.orderMonoidIso ((↑(embed v)).toFun x)) = x

Tactic:
simp

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

Goal state after: