mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ (𝓝 0).HasBasis (fun γ ↦ γ ≠ 0) Iio

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
⊢ Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀

Tactic:
by

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

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

Tactic:
by

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 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
⊢ y * ↑u * ↑s * z =ᵥ y * ↑s * (z * ↑u)

Tactic:
by

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ {γ} ∈ 𝓝 γ

Tactic:
by

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ (𝓝 x).HasBasis (fun x ↦ True) fun x_1 ↦ {x}

Tactic:
by

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
hPz : P z = 0
⊢ W'.addX P Q = (P x * Q z) ^ 2 * Q x

Tactic:
by

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 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
⊢ y * ↑s * (z * ↑u) ≤ᵥ x * ↑t * (w * ↑v)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto f l (𝓝 γ) ↔ ∀ᶠ (x : α) in l, f x = γ

Tactic:
by

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ₁ γ₂ : Γ₀
h : γ₁ < γ₂
⊢ Iio γ₂ ∈ 𝓝 γ₁

Tactic:
by

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 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
⊢ x * ↑t * (w * ↑v) =ᵥ x * ↑v * (↑t * w)

Tactic:
by

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsOpen[topologicalSpace] s ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
by

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 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
⊢ x * ↑v * (↑t * w) ≤ᵥ z * ↑s * (↑t * w)

Tactic:
by

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsClosed[topologicalSpace] s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x : R) (i : (ofClass v).ValueGroup₀ˣ),
    ∃ j,
      ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
        (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ IsClosed[instTopologicalSpaceProd] {p | p.1 ≤ p.2}

Tactic:
by

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 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
⊢ z * ↑s * (↑t * w) =ᵥ w * ↑t * ↑s * z

Tactic:
by

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

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
s : Set R
γ : (ofClass v).ValueGroup₀ˣ
⊢ True ∧ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ)) ⊆ s ↔ {x | v x < embedding ↑γ} ⊆ s

Tactic:
by

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
hQz : Q z = 0
⊢ W'.addX P Q = (-(Q x * P z)) ^ 2 * P x

Tactic:
by

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

Goal state before:
pp: R K : Type u
inst✝² : Ring R
inst✝¹ : DivisionRing K
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s

Tactic:
by

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 Γ₀
⊢ (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | v.restrict x < ↑γ}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
s t : Set Γ₀
h₁ : Disjoint (closure[topologicalSpace] s) t
h₂ : Disjoint s (closure[topologicalSpace] t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
by

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 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
⊢ x * ↑v * ↑t * w =ᵥ x * ↑t * (w * ↑v)

Tactic:
by

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 Γ₀
⊢ (𝓤 R).HasBasis (fun x ↦ True) fun γ ↦ {p | v.restrict (p.2 - p.1) < ↑γ}

Tactic:
by

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 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
⊢ x * ↑t * (w * ↑v) ≤ᵥ y * ↑s * (z * ↑u)

Tactic:
by

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

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 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
⊢ y * ↑s * (z * ↑u) =ᵥ y * ↑u * (↑s * z)

Tactic:
by

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 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
⊢ y * ↑u * (↑s * z) ≤ᵥ w * ↑t * (↑s * z)

Tactic:
by

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 Γ₀
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {y | v.restrict (y - x) < ↑γ} ⊆ s

Tactic:
by

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 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
⊢ w * ↑t * (↑s * z) =ᵥ z * ↑s * ↑t * w

Tactic:
by

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 Γ₀
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s

Tactic:
by

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 y z w : R) (t s u v : ↥(posSubmonoid R)),
    x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

Tactic:
by

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 Γ₀
x : R
h : v x ≠ 0
⊢ v.restrict x ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] fun p ↦ p.1 * p.2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ ContinuousAt Inv.inv γ

Tactic:
by

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 a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : a₁ * ↑b₂ ≤ᵥ b₁ * ↑a₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : b₁ * ↑c₂ ≤ᵥ c₁ * ↑b₂
⊢ a₁ * ↑c₂ * ↑b₂ =ᵥ a₁ * ↑b₂ * ↑c₂

Tactic:
by

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

Goal state before:
pp: case refine_1
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
⊢ {a | (valuation R) (a - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v).symm) r)} ⊆ s

Tactic:
convert! hr; simp

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

Goal state before:
pp: case refine_2
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
⊢ {z | v.restrict (z - x) < ↑((Units.mapEquiv ↑(orderMonoidIso v)) r)} ⊆ s

