mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ W.negAddY P Q = W.negAddY P Q

Tactic:
]

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 y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x * (restrict₀ (ofClass v)) ↑r = (restrict₀ (ofClass v)) y * (restrict₀ (ofClass v)) ↑s

pp: case hb
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

pp: case hd
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0

Tactic:
]

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 y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x * (restrict₀ (ofClass v)) ↑r = (restrict₀ (ofClass v)) y * (restrict₀ (ofClass v)) ↑s

case hb
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

case hd
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 y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case inr
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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x < r}

Tactic:
]

Goal state after:
case inr
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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x < r}
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x < r}
Module: Mathlib.Topology.Algebra.UniformRing

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ ∀ x ∈ {x | v.restrict x ≤ r}, {x | v.restrict x ≤ r} ∈ 𝓝 x

Tactic:
]

Goal state after:
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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ ∀ x ∈ {x | v.restrict x ≤ r}, {x | v.restrict x ≤ r} ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.UniformRing

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

Tactic:
]

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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
hx : x ∈ {x | v.restrict x ≤ r}
⊢ ∃ γ, ∀ (a : R), v.restrict (a - x) < ↑γ → v.restrict a ≤ r

Tactic:
exact ⟨Units.mk0 _ hr, fun y hy ↦
    (sub_add_cancel y x).symm ▸ le_trans (v.restrict.map_add _ _) (max_le (le_of_lt hy) hx)⟩

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
r : (ofClass v).ValueGroup₀
⊢ ∀ x ∈ {x | v.restrict x ≤ r}ᶜ, {x | v.restrict x ≤ r}ᶜ ∈ 𝓝 x

Tactic:
]

Goal state after:
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
r : (ofClass v).ValueGroup₀
⊢ ∀ x ∈ {x | v.restrict x ≤ r}ᶜ, {x | v.restrict x ≤ r}ᶜ ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.UniformRing

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf✝ : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
⊢ 1 = 1

Tactic:
]

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
r : (ofClass v).ValueGroup₀
x : R
hx : r < v.restrict x
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x ≤ r}ᶜ

Tactic:
]

Goal state after:
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
r : (ofClass v).ValueGroup₀
x : R
hx : r < v.restrict x
⊢ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ {x | v.restrict x ≤ r}ᶜ
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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen ({x | v.restrict x ≤ r} \ {x | v.restrict x < r})

Tactic:
]

Goal state after:
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
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen ({x | v.restrict x ≤ r} \ {x | v.restrict x < r})
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝⁷ : Ring α
inst✝⁶ : UniformSpace α
inst✝⁵ : IsTopologicalRing α
inst✝⁴ : IsUniformAddGroup α
β : Type u
inst✝³ : UniformSpace β
inst✝² : Ring β
inst✝¹ : IsUniformAddGroup β
inst✝ : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
a : α
⊢ ↑(f a) = ↑(f a)

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {x | (fun x ↦ ∃ c, Tendsto (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {x | (fun x ↦ ∃ c, Tendsto (fun x ↦ ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun y ↦ ↑y) (map (fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y))))

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
⊢ Cauchy (map (fun y ↦ ↑y) (map (fun x ↦ x⁻¹) (Filter.comap coe' (𝓝 y))))
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this✝ : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
this : (Filter.comap coe' (𝓝 y)).NeBot
⊢ uniformity K ≤ uniformity K

Tactic:
]

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

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' (𝓝 ↑0 ⊓ 𝓝 y) = ⊥

Tactic:
]

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' (𝓝 ↑0 ⊓ 𝓝 y) = ⊥
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' ⊥ = ⊥

Tactic:
]

Goal state after:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x ↦ ↑x⁻¹) = (fun y ↦ ↑y) ∘ fun x ↦ x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' ⊥ = ⊥
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : IsTopologicalRing α
inst✝⁸ : IsUniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : IsUniformAddGroup β
inst✝⁴ : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : IsTopologicalRing R
a✝ b✝ : Completion R
a b : R
⊢ ↑(b * a) = ↑(b * a)

Tactic:
]

Goal state after:
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
⊢ (↑0)⁻¹ = ↑0

Tactic:
]

Goal state after:
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑0)⁻¹ = ↑0
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
x y : α
⊢ (Submodule.quotientRel ⊥.closure) x y ↔ (Submodule.quotientRel ⊥.closure) x y

Tactic:
]

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

Goal state before:
pp: α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id

Tactic:
]

Goal state after:
α✝ : Type u_1
α : Type ?u.4
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalRing α
⊢ Relator.LiftFun (⇑(Submodule.quotientRel ⊥.closure)) (⇑(Submodule.quotientRel ⊥.closure)) id id
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x).hatInv = ↑x⁻¹

