Theorem: inversions_comp (Bruhat/Word.lean)

State before:
f g : Equiv.Perm ℕ
⊢ Inversions (f * g) = (⇑(Equiv.prodCongr g g) ⁻¹' Inversions f) ∆ Inversions g
Tactic:
ext ⟨a, b⟩
State after:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔ (a, b) ∈ (⇑(Equiv.prodCongr g g) ⁻¹' Inversions f) ∆ Inversions g

State before:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔ (a, b) ∈ (⇑(Equiv.prodCongr g g) ⁻¹' Inversions f) ∆ Inversions g
Tactic:
simp only [Set.mem_symmDiff, Set.mem_preimage, Equiv.prodCongr_apply, Prod.map]
State after:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

State before:
case h.mk
f g : Equiv.Perm ℕ
a b : ℕ
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
wlog h : a < b
State after:
case h.mk.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

State before:
case h.mk.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. cases' (le_of_not_lt h).eq_or_lt with h' h'
  . simp [h', not_mem_inversions_diag]
  . repeat simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
    exact this f g _ _ h'
State after:
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

State before:
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
cases' lt_or_le (g a) (g b) with hgab hgba
State after:
case inl
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgab : g a < g b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

State before:
case inl
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgab : g a < g b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. simp [mem_inversions', Set.mem_symmDiff, h, hgab, hgab.not_le]
State after:
case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

State before:
case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. simp [mem_inversions', Set.mem_symmDiff, h, hgba, hgba.not_lt]
State after:
no goals

State before:
case h.mk.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
cases' (le_of_not_lt h).eq_or_lt with h' h'
State after:
case h.mk.inr.inl
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b = a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

State before:
case h.mk.inr.inl
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b = a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. simp [h', not_mem_inversions_diag]
State after:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f

State before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
. repeat simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
  exact this f g _ _ h'
State after:
no goals

State before:
case h.mk.inr.inl
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b = a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp [h', not_mem_inversions_diag]
State after:
no goals

State before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
repeat simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
State after:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (b, a) ∈ Inversions (f * g) ↔
    (g b, g a) ∈ Inversions f ∧ (b, a) ∉ Inversions g ∨ (b, a) ∈ Inversions g ∧ (g b, g a) ∉ Inversions f

State before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (b, a) ∈ Inversions (f * g) ↔
    (g b, g a) ∈ Inversions f ∧ (b, a) ∉ Inversions g ∨ (b, a) ∈ Inversions g ∧ (g b, g a) ∉ Inversions f
Tactic:
exact this f g _ _ h'
State after:
no goals

State before:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp_rw [mem_inversions_symm _ a b, mem_inversions_symm _ (g a) (g b)]
State after:
case h.mk.inr.inr
f g : Equiv.Perm ℕ
a b : ℕ
this :
  ∀ (f g : Equiv.Perm ℕ) (a b : ℕ),
    a < b →
      ((a, b) ∈ Inversions (f * g) ↔
        (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f)
h : ¬a < b
h' : b < a
⊢ (b, a) ∈ Inversions (f * g) ↔
    (g b, g a) ∈ Inversions f ∧ (b, a) ∉ Inversions g ∨ (b, a) ∈ Inversions g ∧ (g b, g a) ∉ Inversions f

State before:
case inl
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgab : g a < g b
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp [mem_inversions', Set.mem_symmDiff, h, hgab, hgab.not_le]
State after:
no goals

State before:
case inr
f g : Equiv.Perm ℕ
a b : ℕ
h : a < b
hgba : g b ≤ g a
⊢ (a, b) ∈ Inversions (f * g) ↔
    (g a, g b) ∈ Inversions f ∧ (a, b) ∉ Inversions g ∨ (a, b) ∈ Inversions g ∧ (g a, g b) ∉ Inversions f
Tactic:
simp [mem_inversions', Set.mem_symmDiff, h, hgba, hgba.not_lt]
State after:
no goals