Theorem: Permutation.Inversion.elim1 (Fifteen/Data/Permutation/Inversion.lean)

State before:
n : Nat
α : Sort u
iv : Inversion 1
⊢ α
Tactic:
rcases iv with ⟨i,j,hlt,hinv⟩
State after:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : 1[↑i] > 1[↑j]
⊢ α

State before:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : 1[↑i] > 1[↑j]
⊢ α
Tactic:
conv at hinv => simp only [get_one]
State after:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ α

State before:
case mk
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ α
Tactic:
exfalso
State after:
case mk.h
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ False

State before:
case mk.h
n : Nat
α : Sort u
i j : Fin n
hlt : i < j
hinv : { val := ↑i, isLt := (_ : ↑i < n) } > { val := ↑j, isLt := (_ : ↑j < n) }
⊢ False
Tactic:
exact Nat.lt_asymm hlt hinv
State after:
no goals