pp: case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑x = 0

Tactic:
]

Goal state after:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑x).hatInv = ↑x⁻¹

case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : IsTopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑x = 0
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 Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ embedding ((embed v) ((valuation R) a / (valuation R) ↑r)) <
    embedding ((embed v) ((valuation R) b / (valuation R) ↑s))

Tactic:
]

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ embedding ((embed v) ((valuation R) a / (valuation R) ↑r)) <
    embedding ((embed v) ((valuation R) b / (valuation R) ↑s))
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 Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ 0 < embedding ((embed v) ((valuation R) ↑r))

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

Goal state after:
case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑r)) = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ 0 < embedding ((embed v) ((valuation R) ↑s))

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

Goal state after:
case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a * (valuation R) ↑s < (valuation R) b * (valuation R) ↑r
⊢ ¬embedding ((embed v) ((valuation R) ↑s)) = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case hb
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ 0 < (valuation R) ↑r

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (coe' '' {0} ∪ coe' '' {0}ᶜ)
⊢ x ∈ closure (c '' {0}ᶜ)

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (coe' '' {0} ∪ coe' '' {0}ᶜ)
⊢ x ∈ closure (c '' {0}ᶜ)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case hd
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : (valuation R) a / (valuation R) ↑r < (valuation R) b / (valuation R) ↑s
⊢ 0 < (valuation R) ↑s

Tactic:
simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]

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
⊢ -P y * P x ^ 3 * P z ^ 3 + 2 * P y * P y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * P x * P y * P z ^ 2 * P z +
                                      3 * P x * P y * P x ^ 2 * P z * P z ^ 2 +
                                    P x ^ 3 * P y * P z ^ 3 -
                                  2 * P y ^ 2 * P y * P z ^ 3 +
                                W'.a₁ * P x * P y ^ 2 * P z ^ 4 +
                              W'.a₁ * P y * P x * P y * P z ^ 3 * P z -
                            W'.a₁ * P x * P y * P y * P z * P z ^ 3 -
                          W'.a₁ * P y ^ 2 * P x * P z ^ 4 -
                        2 * W'.a₂ * P x * P x * P y * P z ^ 4 * P z +
                      2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 +
                    W'.a₃ * P y ^ 2 * P z ^ 6 -
                  W'.a₃ * P y ^ 2 * P z ^ 6 -
                W'.a₄ * P x * P y * P z ^ 6 * P z -
              W'.a₄ * P x * P y * P z ^ 4 * P z ^ 3 +
            W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 +
          W'.a₄ * P x * P y * P z * P z ^ 6 -
        2 * W'.a₆ * P y * P z ^ 6 * P z ^ 3 +
      2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 =
    0

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ -P y * P x ^ 3 * P z ^ 3 + 2 * P y * P y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * P x * P y * P z ^ 2 * P z +
                                      3 * P x * P y * P x ^ 2 * P z * P z ^ 2 +
                                    P x ^ 3 * P y * P z ^ 3 -
                                  2 * P y ^ 2 * P y * P z ^ 3 +
                                W'.a₁ * P x * P y ^ 2 * P z ^ 4 +
                              W'.a₁ * P y * P x * P y * P z ^ 3 * P z -
                            W'.a₁ * P x * P y * P y * P z * P z ^ 3 -
                          W'.a₁ * P y ^ 2 * P x * P z ^ 4 -
                        2 * W'.a₂ * P x * P x * P y * P z ^ 4 * P z +
                      2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 +
                    W'.a₃ * P y ^ 2 * P z ^ 6 -
                  W'.a₃ * P y ^ 2 * P z ^ 6 -
                W'.a₄ * P x * P y * P z ^ 6 * P z -
              W'.a₄ * P x * P y * P z ^ 4 * P z ^ 3 +
            W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 +
          W'.a₄ * P x * P y * P z * P z ^ 6 -
        2 * W'.a₆ * P y * P z ^ 6 * P z ^ 3 +
      2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 =
    0
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (coe' '' {0} ∪ coe' '' {0}ᶜ)
⊢ {↑0}ᶜ ∈ 𝓝 x

Tactic:
]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (coe' '' {0} ∪ coe' '' {0}ᶜ)
⊢ {↑0}ᶜ ∈ 𝓝 x
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 Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : v (a * ↑s) < v (b * ↑r)
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))

Tactic:
]

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : v (a * ↑s) < v (b * ↑r)
⊢ embedding ((embed v) ((valuation R) a)) * embedding ((embed v) ((valuation R) ↑s)) <
    embedding ((embed v) ((valuation R) b)) * embedding ((embed v) ((valuation R) ↑r))