internlm/Lean-Github huggingface dataset:
Theorem: Permutation.sign_mul
Proof state before:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ (inversionNum (x * y) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
rw [← this]
Proof state after:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Theorem: Permutation.sign_mul
Proof state before:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
clear this
Proof state after:
m n : Nat
x y : Permutation n
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Theorem: Permutation.sign_mul
Proof state before:
m n : Nat
x y : Permutation n
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
generalize x.inversionNum = m
Proof state after:
m✝ n : Nat
x y : Permutation n
m : Nat
⊢ ((m % 2 + inversionNum y % 2) % 2 == 1) = ((m % 2 == 1) != (inversionNum y % 2 == 1))
Theorem: Permutation.sign_mul
Proof state before:
m✝ n : Nat
x y : Permutation n
m : Nat
⊢ ((m % 2 + inversionNum y % 2) % 2 == 1) = ((m % 2 == 1) != (inversionNum y % 2 == 1))
Tactic:
generalize y.inversionNum = n
Proof state after:
m✝ n✝ : Nat
x y : Permutation n✝
m n : Nat
⊢ ((m % 2 + n % 2) % 2 == 1) = ((m % 2 == 1) != (n % 2 == 1))
Theorem: Permutation.sign_mul
Proof state before:
m✝ n✝ : Nat
x y : Permutation n✝
m n : Nat
⊢ ((m % 2 + n % 2) % 2 == 1) = ((m % 2 == 1) != (n % 2 == 1))
Tactic:
cases m.mod_two_eq_zero_or_one
  <;> cases n.mod_two_eq_zero_or_one
  <;> rename_i hm hn
  <;> simp only [hm, hn]
Proof state after:
no goals
Theorem: Permutation.sign_inv
Proof state before:
m n : Nat
x : Permutation n
⊢ sign (inv x) = sign x
Tactic:
have : sign (x.inv * x) = sign (1 : Permutation n) := x.inv_mul ▸ rfl
Proof state after:
m n : Nat
x : Permutation n
this : sign (inv x * x) = sign 1
⊢ sign (inv x) = sign x
Theorem: Permutation.sign_inv
Proof state before:
m n : Nat
x : Permutation n
this : sign (inv x * x) = sign 1
⊢ sign (inv x) = sign x
Tactic:
conv at this =>
  simp only [sign_mul, sign_one]
  rewrite [Bool.bne_eq_false]
Proof state after:
m n : Nat
x : Permutation n
this : sign (inv x) = sign x
⊢ sign (inv x) = sign x
Theorem: Permutation.sign_inv
Proof state before:
m n : Nat
x : Permutation n
this : sign (inv x) = sign x
⊢ sign (inv x) = sign x
Tactic:
exact this
Proof state after:
no goals
Theorem: Permutation.sign_powNat_of_even
Proof state before:
m n : Nat
x : Permutation n
k : Nat
h : sign x = false
⊢ sign (x ^ k) = false
Tactic:
induction k with
| zero => rw [powNat_zero, sign_one]
| succ k IH =>
  rewrite [powNat_succ, sign_mul, h, IH]
  decide
Proof state after:
no goals
Theorem: Permutation.sign_powNat_of_even
Proof state before:
case zero
m n : Nat
x : Permutation n
h : sign x = false
⊢ sign (x ^ Nat.zero) = false
Tactic:
rw [powNat_zero, sign_one]
Proof state after:
no goals
Theorem: Permutation.sign_powNat_of_even
Proof state before:
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ sign (x ^ Nat.succ k) = false
Tactic:
rewrite [powNat_succ, sign_mul, h, IH]
Proof state after:
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ (false != false) = false
Theorem: Permutation.sign_powNat_of_even
Proof state before:
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ (false != false) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Permutation.sign_powInt_of_even
Proof state before:
m n : Nat
x : Permutation n
k : Int
h : sign x = false
⊢ sign (x ^ k) = false
Tactic:
rcases k with ⟨k⟩ | ⟨k⟩
Proof state after:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.ofNat k) = false

case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.ofNat k) = false

