Module: Mathlib.RingTheory.Valuation.Basic

Goal state before:
pp: case neg
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ Units.mk0 ((ofClass w) (↑hx'.choose).2 * (ofClass w) (↑hy'.choose).1) ⋯ ≤
      Units.mk0 ((ofClass w) (↑hy'.choose).2 * (ofClass w) (↑hx'.choose).1) ⋯ ↔
    Units.mk0 ((ofClass v) (↑hx'.choose).2 * (ofClass v) (↑hy'.choose).1) ?neg.hxy✝ ≤
      Units.mk0 ((ofClass v) (↑hy'.choose).2 * (ofClass v) (↑hx'.choose).1) ?neg.hxy✝¹

pp: case neg.hxy
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ (ofClass v) (↑hy'.choose).2 * (ofClass v) (↑hx'.choose).1 ≠ 0

pp: case neg.hxy
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ (ofClass v) (↑hx'.choose).2 * (ofClass v) (↑hy'.choose).1 ≠ 0

Tactic:
· simp only [← Units.val_le_val]
        repeat rw [Units.val_mk0]
        simp only [MonoidWithZeroHom.coe_ofClass, ← map_mul w, ← h.le_iff_le]
        simp

Goal state after:
case neg.hxy
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ (ofClass v) (↑hy'.choose).2 * (ofClass v) (↑hx'.choose).1 ≠ 0

case neg.hxy
K : Type u_1
F : Type u_2
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : LinearOrderedCommGroupWithZero Γ'₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ''₀
inst✝ : Ring R
v : Valuation R Γ₀
w : Valuation R Γ'₀
u : Valuation R Γ''₀
h : v.IsEquiv w
x y : (ofClass v).ValueGroup₀
hx0 : ¬x = 0
hy0 : ¬y = 0
pf✝¹² : MonoidWithZeroHomClass (Valuation R Γ'₀) R Γ'₀
pf✝¹¹ : MonoidWithZeroHomClass (Valuation R Γ₀) R Γ₀
pf✝¹⁰ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).1 ≠ 0
pf✝⁹ : ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }), (ofClass v) (↑d).2 ≠ 0
hx : ∃ d, x = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁸ : (ofClass w) (↑hx.choose).1 ≠ 0
pf✝⁷ : (ofClass w) (↑hx.choose).2 ≠ 0
hy : ∃ d, y = ↑(valueGroup.mk (ofClass v) (↑d).1 (↑d).2 ⋯ ⋯)
pf✝⁶ : (ofClass w) (↑hy.choose).1 ≠ 0
pf✝⁵ : (ofClass w) (↑hy.choose).2 ≠ 0
pf✝⁴ :
  ∀ (d : { xy // ¬(ofClass v) xy.1 = 0 ∧ ¬(ofClass v) xy.2 = 0 }),
    (Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯ ∈ (ofClass v).valueGroup
hx' : ∃ d, x = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hx20 : (ofClass w) (↑hx'.choose).2 ≠ 0
hy' : ∃ d, y = ↑⟨(Units.mk0 ((ofClass v) (↑d).1) ⋯)⁻¹ * Units.mk0 ((ofClass v) (↑d).2) ⋯, ⋯⟩
hy10 : (ofClass w) (↑hy'.choose).1 ≠ 0
hx10 : (ofClass w) (↑hy'.choose).2 ≠ 0
hy20 : (ofClass w) (↑hx'.choose).1 ≠ 0
pf✝³ : (ofClass v) (↑hx'.choose).2 ≠ 0
pf✝² : (ofClass v) (↑hy'.choose).1 ≠ 0
pf✝¹ : (ofClass v) (↑hy'.choose).2 ≠ 0
pf✝ : (ofClass v) (↑hx'.choose).1 ≠ 0
⊢ (ofClass v) (↑hx'.choose).2 * (ofClass v) (↑hy'.choose).1 ≠ 0