Theorem: wordForSwap_eq_swap (Bruhat/Word.lean)

State before:
i k : ℕ
⊢ Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
Tactic:
induction' k with k ih
State after:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i Nat.zero) = Equiv.swap i (i + (Nat.zero + 1))

case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))

State before:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i Nat.zero) = Equiv.swap i (i + (Nat.zero + 1))

case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
. simp only [Nat.zero_eq, add_zero, Equiv.swap_self]
  rfl
State after:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))

State before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
. rw [WordForSwap_toPerm_succ, ih]
  change _ * _ * (Equiv.swap _ _)⁻¹ = _
  rw [← Equiv.swap_apply_apply, Equiv.swap_apply_left,
      Equiv.swap_apply_of_ne_of_ne (by simp) (by simp)]
State after:
no goals

State before:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i Nat.zero) = Equiv.swap i (i + (Nat.zero + 1))
Tactic:
simp only [Nat.zero_eq, add_zero, Equiv.swap_self]
State after:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i 0) = Equiv.swap i (i + (0 + 1))

State before:
case zero
i : ℕ
⊢ Word.toPerm (WordForSwap i 0) = Equiv.swap i (i + (0 + 1))
Tactic:
rfl
State after:
no goals

State before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Word.toPerm (WordForSwap i (Nat.succ k)) = Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
rw [WordForSwap_toPerm_succ, ih]
State after:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * Equiv.swap (i + (k + 1)) (i + (k + 2)) =
    Equiv.swap i (i + (Nat.succ k + 1))

State before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * Equiv.swap (i + (k + 1)) (i + (k + 2)) =
    Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
change _ * _ * (Equiv.swap _ _)⁻¹ = _
State after:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * (Equiv.swap (i + (k + 1)) (i + (k + 2)))⁻¹ =
    Equiv.swap i (i + (Nat.succ k + 1))

State before:
case succ
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ Equiv.swap (i + (k + 1)) (i + (k + 2)) * Equiv.swap i (i + (k + 1)) * (Equiv.swap (i + (k + 1)) (i + (k + 2)))⁻¹ =
    Equiv.swap i (i + (Nat.succ k + 1))
Tactic:
rw [← Equiv.swap_apply_apply, Equiv.swap_apply_left,
    Equiv.swap_apply_of_ne_of_ne (by simp) (by simp)]
State after:
no goals

State before:
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ i ≠ i + (k + 1)
Tactic:
simp
State after:
no goals

State before:
i k : ℕ
ih : Word.toPerm (WordForSwap i k) = Equiv.swap i (i + (k + 1))
⊢ i ≠ i + (k + 2)
Tactic:
simp
State after:
no goals