case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Tactic:
. show sign (x ^ (k : Nat)) = false
  exact sign_powNat_of_even x k h
Proof state after:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Tactic:
. show sign (x.inv ^ (k+1 : Nat)) = false
  apply sign_powNat_of_even
  rewrite [x.sign_inv]
  exact h
Proof state after:
no goals
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.ofNat k) = false
Tactic:
show sign (x ^ (k : Nat)) = false
Proof state after:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ k) = false
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case ofNat
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ k) = false
Tactic:
exact sign_powNat_of_even x k h
Proof state after:
no goals
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
Tactic:
show sign (x.inv ^ (k+1 : Nat)) = false
Proof state after:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x ^ (k + 1)) = false
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x ^ (k + 1)) = false
Tactic:
apply sign_powNat_of_even
Proof state after:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x) = false
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x) = false
Tactic:
rewrite [x.sign_inv]
Proof state after:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign x = false
Theorem: Permutation.sign_powInt_of_even
Proof state before:
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign x = false
Tactic:
exact h
Proof state after:
no goals
Theorem: Permutation.sign_conj
Proof state before:
m n : Nat
x y : Permutation n
⊢ sign (x * y * inv x) = sign y
Tactic:
simp only [sign_mul]
Proof state after:
m n : Nat
x y : Permutation n
⊢ ((sign x != sign y) != sign (inv x)) = sign y
Theorem: Permutation.sign_conj
Proof state before:
m n : Nat
x y : Permutation n
⊢ ((sign x != sign y) != sign (inv x)) = sign y
Tactic:
rw [sign_inv, Bool.bne_comm x.sign, Bool.bne_assoc, Bool.bne_self, Bool.bne_false]
Proof state after:
no goals
Theorem: Permutation.sign_transposAdj
Proof state before:
m n i : Nat
h : i + 1 < n
⊢ sign (transposAdj i h) = true
Tactic:
dsimp [sign]
Proof state after:
m n i : Nat
h : i + 1 < n
⊢ (inversionNum (transposAdj i h) % 2 == 1) = true
Theorem: Permutation.sign_transposAdj
Proof state before:
m n i : Nat
h : i + 1 < n
⊢ (inversionNum (transposAdj i h) % 2 == 1) = true
Tactic:
rewrite [inversionNum_transposAdj]
Proof state after:
m n i : Nat
h : i + 1 < n
⊢ (1 % 2 == 1) = true
Theorem: Permutation.sign_transposAdj
Proof state before:
m n i : Nat
h : i + 1 < n
⊢ (1 % 2 == 1) = true
Tactic:
decide
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
m n : Nat
i j : Fin n
h : i ≠ j
⊢ sign (transpos i j) = true
Tactic:
suffices ∀ (i j : Fin n), i < j → (transpos i j).sign = true by
  rcases Nat.lt_trichotomy i.1 j.1 with hlt | heq | hgt
  . exact this i j hlt
  . exfalso; exact h <| Fin.eq_of_val_eq heq
  . rewrite [transpos_comm]; exact this j i hgt
