case intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : ValuationRing R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hf : Function.Surjective ↑f
a b : R
⊢ ∃ c, ↑f a * c = ↑f b ∨ ↑f b * c = ↑f a
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : ValuationRing R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hf : Function.Surjective ↑f
a b : S
⊢ ∃ c, a * c = b ∨ b * c = a
obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := hf a, hf b
case intro.intro.intro.inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : ValuationRing R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hf : Function.Surjective ↑f
a c : R
⊢ ∃ c_1, ↑f a * c_1 = ↑f (a * c) ∨ ↑f (a * c) * c_1 = ↑f a

case intro.intro.intro.inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : ValuationRing R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hf : Function.Surjective ↑f
b c : R
⊢ ∃ c_1, ↑f (b * c) * c_1 = ↑f b ∨ ↑f b * c_1 = ↑f (b * c)
case intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : ValuationRing R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hf : Function.Surjective ↑f
a b : R
⊢ ∃ c, ↑f a * c = ↑f b ∨ ↑f b * c = ↑f a
obtain ⟨c, rfl | rfl⟩ := ValuationRing.cond a b
no goals
case intro.intro.intro.inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : ValuationRing R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hf : Function.Surjective ↑f
a c : R
⊢ ∃ c_1, ↑f a * c_1 = ↑f (a * c) ∨ ↑f (a * c) * c_1 = ↑f a

case intro.intro.intro.inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : ValuationRing R
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R →+* S
hf : Function.Surjective ↑f
b c : R
⊢ ∃ c_1, ↑f (b * c) * c_1 = ↑f b ∨ ↑f b * c_1 = ↑f (b * c)
exacts [⟨f c, Or.inl <| (map_mul _ _ _).symm⟩, ⟨f c, Or.inr <| (map_mul _ _ _).symm⟩]