Theorem: QuadRing.eq_top_of_min_eq_top (ECTate/Algebra/QuadRing/Valuations.lean)

State before:
a b : ℕ∞
⊢ min a b = ⊤ → a = ⊤
Tactic:
sorry
State after:
no goals