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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : (ofClass v) w = 0
h✝¹ : (ofClass v) x = 0
h✝ : (ofClass v) z = 0
⊢ 0 / 0 = 0 / 0 * (0 / 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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : (ofClass v) w = 0
h✝¹ : (ofClass v) x = 0
h✝ : ¬(ofClass v) z = 0
⊢ 0 / 0 = 0 / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : (ofClass v) w = 0
h✝¹ : ¬(ofClass v) x = 0
h✝ : (ofClass v) z = 0
⊢ 0 / 0 = ↑⟨Units.mk0 ((ofClass v) x) h✝¹, ⋯⟩ / 0 * (0 / 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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : (ofClass v) w = 0
h✝¹ : ¬(ofClass v) x = 0
h✝ : ¬(ofClass v) z = 0
⊢ 0 / 0 = ↑⟨Units.mk0 ((ofClass v) x) h✝¹, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : ¬(ofClass v) w = 0
h✝¹ : (ofClass v) z = 0
h✝ : (ofClass v) x = 0
⊢ 0 / 0 = 0 / 0 * (0 / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : ¬(ofClass v) w = 0
h✝¹ : (ofClass v) z = 0
h✝ : ¬(ofClass v) x = 0
⊢ 0 / 0 = ↑⟨Units.mk0 ((ofClass v) x) h✝, ⋯⟩ / 0 * (0 / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : ¬(ofClass v) w = 0
h✝¹ : ¬(ofClass v) z = 0
h✝ : (ofClass v) x = 0
⊢ 0 / (↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    0 / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (0 / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : (ofClass v) y = 0
h✝² : ¬(ofClass v) w = 0
h✝¹ : ¬(ofClass v) z = 0
h✝ : ¬(ofClass v) x = 0
⊢ 0 / (↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    ↑⟨Units.mk0 ((ofClass v) x) h✝, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (0 / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ 0 / 0 = 0 / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / 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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ 0 / 0 = 0 / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (↑⟨Units.mk0 ((ofClass v) y) 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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ 0 / 0 = 0 / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : (ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ 0 / (↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    0 / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ / 0 =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / 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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : (ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ / 0 =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * (↑⟨Units.mk0 ((ofClass v) y) 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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : (ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ / 0 =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / 0 * (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ ↑⟨Units.mk0 ((ofClass v) x) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) y) ⋯, ⋯⟩ /
      (↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ * ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩) =
    ↑⟨Units.mk0 ((ofClass v) x) h✝², ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) z) ⋯, ⋯⟩ *
      (↑⟨Units.mk0 ((ofClass v) y) h✝³, ⋯⟩ / ↑⟨Units.mk0 ((ofClass v) w) ⋯, ⋯⟩)

Tactic:
all_goals simp_all

Goal state after:
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✝¹ x✝ : ValueGroupWithZero R
x y z : R
hz : 0 <ᵥ z
w : R
hw : 0 <ᵥ w
h✝³ : ¬(ofClass v) y = 0
h✝² : ¬(ofClass v) x = 0
h✝¹ : ¬(ofClass v) w = 0
h✝ : ¬(ofClass v) z = 0
⊢ ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩ / (↑⟨Units.mk0 (v z) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v w) ⋯, ⋯⟩) =
    ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ / ↑⟨Units.mk0 (v z) ⋯, ⋯⟩ * (↑⟨Units.mk0 (v y) ⋯, ⋯⟩ / ↑⟨Units.mk0 (v w) ⋯, ⋯⟩)