Theorem: Permutation.transpos_conj (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
⊢ (x * transpos i j)[k] = (transpos x[↑i] x[↑j] * x)[k]
Tactic:
simp only [get_mul, get_transpos]
State after:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
if hjk : j.1 = k then
  cases hjk; simp only [if_pos]
else
  have : x[j.1].1 ≠ x[k].1 :=
    fun h => hjk <| x.get_inj _ _ (Fin.eq_of_val_eq h)
  simp only [hjk, this, if_neg]
  if hik : i.1 = k then
    cases hik; simp only [if_pos]
  else
    have : x[i.1].1 ≠ x[k].1 :=
      fun h => hik <| x.get_inj _ _ (Fin.eq_of_val_eq h)
    simp only [hik, this, if_neg]
State after:
no goals

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ↑j = k
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
cases hjk
State after:
case refl
n : Nat
i j : Fin n
x : Permutation n
hk : ↑j < n
⊢ x[↑(if ↑j = ↑j then i else if ↑i = ↑j then j else { val := ↑j, isLt := hk })] =
    if ↑x[↑j] = ↑x[↑j] then x[↑i] else if ↑x[↑i] = ↑x[↑j] then x[↑j] else { val := ↑x[↑j], isLt := (_ : ↑x[↑j] < n) }

State before:
case refl
n : Nat
i j : Fin n
x : Permutation n
hk : ↑j < n
⊢ x[↑(if ↑j = ↑j then i else if ↑i = ↑j then j else { val := ↑j, isLt := hk })] =
    if ↑x[↑j] = ↑x[↑j] then x[↑i] else if ↑x[↑i] = ↑x[↑j] then x[↑j] else { val := ↑x[↑j], isLt := (_ : ↑x[↑j] < n) }
Tactic:
simp only [if_pos]
State after:
no goals

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
have : x[j.1].1 ≠ x[k].1 :=
  fun h => hjk <| x.get_inj _ _ (Fin.eq_of_val_eq h)
State after:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑j] = ↑x[k] then x[↑i] else if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
simp only [hjk, this, if_neg]
State after:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
if hik : i.1 = k then
  cases hik; simp only [if_pos]
else
  have : x[i.1].1 ≠ x[k].1 :=
    fun h => hik <| x.get_inj _ _ (Fin.eq_of_val_eq h)
  simp only [hik, this, if_neg]
State after:
no goals

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
hik : ↑i = k
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
cases hik
State after:
case refl
n : Nat
i j : Fin n
x : Permutation n
hk : ↑i < n
hjk : ¬↑j = ↑i
this : ↑x[↑j] ≠ ↑x[↑i]
⊢ x[↑(if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑x[↑i] = ↑x[↑i] then x[↑j] else { val := ↑x[↑i], isLt := (_ : ↑x[↑i] < n) }

State before:
case refl
n : Nat
i j : Fin n
x : Permutation n
hk : ↑i < n
hjk : ¬↑j = ↑i
this : ↑x[↑j] ≠ ↑x[↑i]
⊢ x[↑(if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑x[↑i] = ↑x[↑i] then x[↑j] else { val := ↑x[↑i], isLt := (_ : ↑x[↑i] < n) }
Tactic:
simp only [if_pos]
State after:
no goals

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
hik : ¬↑i = k
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
have : x[i.1].1 ≠ x[k].1 :=
  fun h => hik <| x.get_inj _ _ (Fin.eq_of_val_eq h)
State after:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this✝ : ↑x[↑j] ≠ ↑x[k]
hik : ¬↑i = k
this : ↑x[↑i] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }

State before:
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this✝ : ↑x[↑j] ≠ ↑x[k]
hik : ¬↑i = k
this : ↑x[↑i] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
Tactic:
simp only [hik, this, if_neg]
State after:
no goals