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

Tactic:
split_ifs

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✝¹ 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)

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)

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)

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)

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) ⋯, ⋯⟩)

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) ⋯, ⋯⟩)

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) ⋯, ⋯⟩)

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) ⋯, ⋯⟩)

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)

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)

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) ⋯, ⋯⟩)

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) ⋯, ⋯⟩)

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)

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)

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) ⋯, ⋯⟩)

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) ⋯, ⋯⟩)