Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos
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)
h1 : (ofClass v) x = 0
h2 : (ofClass v) y = 0
⊢ v x * v ↑r = v y * v ↑s → 0 = 0

pp: case pos
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)
h1 : (ofClass v) x = 0
h2 : ¬(ofClass v) y = 0
h3 : (ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s → 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * 0

pp: case neg
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)
h1 : (ofClass v) x = 0
h2 : ¬(ofClass v) y = 0
h3 : ¬(ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s → 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑s) h3, ⋯⟩

pp: case pos
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)
h1 : ¬(ofClass v) x = 0
h✝¹ : (ofClass v) ↑r = 0
h✝ : (ofClass v) y = 0
⊢ v x * v ↑r = v y * v ↑s → ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * 0 = 0

pp: case pos
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)
h1 : ¬(ofClass v) x = 0
h✝² : (ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : (ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s → ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * 0

pp: case neg
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)
h1 : ¬(ofClass v) x = 0
h✝² : (ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : ¬(ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s →
    ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑s) h✝, ⋯⟩

pp: case pos
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)
h1 : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) ↑r = 0
h✝ : (ofClass v) y = 0
⊢ v x * v ↑r = v y * v ↑s → ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑r) h✝¹, ⋯⟩ = 0

pp: case pos
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)
h1 : ¬(ofClass v) x = 0
h✝² : ¬(ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : (ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s →
    ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑r) h✝², ⋯⟩ = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * 0

pp: case neg
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)
h1 : ¬(ofClass v) x = 0
h✝² : ¬(ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : ¬(ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s →
    ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑r) h✝², ⋯⟩ =
      ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑s) h✝, ⋯⟩

Tactic:
<;>

Goal state after:
case pos
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)
h1 : (ofClass v) x = 0
h2 : (ofClass v) y = 0
⊢ v x * v ↑r = v y * v ↑s → 0 = 0

case pos
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)
h1 : (ofClass v) x = 0
h2 : ¬(ofClass v) y = 0
h3 : (ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s → 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * 0

case neg
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)
h1 : (ofClass v) x = 0
h2 : ¬(ofClass v) y = 0
h3 : ¬(ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s → 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑s) h3, ⋯⟩

case pos
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)
h1 : ¬(ofClass v) x = 0
h✝¹ : (ofClass v) ↑r = 0
h✝ : (ofClass v) y = 0
⊢ v x * v ↑r = v y * v ↑s → ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * 0 = 0

case pos
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)
h1 : ¬(ofClass v) x = 0
h✝² : (ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : (ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s → ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * 0

case neg
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)
h1 : ¬(ofClass v) x = 0
h✝² : (ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : ¬(ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s →
    ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * 0 = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑s) h✝, ⋯⟩

case pos
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)
h1 : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) ↑r = 0
h✝ : (ofClass v) y = 0
⊢ v x * v ↑r = v y * v ↑s → ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑r) h✝¹, ⋯⟩ = 0

case pos
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)
h1 : ¬(ofClass v) x = 0
h✝² : ¬(ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : (ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s →
    ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑r) h✝², ⋯⟩ = ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * 0

case neg
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)
h1 : ¬(ofClass v) x = 0
h✝² : ¬(ofClass v) ↑r = 0
h✝¹ : ¬(ofClass v) y = 0
h✝ : ¬(ofClass v) ↑s = 0
⊢ v x * v ↑r = v y * v ↑s →
    ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑r) h✝², ⋯⟩ =
      ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) ↑s) h✝, ⋯⟩