Proof state after:
m n : Nat
i j : Fin n
h : i ≠ j
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true
Theorem: Permutation.sign_transpos
Proof state before:
m n : Nat
i j : Fin n
h : i ≠ j
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true
Tactic:
clear i j h
Proof state after:
m n : Nat
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true
Theorem: Permutation.sign_transpos
Proof state before:
m n : Nat
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true
Tactic:
intro i j h
Proof state after:
m n : Nat
i j : Fin n
h : i < j
⊢ sign (transpos i j) = true
Theorem: Permutation.sign_transpos
Proof state before:
m n : Nat
i j : Fin n
h : i < j
⊢ sign (transpos i j) = true
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case mk
m n : Nat
j : Fin n
i : Nat
hi : i < n
h : { val := i, isLt := hi } < j
⊢ sign (transpos { val := i, isLt := hi } j) = true
Theorem: Permutation.sign_transpos
Proof state before:
case mk
m n : Nat
j : Fin n
i : Nat
hi : i < n
h : { val := i, isLt := hi } < j
⊢ sign (transpos { val := i, isLt := hi } j) = true
Tactic:
rcases j with ⟨j,hj⟩
Proof state after:
case mk.mk
m n i : Nat
hi : i < n
j : Nat
hj : j < n
h : { val := i, isLt := hi } < { val := j, isLt := hj }
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk
m n i : Nat
hi : i < n
j : Nat
hj : j < n
h : { val := i, isLt := hi } < { val := j, isLt := hj }
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
Tactic:
simp at h
Proof state after:
case mk.mk
m n i : Nat
hi : i < n
j : Nat
hj : j < n
h : i < j
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk
m n i : Nat
hi : i < n
j : Nat
hj : j < n
h : i < j
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
Tactic:
induction h with
| refl => exact sign_transposAdj i hj
| @step j hij IH =>
  let s := transpos ⟨i,hi⟩ ⟨j, Nat.lt_of_succ_lt hj⟩
  have : transpos ⟨i,hi⟩ ⟨j+1,hj⟩ = transposAdj j hj * s * (transposAdj j hj).inv := by
    simp only [transpos_conj]
    rw [get_transposAdj_of_lt hij, get_transposAdj_self]
  rewrite [this]; simp only [sign_conj]
  exact IH _
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
⊢ sign (transpos i j) = true
Tactic:
rcases Nat.lt_trichotomy i.1 j.1 with hlt | heq | hgt
Proof state after:
case inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hlt : ↑i < ↑j
⊢ sign (transpos i j) = true

case inr.inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ sign (transpos i j) = true

case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true
Theorem: Permutation.sign_transpos
Proof state before:
case inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hlt : ↑i < ↑j
⊢ sign (transpos i j) = true

case inr.inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ sign (transpos i j) = true

case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true
Tactic:
. exact this i j hlt
Proof state after:
case inr.inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ sign (transpos i j) = true

case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true
Theorem: Permutation.sign_transpos
Proof state before:
case inr.inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ sign (transpos i j) = true

case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true
Tactic:
. exfalso; exact h <| Fin.eq_of_val_eq heq
Proof state after:
case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true
Theorem: Permutation.sign_transpos
Proof state before:
case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true
Tactic:
. rewrite [transpos_comm]; exact this j i hgt
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
case inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hlt : ↑i < ↑j
⊢ sign (transpos i j) = true
Tactic:
exact this i j hlt
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
case inr.inl
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ sign (transpos i j) = true
Tactic:
exfalso
Proof state after:
case inr.inl.h
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ False
Theorem: Permutation.sign_transpos
Proof state before:
case inr.inl.h
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
heq : ↑i = ↑j
⊢ False
Tactic:
exact h <| Fin.eq_of_val_eq heq
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos i j) = true
Tactic:
rewrite [transpos_comm]
Proof state after:
case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos j i) = true
Theorem: Permutation.sign_transpos
Proof state before:
case inr.inr
m n : Nat
i j : Fin n
h : i ≠ j
this : ∀ (i j : Fin n), i < j → sign (transpos i j) = true
hgt : ↑j < ↑i
⊢ sign (transpos j i) = true
Tactic:
exact this j i hgt
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk.refl
m n i : Nat
hi : i < n
j : Nat
hj : Nat.succ i < n
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ i, isLt := hj }) = true
Tactic:
exact sign_transposAdj i hj
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ j, isLt := hj }) = true
Tactic:
let s := transpos ⟨i,hi⟩ ⟨j, Nat.lt_of_succ_lt hj⟩
Proof state after:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ j, isLt := hj }) = true
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ j, isLt := hj }) = true
Tactic:
have : transpos ⟨i,hi⟩ ⟨j+1,hj⟩ = transposAdj j hj * s * (transposAdj j hj).inv := by
  simp only [transpos_conj]
  rw [get_transposAdj_of_lt hij, get_transposAdj_self]
