internlm/Lean-Github huggingface dataset:
Theorem: Permutation.get_castAdd_lt
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]
Tactic:
rewrite [Array.getElem_append_left _ _ ((Array.size_map _ _).symm ▸ this)]
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val)[i] = Fin.castAdd m x.val[i]
Theorem: Permutation.get_castAdd_lt
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val)[i] = Fin.castAdd m x.val[i]
Tactic:
rw [Array.getElem_map]
Proof state after:
no goals
Theorem: Permutation.get_castAdd_ge
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
⊢ (castAdd m x)[i] = { val := i, isLt := hi }
Tactic:
unfold castAdd GetElem.getElem
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
⊢ instGetElemPermutationNatFinLtInstLTNat.1
      { val := Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n),
        size_eq :=
          (_ :
            Array.size
                (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n)) =
              n + m),
        nodup :=
          (_ :
            Array.Nodup
              (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))) }
      i hi =
    { val := i, isLt := hi }
Theorem: Permutation.get_castAdd_ge
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
⊢ instGetElemPermutationNatFinLtInstLTNat.1
      { val := Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n),
        size_eq :=
          (_ :
            Array.size
                (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n)) =
              n + m),
        nodup :=
          (_ :
            Array.Nodup
              (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))) }
      i hi =
    { val := i, isLt := hi }
Tactic:
simp only [instGetElemPermutationNatFinLtInstLTNat]
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    { val := i, isLt := hi }
Theorem: Permutation.get_castAdd_ge
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    { val := i, isLt := hi }
Tactic:
have : i ≥ x.val.size := x.size_eq.symm ▸ h
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    { val := i, isLt := hi }
Theorem: Permutation.get_castAdd_ge
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    { val := i, isLt := hi }
Tactic:
rewrite [Array.getElem_append_right _ _ ((Array.size_map _ _).symm ▸ this)]
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ (Array.ofFn fun i =>
        Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i - Array.size (Array.map (Fin.castAdd m) x.val)] =
    { val := i, isLt := hi }
Theorem: Permutation.get_castAdd_ge
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ (Array.ofFn fun i =>
        Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i - Array.size (Array.map (Fin.castAdd m) x.val)] =
    { val := i, isLt := hi }
