Theorem: WordForSwap_toPerm_succ (Bruhat/Goal.lean)

State before:
i k : ℕ
⊢ Word.toPerm (WordForSwap i (k + 1)) =
    Equiv.swap (i + (k + 1)) (i + (k + 2)) * Word.toPerm (WordForSwap i k) * Equiv.swap (i + (k + 1)) (i + (k + 2))
Tactic:
simp [WordForSwap, Word.toPerm]
State after:
i k : ℕ
⊢ Equiv.swap (i + k + 1) (i + k + 1 + 1) *
      (List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
        Equiv.swap (i + k + 1) (i + k + 1 + 1)) =
    Equiv.swap (i + (k + 1)) (i + (k + 2)) * List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
      Equiv.swap (i + (k + 1)) (i + (k + 2))

State before:
i k : ℕ
⊢ Equiv.swap (i + k + 1) (i + k + 1 + 1) *
      (List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
        Equiv.swap (i + k + 1) (i + k + 1 + 1)) =
    Equiv.swap (i + (k + 1)) (i + (k + 2)) * List.prod (List.map (fun i => Equiv.swap i (i + 1)) (WordForSwap i k)) *
      Equiv.swap (i + (k + 1)) (i + (k + 2))
Tactic:
rfl
State after:
no goals