Proof state after:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
this : transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ j, isLt := hj }) = true
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
this : transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
⊢ sign (transpos { val := i, isLt := hi } { val := Nat.succ j, isLt := hj }) = true
Tactic:
rewrite [this]
Proof state after:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
this : transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
⊢ sign (transposAdj j hj * s * inv (transposAdj j hj)) = true
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
this : transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
⊢ sign (transposAdj j hj * s * inv (transposAdj j hj)) = true
Tactic:
simp only [sign_conj]
Proof state after:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
this : transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }) = true
Theorem: Permutation.sign_transpos
Proof state before:
case mk.mk.step
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
this : transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
⊢ sign (transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }) = true
Tactic:
exact IH _
Proof state after:
no goals
Theorem: Permutation.sign_transpos
Proof state before:
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
⊢ transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transposAdj j hj * s * inv (transposAdj j hj)
Tactic:
simp only [transpos_conj]
Proof state after:
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
⊢ transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transpos (transposAdj j hj)[i] (transposAdj j hj)[j]
Theorem: Permutation.sign_transpos
Proof state before:
m n i : Nat
hi : i < n
j✝ j : Nat
hij : Nat.le (Nat.succ i) j
IH : ∀ (hj : j < n), sign (transpos { val := i, isLt := hi } { val := j, isLt := hj }) = true
hj : Nat.succ j < n
s : Permutation n := transpos { val := i, isLt := hi } { val := j, isLt := (_ : j < n) }
⊢ transpos { val := i, isLt := hi } { val := j + 1, isLt := hj } = transpos (transposAdj j hj)[i] (transposAdj j hj)[j]
Tactic:
rw [get_transposAdj_of_lt hij, get_transposAdj_self]
Proof state after:
no goals
Theorem: Permutation.sign_swap
Proof state before:
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ sign (swap x i j) = !sign x
Tactic:
rewrite [← mul_transpose_eq_swap, sign_mul, sign_transpos i j h]
Proof state after:
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ (sign x != true) = !sign x
Theorem: Permutation.sign_swap
Proof state before:
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ (sign x != true) = !sign x
Tactic:
exact Bool.bne_true _
Proof state after:
no goals
Theorem: Permutation.sign_cyclic_cons
Proof state before:
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (cyclic (i :: l)) = (List.length l % 2 == 1)
Tactic:
dsimp [cyclic]
Proof state after:
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
Theorem: Permutation.sign_cyclic_cons
Proof state before:
m n✝ n : Nat
i : Fin n
l : List (Fin n)
h : ¬i ∈ l
⊢ sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
Tactic:
induction l with
| nil => exact sign_one
| cons j l IH =>
  dsimp
  rewrite [List.mem_cons, not_or] at h
  rewrite [sign_swap _ i j h.1, IH h.2, Bool.eq_iff_iff]
  conv =>
    lhs; rewrite [Nat.not_beq_eq_true_eq]
  conv =>
    rhs; rewrite [beq_iff_eq, Nat.succ_eq_add_one, Nat.add_mod]
    change (l.length % 2 + 1) % 2 = 1
  cases l.length.mod_two_eq_zero_or_one
  all_goals (rename_i h; simp only [h])
Proof state after:
no goals
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case nil
m n✝ n : Nat
i : Fin n
h : ¬i ∈ []
⊢ sign (List.foldr (fun j x => swap x i j) 1 []) = (List.length [] % 2 == 1)
Tactic:
exact sign_one
Proof state after:
no goals
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i ∈ j :: l
⊢ sign (List.foldr (fun j x => swap x i j) 1 (j :: l)) = (List.length (j :: l) % 2 == 1)
Tactic:
dsimp
Proof state after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i ∈ j :: l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i ∈ j :: l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)
Tactic:
rewrite [List.mem_cons, not_or] at h
Proof state after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ sign (swap (List.foldr (fun j x => swap x i j) 1 l) i j) = (Nat.succ (List.length l) % 2 == 1)
Tactic:
rewrite [sign_swap _ i j h.1, IH h.2, Bool.eq_iff_iff]
Proof state after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ (!List.length l % 2 == 1) = true ↔ (Nat.succ (List.length l) % 2 == 1) = true