Theorem: mem_inversions_symm (Bruhat/Word.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a, b) ∈ Inversions g ↔ (b, a) ∈ Inversions g
Tactic:
simp only [mem_inversions']
State after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
wlog h : a < b
State after:
case inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

State before:
case inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
. cases' eq_or_lt_of_le (le_of_not_lt h) with h' h'
  . simp [h']
  . rw [this _ _ _ h']
State after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
have h' : g a ≠ g b := fun hg => h.ne (g.injective hg)
State after:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
h' : g a ≠ g b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

State before:
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
h : a < b
h' : g a ≠ g b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
simp [h, h.not_lt, h'.symm.le_iff_lt]
State after:
no goals

State before:
case inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
cases' eq_or_lt_of_le (le_of_not_lt h) with h' h'
State after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b = a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

State before:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b = a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
. simp [h']
State after:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)

State before:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
. rw [this _ _ _ h']
State after:
no goals

State before:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b = a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
simp [h']
State after:
no goals

State before:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
g : Equiv.Perm α
a b : α
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] (g : Equiv.Perm α) (a b : α),
    a < b → ((a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b))
h : ¬a < b
h' : b < a
⊢ (a < b ↔ g b ≤ g a) ↔ (b < a ↔ g a ≤ g b)
Tactic:
rw [this _ _ _ h']
State after:
no goals