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

Goal state before:
pp: case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

Tactic:
·

Goal state after:
case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

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

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

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

Tactic:
·

Goal state after:
case pos
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
⊢ (fromAffine Affine.Point.zero).toAffineLift = Affine.Point.zero

pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
x✝ y✝ : F
h✝ : W.toAffine.Nonsingular x✝ y✝
⊢ (fromAffine (Affine.Point.some x✝ y✝ h✝)).toAffineLift = Affine.Point.some x✝ y✝ h✝

Tactic:
·

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
⊢ (fromAffine Affine.Point.zero).toAffineLift = Affine.Point.zero
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
x✝ y✝ : F
h✝ : W.toAffine.Nonsingular x✝ y✝
⊢ (fromAffine (Affine.Point.some x✝ y✝ h✝)).toAffineLift = Affine.Point.some x✝ y✝ h✝

Tactic:
·

Goal state after:
case some
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
x✝ y✝ : F
h✝ : W.toAffine.Nonsingular x✝ y✝
⊢ (fromAffine (Affine.Point.some x✝ y✝ h✝)).toAffineLift = Affine.Point.some x✝ y✝ h✝
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
⊢ y * ↑u ≤ᵥ 0

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
⊢ x * ↑v ≤ᵥ 0

Tactic:
·

Goal state after:
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
⊢ y * ↑u ≤ᵥ 0
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
⊢ x * ↑v ≤ᵥ 0

Tactic:
·

Goal state after:
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
⊢ x * ↑v ≤ᵥ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

pp: case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
·

Goal state after:
case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
·

Goal state after:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

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

pp: case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
Hx : v x = 0
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

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

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

Tactic:
·

Goal state after:
case neg
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

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

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x_1 * x) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

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

Tactic:
·

Goal state after:
case pos
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)

Tactic:
·

Goal state after:
case neg
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
⊢ (x * ↑v ≤ᵥ z * ↑s) = (y * ↑u ≤ᵥ w * ↑t)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg.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
⊢ y * ↑u ≤ᵥ w * ↑t

pp: case neg.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
⊢ x * ↑v ≤ᵥ z * ↑s

Tactic:
·

Goal state after:
case neg.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
⊢ y * ↑u ≤ᵥ w * ↑t
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case pos
α : 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)
hs : 0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

pp: case neg
α : 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)
hs : 0 ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
·

Goal state after:
case pos
α : 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)
hs : 0 ∈ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg.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
⊢ x * ↑v ≤ᵥ z * ↑s

Tactic:
·

Goal state after:
case neg.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
⊢ x * ↑v ≤ᵥ z * ↑s
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case neg
α : 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)
hs : 0 ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
·

Goal state after:
case neg
α : 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)
hs : 0 ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this : ∀ (x y : Γ₀), x ≤ y → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
hle : ¬x ≤ y
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
·

Goal state after:
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this : ∀ (x y : Γ₀), x ≤ y → Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
hle : ¬x ≤ y
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 ((0, 0).1 * (0, 0).2))

pp: case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))

pp: case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
·

Goal state after:
case inl.inl
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : 0 ≤ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 ((0, 0).1 * (0, 0).2))
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))

pp: case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
·

Goal state after:
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
·

Goal state after:
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
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
hx : x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case neg
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
hx : x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case pos
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
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case neg
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
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
·

Goal state after:
case pos
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
hx : x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
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
hx : x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case pos
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
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case neg
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
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
·

Goal state after:
case neg
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
hx : x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ

pp: case mpr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ) →
    ∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(v.ltAddSubgroup ((Units.map ↑embedding) i))) → ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) →
    ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
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
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

pp: case neg
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
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
·

Goal state after:
case pos
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
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg
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
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
·

Goal state after:
case neg
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
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