Theorem: mem_stdinversions (Bruhat/Word.lean)

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