Theorem: swapHasWord (Bruhat/Word.lean)

State before:
i j : ℕ
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
cases' le_or_lt i j with h h
State after:
case inl
i j : ℕ
h : i ≤ j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)

State before:
case inl
i j : ℕ
h : i ≤ j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
cases' h.eq_or_lt with h h
State after:
case inl.inl
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ RepbleByWord (Equiv.swap i j)

case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)

State before:
case inl.inl
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ RepbleByWord (Equiv.swap i j)

case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
. use []
  rw [idHasWord, h, Equiv.swap_self]
  rfl
State after:
case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)

State before:
case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)

case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
. obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
  use WordForSwap i k
  rw [wordForSwap_eq_swap, add_assoc]
State after:
case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)

State before:
case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
. obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
  use WordForSwap j k
  rw [wordForSwap_eq_swap, add_assoc, Equiv.swap_comm]
State after:
no goals

State before:
case inl.inl
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
use []
State after:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ Word.toPerm [] = Equiv.swap i j

State before:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ Word.toPerm [] = Equiv.swap i j
Tactic:
rw [idHasWord, h, Equiv.swap_self]
State after:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ 1 = Equiv.refl ℕ

State before:
case h
i j : ℕ
h✝ : i ≤ j
h : i = j
⊢ 1 = Equiv.refl ℕ
Tactic:
rfl
State after:
no goals

State before:
case inl.inr
i j : ℕ
h✝ : i ≤ j
h : i < j
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
State after:
case inl.inr.intro
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ RepbleByWord (Equiv.swap i (i + k + 1))

State before:
case inl.inr.intro
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ RepbleByWord (Equiv.swap i (i + k + 1))
Tactic:
use WordForSwap i k
State after:
case h
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ Word.toPerm (WordForSwap i k) = Equiv.swap i (i + k + 1)

State before:
case h
i k : ℕ
h✝ : i ≤ i + k + 1
h : i < i + k + 1
⊢ Word.toPerm (WordForSwap i k) = Equiv.swap i (i + k + 1)
Tactic:
rw [wordForSwap_eq_swap, add_assoc]
State after:
no goals

State before:
case inr
i j : ℕ
h : j < i
⊢ RepbleByWord (Equiv.swap i j)
Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h
State after:
case inr.intro
j k : ℕ
h : j < j + k + 1
⊢ RepbleByWord (Equiv.swap (j + k + 1) j)

State before:
case inr.intro
j k : ℕ
h : j < j + k + 1
⊢ RepbleByWord (Equiv.swap (j + k + 1) j)
Tactic:
use WordForSwap j k
State after:
case h
j k : ℕ
h : j < j + k + 1
⊢ Word.toPerm (WordForSwap j k) = Equiv.swap (j + k + 1) j

State before:
case h
j k : ℕ
h : j < j + k + 1
⊢ Word.toPerm (WordForSwap j k) = Equiv.swap (j + k + 1) j
Tactic:
rw [wordForSwap_eq_swap, add_assoc, Equiv.swap_comm]
State after:
no goals