Theorem: Permutation.sign_transpos (Fifteen/Data/Permutation/Sign.lean)

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
State after:
m n : Nat
i j : Fin n
h : i ≠ j
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true

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
State after:
m n : Nat
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true

State before:
m n : Nat
⊢ ∀ (i j : Fin n), i < j → sign (transpos i j) = true
Tactic:
intro i j h
State after:
m n : Nat
i j : Fin n
h : i < j
⊢ sign (transpos i j) = true

State before:
m n : Nat
i j : Fin n
h : i < j
⊢ sign (transpos i j) = true
Tactic:
rcases i with ⟨i,hi⟩
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

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⟩
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

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
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

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 _
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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]
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

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
State after:
no goals

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
State after:
no goals

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⟩
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

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]
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

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]
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

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]
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

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 _
State after:
no goals

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]
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]

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]
State after:
no goals