Theorem: mem_inversions (Bruhat/Word.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
p : α × α
⊢ p ∈ Inversions g ↔ (p.1 < p.2 ↔ g p.2 ≤ g p.1)
Tactic:
rfl
State after:
no goals