Theorem: not_mem_stdinversions_diag (Bruhat/Word.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a : α
⊢ (a, a) ∉ StdInversions g
Tactic:
simp [mem_stdinversions']
State after:
no goals