Tactic:
rewrite [Array.getElem_ofFn]
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ Fin.cast (_ : m + n = n + m)
      (Fin.addNat
        { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
          isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
        n) =
    { val := i, isLt := hi }
Theorem: Permutation.get_castAdd_ge
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ Fin.cast (_ : m + n = n + m)
      (Fin.addNat
        { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
          isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
        n) =
    { val := i, isLt := hi }
Tactic:
apply Fin.eq_of_val_eq
Proof state after:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ ↑(Fin.cast (_ : m + n = n + m)
        (Fin.addNat
          { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
            isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
          n)) =
    ↑{ val := i, isLt := hi }
Theorem: Permutation.get_castAdd_ge
Proof state before:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ ↑(Fin.cast (_ : m + n = n + m)
        (Fin.addNat
          { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
            isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
          n)) =
    ↑{ val := i, isLt := hi }
Tactic:
simp only [Array.size_map, Fin.addNat_mk, Fin.cast_mk, x.size_eq]
Proof state after:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ i - n + n = i
Theorem: Permutation.get_castAdd_ge
Proof state before:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ i - n + n = i
Tactic:
exact Nat.sub_add_cancel h
Proof state after:
no goals
Theorem: Permutation.get_castAdd_ite
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
Tactic:
if h : i < n then
  rewrite [dif_pos h]; exact x.get_castAdd_lt m i h
else
  rewrite [dif_neg h]; exact x.get_castAdd_ge m i (Nat.le_of_not_lt h)
Proof state after:
no goals
Theorem: Permutation.get_castAdd_ite
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
Tactic:
rewrite [dif_pos h]
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = Fin.castAdd m x[i]
Theorem: Permutation.get_castAdd_ite
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = Fin.castAdd m x[i]
Tactic:
exact x.get_castAdd_lt m i h
Proof state after:
no goals
Theorem: Permutation.get_castAdd_ite
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : ¬i < n
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
Tactic:
rewrite [dif_neg h]
Proof state after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : ¬i < n
⊢ (castAdd m x)[i] = { val := i, isLt := hi }
Theorem: Permutation.get_castAdd_ite
Proof state before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : ¬i < n
⊢ (castAdd m x)[i] = { val := i, isLt := hi }
Tactic:
exact x.get_castAdd_ge m i (Nat.le_of_not_lt h)
Proof state after:
no goals
Theorem: Permutation.one_mul
Proof state before:
n : Nat
x : Permutation n
i : Nat
hi : i < n
⊢ (1 * x)[i] = x[i]
Tactic:
rw [get_mul, get_one]
Proof state after:
no goals
Theorem: Permutation.mul_one
Proof state before:
n : Nat
x : Permutation n
i : Nat
hi : i < n
⊢ (x * 1)[i] = x[i]
Tactic:
rw [get_mul, get_one]
Proof state after:
no goals
Theorem: Permutation.mul_assoc
Proof state before:
n : Nat
x y z : Permutation n
i : Nat
hi : i < n
⊢ (x * y * z)[i] = (x * (y * z))[i]
Tactic:
simp only [get_mul]
Proof state after:
no goals
Theorem: Permutation.inv_mul
Proof state before:
n : Nat
x : Permutation n
⊢ toFun (inv x * x) = toFun 1
Tactic:
funext i
Proof state after:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (inv x * x) i = toFun 1 i
Theorem: Permutation.inv_mul
Proof state before:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (inv x * x) i = toFun 1 i
Tactic:
simp only [toFun_mul, toFun_one]
Proof state after:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ (toFun (inv x) ∘ toFun x) i = id i
Theorem: Permutation.inv_mul
Proof state before:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ (toFun (inv x) ∘ toFun x) i = id i
Tactic:
exact toFun_inv_toFun x i
Proof state after:
no goals
Theorem: Permutation.mul_inv
Proof state before:
n : Nat
x : Permutation n
⊢ toFun (x * inv x) = toFun 1
Tactic:
funext i
Proof state after:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (x * inv x) i = toFun 1 i
Theorem: Permutation.mul_inv
Proof state before:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (x * inv x) i = toFun 1 i
Tactic:
simp only [toFun_mul, toFun_one]
Proof state after:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ (toFun x ∘ toFun (inv x)) i = id i
Theorem: Permutation.mul_inv
Proof state before:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ (toFun x ∘ toFun (inv x)) i = id i
Tactic:
exact toFun_toFun_inv x i
Proof state after:
no goals
Theorem: Permutation.mul_left_cancel
Proof state before:
n : Nat
x y z : Permutation n
h : x * y = x * z
this : (fun x_1 => inv x * x_1) (x * y) = (fun x_1 => inv x * x_1) (x * z)
⊢ y = z
Tactic:
conv at this =>
  dsimp; simp only [← mul_assoc, inv_mul, one_mul]
Proof state after:
n : Nat
x y z : Permutation n
h : x * y = x * z
this : y = z
⊢ y = z
Theorem: Permutation.mul_left_cancel
Proof state before:
n : Nat
x y z : Permutation n
h : x * y = x * z
this : y = z
⊢ y = z
Tactic:
exact this
Proof state after:
no goals
Theorem: Permutation.mul_right_cancel
Proof state before:
n : Nat
x y z : Permutation n
h : x * z = y * z
this : (fun x => x * inv z) (x * z) = (fun x => x * inv z) (y * z)
⊢ x = y
Tactic:
conv at this =>
  dsimp; simp only [mul_assoc, mul_inv, mul_one]
Proof state after:
n : Nat
x y z : Permutation n
h : x * z = y * z
this : x = y
⊢ x = y
Theorem: Permutation.mul_right_cancel
Proof state before:
n : Nat
x y z : Permutation n
h : x * z = y * z
this : x = y
⊢ x = y
Tactic:
exact this
Proof state after:
no goals
Theorem: Permutation.mul_inv_eq_of_eq_mul
Proof state before:
n : Nat
x y z : Permutation n
h : x = z * y
this : (fun x => x * inv y) x = (fun x => x * inv y) (z * y)
⊢ x * inv y = z
Tactic:
conv at this => dsimp; rewrite [mul_assoc, mul_inv, mul_one]
Proof state after:
n : Nat
x y z : Permutation n
h : x = z * y
this : x * inv y = z
⊢ x * inv y = z
Theorem: Permutation.mul_inv_eq_of_eq_mul
Proof state before:
n : Nat
x y z : Permutation n
h : x = z * y
this : x * inv y = z
⊢ x * inv y = z
Tactic:
exact this
Proof state after:
no goals
Theorem: Permutation.inv_mul_eq_of_mul_eq
Proof state before:
n : Nat
x y z : Permutation n
h : y * x = z
this : (fun x => inv y * x) (y * x) = (fun x => inv y * x) z
⊢ x = inv y * z
Tactic:
conv at this => dsimp; rewrite [← mul_assoc, inv_mul, one_mul]
Proof state after:
n : Nat
x y z : Permutation n
h : y * x = z
this : x = inv y * z
⊢ x = inv y * z
Theorem: Permutation.inv_mul_eq_of_mul_eq
Proof state before:
n : Nat
x y z : Permutation n
h : y * x = z
this : x = inv y * z
⊢ x = inv y * z
Tactic:
exact this
Proof state after:
no goals
Theorem: Permutation.eq_inv_of_mul_eq_left
Proof state before:
n : Nat
x y : Permutation n
h : x * y = 1
this : (fun x_1 => inv x * x_1) (x * y) = (fun x_1 => inv x * x_1) 1
⊢ y = inv x
Tactic:
conv at this =>
  dsimp; rewrite [← mul_assoc, inv_mul, one_mul, mul_one]
Proof state after:
n : Nat
x y : Permutation n
h : x * y = 1
this : y = inv x
⊢ y = inv x
Theorem: Permutation.eq_inv_of_mul_eq_left
Proof state before:
n : Nat
x y : Permutation n
h : x * y = 1
this : y = inv x
⊢ y = inv x
Tactic:
exact this
Proof state after:
no goals
Theorem: Permutation.eq_inv_of_mul_eq_right
Proof state before:
n : Nat
x y : Permutation n
h : x * y = 1
this : (fun x => x * inv y) (x * y) = (fun x => x * inv y) 1
⊢ x = inv y
Tactic:
conv at this =>
  dsimp; rewrite [mul_assoc, mul_inv, one_mul, mul_one]
Proof state after:
n : Nat
x y : Permutation n
h : x * y = 1
this : x = inv y
⊢ x = inv y
Theorem: Permutation.eq_inv_of_mul_eq_right
Proof state before:
n : Nat
x y : Permutation n
h : x * y = 1
this : x = inv y
⊢ x = inv y
Tactic:
exact this
Proof state after:
no goals
Theorem: Permutation.powNat_add
Proof state before:
n : Nat
x : Permutation n
k l : Nat
⊢ x ^ (k + l) = x ^ k * x ^ l
Tactic:
induction k with
| zero =>
  simp only [Nat.zero_eq, Nat.zero_add, powNat_zero, one_mul]
| succ k IH =>
  simp only [Nat.succ_add, powNat_succ]
  rw [mul_assoc, IH]
Proof state after:
no goals
Theorem: Permutation.powNat_add
Proof state before:
case zero
n : Nat
x : Permutation n
l : Nat
⊢ x ^ (Nat.zero + l) = x ^ Nat.zero * x ^ l
Tactic:
simp only [Nat.zero_eq, Nat.zero_add, powNat_zero, one_mul]
Proof state after:
no goals
Theorem: Permutation.powNat_add
Proof state before:
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x ^ (Nat.succ k + l) = x ^ Nat.succ k * x ^ l
Tactic:
simp only [Nat.succ_add, powNat_succ]
Proof state after:
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x * x ^ (k + l) = x * x ^ k * x ^ l
Theorem: Permutation.powNat_add
Proof state before:
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x * x ^ (k + l) = x * x ^ k * x ^ l
Tactic:
rw [mul_assoc, IH]
Proof state after:
no goals
Theorem: Permutation.get_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (Array.swap x.val (Fin.cast (_ : n = Array.size x.val) i) (Fin.cast (_ : n = Array.size x.val) j))[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
simp only [Array.getElem_swap, Fin.cast]
Proof state after:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then x.val[↑i] else if ↑i = k then x.val[↑j] else x.val[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Theorem: Permutation.get_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then x.val[↑i] else if ↑i = k then x.val[↑j] else x.val[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rfl
Proof state after:
no goals
Theorem: Permutation.swap_swap_same
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (swap (swap x i j) i j)[k] = x[k]
Tactic:
simp only [get_swap, if_pos]
Proof state after:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Theorem: Permutation.swap_swap_same
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Tactic:
apply dite (j.1 = k) <;> apply dite (i.1 = k) <;> intro hik hjk
Proof state after:
case t.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Theorem: Permutation.swap_swap_same
Proof state before:
case t.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Tactic:
all_goals simp only [hik, hjk, if_pos, if_neg]
Proof state after:
case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if k = ↑i then x[↑i] else x[k]) = x[k]
Theorem: Permutation.swap_swap_same
Proof state before:
case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if k = ↑i then x[↑i] else x[k]) = x[k]
Tactic:
rw [if_neg (Ne.symm hik)]
Proof state after:
no goals
Theorem: Permutation.swap_swap_same
Proof state before:
case e.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
Tactic:
simp only [hik, hjk, if_pos, if_neg]
Proof state after:
no goals
Theorem: Permutation.get_transpos
Proof state before:
n : Nat
i j : Fin n
k : Nat
hk : k < n
⊢ (transpos i j)[k] = if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk }
Tactic:
simp only [transpos, get_swap, get_one]
Proof state after:
no goals
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (x * transpos i j)[k] = (swap x i j)[k]
Tactic:
simp only [get_mul, get_transpos, get_swap]
Proof state after:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
if hjk : j.1 = k then
  cases hjk; simp only [if_pos]
else if hik : i.1 = k then
  cases hik; simp only [if_neg hjk, if_pos]
else
  simp only [if_neg hjk, if_neg hik]
Proof state after:
no goals
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin 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 ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
cases hjk
Proof state after:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑j < n
⊢ x[↑(if ↑j = ↑j then i else if ↑i = ↑j then j else { val := ↑j, isLt := hk })] =
    if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑j < n
⊢ x[↑(if ↑j = ↑j then i else if ↑i = ↑j then j else { val := ↑j, isLt := hk })] =
    if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]
Tactic:
simp only [if_pos]
Proof state after:
no goals
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin 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 ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
if hik : i.1 = k then
cases hik; simp only [if_neg hjk, if_pos]
else
simp only [if_neg hjk, if_neg hik]
Proof state after:
no goals
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hjk : ¬↑j = k
hik : ↑i = k
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
cases hik
Proof state after:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑i < n
hjk : ¬↑j = ↑i
⊢ x[↑(if ↑j = ↑i then i else if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑j = ↑i then x[↑i] else if ↑i = ↑i then x[↑j] else x[↑i]
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑i < n
hjk : ¬↑j = ↑i
⊢ x[↑(if ↑j = ↑i then i else if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑j = ↑i then x[↑i] else if ↑i = ↑i then x[↑j] else x[↑i]
Tactic:
simp only [if_neg hjk, if_pos]
Proof state after:
no goals
Theorem: Permutation.mul_transpose_eq_swap
Proof state before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
simp only [if_neg hjk, if_neg hik]
Proof state after:
no goals
Theorem: Permutation.transpos_mul_transpos_same
Proof state before:
n : Nat
i j : Fin n
⊢ transpos i j * transpos i j = 1
Tactic:
rewrite [mul_transpose_eq_swap]
Proof state after:
n : Nat
i j : Fin n
⊢ swap (transpos i j) i j = 1
Theorem: Permutation.transpos_mul_transpos_same
Proof state before:
n : Nat
i j : Fin n
⊢ swap (transpos i j) i j = 1
Tactic:
dsimp [transpos]
Proof state after:
n : Nat
i j : Fin n
⊢ swap (swap 1 i j) i j = 1
Theorem: Permutation.transpos_mul_transpos_same
Proof state before:
n : Nat
i j : Fin n
⊢ swap (swap 1 i j) i j = 1
Tactic:
exact swap_swap_same 1 i j
Proof state after:
no goals
Theorem: Permutation.transpos_conj
Proof 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]
Proof 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) }
Theorem: Permutation.transpos_conj
Proof 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]
Proof state after:
no goals
Theorem: Permutation.transpos_conj
Proof 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
Proof 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) }