case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b : ValueGroup A K
a : K
⊢ Quot.mk Setoid.r a ≤ b ∨ b ≤ Quot.mk Setoid.r a
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
⊢ a ≤ b ∨ b ≤ a
rcases a with ⟨a⟩
case mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
a b : K
⊢ Quot.mk Setoid.r a ≤ Quot.mk Setoid.r b ∨ Quot.mk Setoid.r b ≤ Quot.mk Setoid.r a
case mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b : ValueGroup A K
a : K
⊢ Quot.mk Setoid.r a ≤ b ∨ b ≤ Quot.mk Setoid.r a
rcases b with ⟨b⟩
case mk.mk.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b✝ : ValueGroup A K
b : K
xa ya : A
hya : ya ∈ nonZeroDivisors A
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤ Quot.mk Setoid.r b ∨
    Quot.mk Setoid.r b ≤ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
case mk.mk
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a✝ b✝ : ValueGroup A K
a b : K
⊢ Quot.mk Setoid.r a ≤ Quot.mk Setoid.r b ∨ Quot.mk Setoid.r b ≤ Quot.mk Setoid.r a
obtain ⟨xa, ya, hya, rfl⟩ : ∃ a b : A, _ := IsFractionRing.div_surjective a
case mk.mk.intro.intro.intro.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
case mk.mk.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b✝ : ValueGroup A K
b : K
xa ya : A
hya : ya ∈ nonZeroDivisors A
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤ Quot.mk Setoid.r b ∨
    Quot.mk Setoid.r b ≤ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
obtain ⟨xb, yb, hyb, rfl⟩ : ∃ a b : A, _ := IsFractionRing.div_surjective b
case mk.mk.intro.intro.intro.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this : ↑(algebraMap A K) ya ≠ 0
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
case mk.mk.intro.intro.intro.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
have : (algebraMap A K) ya ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hya
case mk.mk.intro.intro.intro.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
case mk.mk.intro.intro.intro.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this : ↑(algebraMap A K) ya ≠ 0
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
have : (algebraMap A K) yb ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hyb
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)

case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
case mk.mk.intro.intro.intro.intro.intro.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
obtain ⟨c, h | h⟩ := ValuationRing.cond (xa * yb) (xb * ya)
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
    Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
right
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ c • (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) = ↑(algebraMap A K) xb / ↑(algebraMap A K) yb
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
    Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
use c
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ ↑(algebraMap A K) c * (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) = ↑(algebraMap A K) xb / ↑(algebraMap A K) yb
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ c • (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) = ↑(algebraMap A K) xb / ↑(algebraMap A K) yb
rw [Algebra.smul_def]
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ ↑(algebraMap A K) c * ↑(algebraMap A K) xa * ↑(algebraMap A K) yb = ↑(algebraMap A K) xb * ↑(algebraMap A K) ya
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ ↑(algebraMap A K) c * (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) = ↑(algebraMap A K) xb / ↑(algebraMap A K) yb
field_simp
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ ↑(algebraMap A K) (c * xa * yb) = ↑(algebraMap A K) (xa * yb * c)
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ ↑(algebraMap A K) c * ↑(algebraMap A K) xa * ↑(algebraMap A K) yb = ↑(algebraMap A K) xb * ↑(algebraMap A K) ya
simp only [← RingHom.map_mul, ← h]
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h.h.e_6.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ c * xa * yb = xa * yb * c
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ ↑(algebraMap A K) (c * xa * yb) = ↑(algebraMap A K) (xa * yb * c)
congr 1
no goals
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inl.h.h.e_6.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xa * yb * c = xb * ya
⊢ c * xa * yb = xa * yb * c
ring
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb)
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ∨
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) ≤
      Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya)
left
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ c • (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) = ↑(algebraMap A K) xa / ↑(algebraMap A K) ya
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ Quot.mk Setoid.r (↑(algebraMap A K) xa / ↑(algebraMap A K) ya) ≤
    Quot.mk Setoid.r (↑(algebraMap A K) xb / ↑(algebraMap A K) yb)
use c
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ ↑(algebraMap A K) c * (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) = ↑(algebraMap A K) xa / ↑(algebraMap A K) ya
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ c • (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) = ↑(algebraMap A K) xa / ↑(algebraMap A K) ya
rw [Algebra.smul_def]
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ ↑(algebraMap A K) c * ↑(algebraMap A K) xb * ↑(algebraMap A K) ya = ↑(algebraMap A K) xa * ↑(algebraMap A K) yb
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ ↑(algebraMap A K) c * (↑(algebraMap A K) xb / ↑(algebraMap A K) yb) = ↑(algebraMap A K) xa / ↑(algebraMap A K) ya
field_simp
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ ↑(algebraMap A K) (c * xb * ya) = ↑(algebraMap A K) (xb * ya * c)
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ ↑(algebraMap A K) c * ↑(algebraMap A K) xb * ↑(algebraMap A K) ya = ↑(algebraMap A K) xa * ↑(algebraMap A K) yb
simp only [← RingHom.map_mul, ← h]
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h.h.e_6.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ c * xb * ya = xb * ya * c
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ ↑(algebraMap A K) (c * xb * ya) = ↑(algebraMap A K) (xb * ya * c)
congr 1
no goals
case mk.mk.intro.intro.intro.intro.intro.intro.intro.inr.h.h.e_6.h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
a b : ValueGroup A K
xa ya : A
hya : ya ∈ nonZeroDivisors A
xb yb : A
hyb : yb ∈ nonZeroDivisors A
this✝ : ↑(algebraMap A K) ya ≠ 0
this : ↑(algebraMap A K) yb ≠ 0
c : A
h : xb * ya * c = xa * yb
⊢ c * xb * ya = xb * ya * c
ring