case refine_1
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.522037
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
a b : R
⊢ a ∣ b ∨ b ∣ a

case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.522037
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal R fun x x_1 => x ∣ x_1
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.522037
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ValuationRing R ↔ IsTotal R fun x x_1 => x ∣ x_1
refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩
no goals
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.522037
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : ValuationRing R
a b : R
⊢ a ∣ b ∨ b ∣ a
obtain ⟨c, rfl | rfl⟩ := ValuationRing.cond a b <;> simp
no goals
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type ?u.522037
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
H : IsTotal R fun x x_1 => x ∣ x_1
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a
obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := @IsTotal.total _ _ H a b <;> use c <;> simp