Tactic:
convert! hr; 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
⊢ (∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s

Tactic:
by

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
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2

Tactic:
by

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 a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : a₁ * ↑b₂ ≤ᵥ b₁ * ↑a₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : b₁ * ↑c₂ ≤ᵥ c₁ * ↑b₂
⊢ b₁ * ↑a₂ * ↑c₂ =ᵥ b₁ * ↑c₂ * ↑a₂

Tactic:
by

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 a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : a₁ * ↑b₂ ≤ᵥ b₁ * ↑a₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : b₁ * ↑c₂ ≤ᵥ c₁ * ↑b₂
⊢ c₁ * ↑b₂ * ↑a₂ =ᵥ c₁ * ↑a₂ * ↑b₂

Tactic:
by

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
a b c : ValueGroupWithZero R
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
by

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
a b : ValueGroupWithZero R
hab : a ≤ b
hba : b ≤ a
⊢ a = b

Tactic:
by

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 Γ₀
x : R
h : v x ≠ 0
⊢ {y | v y = v x} ∈ 𝓝 x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : ValuativeRel R
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑γ} ⊆ s

Tactic:
by

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
a b : ValueGroupWithZero R
⊢ a ≤ b ∨ b ≤ a

Tactic:
by

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
t s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * ↑s <ᵥ y * ↑t

Tactic:
by

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
s : ↥(posSubmonoid R)
⊢ 0 < ValueGroupWithZero.mk x s ↔ 0 <ᵥ x

Tactic:
by

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 Γ₀
h : ∀ (x : R), x ≠ 0 → v x = 1
⊢ DiscreteTopology R

Tactic:
by

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

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)
⊢ ⊥ ≤ ValueGroupWithZero.mk x y

Tactic:
by

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

Goal state before:
pp: K : Type u
inst✝³ : DivisionRing K
Γ₀ : Type v
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued K Γ₀
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), v x ≠ 0 → r < v x
⊢ ∀ (x : K), x ≠ 0 → v x = 1

Tactic:
by

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
⊢ {z | v.restrict (z - x) < ↑(Units.mk0 ((orderMonoidIso v) ↑γ) ⋯)} ⊆ (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑γ}

Tactic:
by

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.addX P Q = addU P Q ^ 2

Tactic:
by

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

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
a b : ValueGroupWithZero R
hab : a ≤ b
c : ValueGroupWithZero R
⊢ a * c ≤ b * c

Tactic:
by

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
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero R

Tactic:
by

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
⊢ (fun x_1 ↦ x + x_1) '' {z | (valuation R) z < ↑(Units.mk0 ((orderMonoidIso v).symm ↑γ) ⋯)} ⊆
    {z | v.restrict (z - x) < ↑γ}

Tactic:
by

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
⊢ IsValuativeTopology R

Tactic:
by

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
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (n / (P z * Q z * d)) =
    (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
          Q x * P z ^ 2 * d ^ 2) /
        (P z * Q z) ^ 2 /
      d ^ 2

Tactic:
by

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
inst✝ : IsTopologicalAddGroup R
H : ∀ {s : Set R}, s ∈ 𝓝 0 ↔ ∃ γ, {z | v.restrict z < ↑γ} ⊆ s
s : Set R
x : R
this : ∀ (γ : (ofClass v).ValueGroup₀ˣ), x +ᵥ {z | v.restrict z < ↑γ} = {a | v.restrict (-x + a) < ↑γ}
⊢ (∃ γ, x +ᵥ {z | v.restrict z < ↑γ} ⊆ s) ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s

Tactic:
by

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
inst✝ : IsTopologicalAddGroup R
H : ∀ {s : Set R}, s ∈ 𝓝 0 ↔ ∃ γ, {z | v.restrict z < ↑γ} ⊆ s
⊢ IsValuativeTopology R

Tactic:
by

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
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {z | (valuation R) (z - x) < ↑γ} ⊆ s

Tactic:
by

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
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | (valuation R) x < ↑γ} ⊆ s

Tactic:
by

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
⊢ (𝓝 x).HasBasis (fun x ↦ True) fun γ ↦ {z | (valuation R) (z - x) < ↑γ}

Tactic:
by

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

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

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
⊢ (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R) x < ↑γ}

Tactic:
by

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

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

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq 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.addX P Q / addZ P Q ^ 2 =
    W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
by

Goal state after: