Theorem: mem_support_of_inversion (Bruhat/Word.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : (a, b) ∈ Inversions g
⊢ a ∈ support g ∨ b ∈ support g
Tactic:
simp only [mem_inversions', support, ne_eq, Set.mem_setOf_eq] at hab ⊢
State after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
⊢ ¬g a = a ∨ ¬g b = b

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
⊢ ¬g a = a ∨ ¬g b = b
Tactic:
by_contra! hab'
State after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
hab' : g a = a ∧ g b = b
⊢ False

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : a < b ↔ g b ≤ g a
hab' : g a = a ∧ g b = b
⊢ False
Tactic:
rw [hab'.1, hab'.2, ← not_le] at hab
State after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬b ≤ a ↔ b ≤ a
hab' : g a = a ∧ g b = b
⊢ False

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
hab : ¬b ≤ a ↔ b ≤ a
hab' : g a = a ∧ g b = b
⊢ False
Tactic:
exact not_iff_self hab
State after:
no goals