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

State before:
n i : Nat
h : i + 1 < n
iv : Inversion (transposAdj i h)
⊢ iv = transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
cases iv.fst_eq_or_snd_eq_of_transpos i.lt_succ_self
<;> cases iv <;> rename_i k l hlt hinv heq <;> cases heq
<;> simp only [transposAdj, get_transpos, if_pos] at hinv
State after:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  (if i + 1 = i then { val := i, isLt := (_ : i < n) } else { val := i + 1, isLt := h }) >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑l then { val := i + 1, isLt := h }
      else
        { val := ↑l,
          isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  (if i + 1 = i then { val := i, isLt := (_ : i < n) } else { val := i + 1, isLt := h }) >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑l then { val := i + 1, isLt := h }
      else
        { val := ↑l,
          isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
. simp only [i.succ_ne_self, Nat.ne_of_lt (a:=i) (b:=l.1) hlt, if_neg] at hinv
  if hil : i+1 = l.1 then
    have : ⟨i+1,h⟩ = l := Fin.eq_of_val_eq hil
    cases this; rfl
  else
    exfalso
    conv at hinv => simp only [hil, if_neg]; change i+1 > l.1
    exact Nat.not_le_of_lt hinv hlt
State after:
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
. simp only [Ne.symm <| Nat.ne_of_lt (a:=k.1) (b:=i+1) hlt, if_neg] at hinv
  if hik : i = k.1 then
    have : ⟨i, Nat.lt_of_succ_lt h⟩ = k := Fin.eq_of_val_eq hik
    cases this; rfl
  else
    exfalso
    conv at hinv => simp only [hik, if_neg]; change k.1 > i
    exact Nat.not_le_of_lt hlt hinv
State after:
no goals

State before:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  (if i + 1 = i then { val := i, isLt := (_ : i < n) } else { val := i + 1, isLt := h }) >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑l then { val := i + 1, isLt := h }
      else
        { val := ↑l,
          isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
simp only [i.succ_ne_self, Nat.ne_of_lt (a:=i) (b:=l.1) hlt, if_neg] at hinv
State after:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
case inl.mk.refl
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
if hil : i+1 = l.1 then
  have : ⟨i+1,h⟩ = l := Fin.eq_of_val_eq hil
  cases this; rfl
else
  exfalso
  conv at hinv => simp only [hil, if_neg]; change i+1 > l.1
  exact Nat.not_le_of_lt hinv hlt
State after:
no goals

State before:
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : i + 1 = ↑l
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
have : ⟨i+1,h⟩ = l := Fin.eq_of_val_eq hil
State after:
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : i + 1 = ↑l
this : { val := i + 1, isLt := h } = l
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : i + 1 = ↑l
this : { val := i + 1, isLt := h } = l
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
cases this
State after:
case refl
n i : Nat
h : i + 1 < n
hlt : { val := i, isLt := (_ : i < n) } < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑{ val := i + 1, isLt := h } then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑{ val := i + 1, isLt := h },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i + 1, isLt := h }) }
hil : i + 1 = ↑{ val := i + 1, isLt := h }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
case refl
n i : Nat
h : i + 1 < n
hlt : { val := i, isLt := (_ : i < n) } < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑{ val := i + 1, isLt := h } then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑{ val := i + 1, isLt := h },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i + 1, isLt := h }) }
hil : i + 1 = ↑{ val := i + 1, isLt := h }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
rfl
State after:
no goals

State before:
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : ¬i + 1 = ↑l
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := l, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
exfalso
State after:
case h
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : ¬i + 1 = ↑l
⊢ False

State before:
case h
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv :
  { val := i + 1, isLt := h } >
    if i + 1 = ↑l then { val := i, isLt := (_ : i < n) }
    else
      { val := ↑l,
        isLt := (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑l) }
hil : ¬i + 1 = ↑l
⊢ False
Tactic:
conv at hinv => simp only [hil, if_neg]; change i+1 > l.1
State after:
case h
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv : i + 1 > ↑l
hil : ¬i + 1 = ↑l
⊢ False

State before:
case h
n i : Nat
h : i + 1 < n
l : Fin n
hlt : { val := i, isLt := (_ : i < n) } < l
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑l]
hinv : i + 1 > ↑l
hil : ¬i + 1 = ↑l
⊢ False
Tactic:
exact Nat.not_le_of_lt hinv hlt
State after:
no goals

State before:
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i + 1 = ↑k then { val := i, isLt := (_ : i < n) }
    else
      if i = ↑k then { val := i + 1, isLt := h }
      else
        { val := ↑k,
          isLt :=
            (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
simp only [Ne.symm <| Nat.ne_of_lt (a:=k.1) (b:=i+1) hlt, if_neg] at hinv
State after:
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
case inr.mk.refl
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
if hik : i = k.1 then
  have : ⟨i, Nat.lt_of_succ_lt h⟩ = k := Fin.eq_of_val_eq hik
  cases this; rfl
else
  exfalso
  conv at hinv => simp only [hik, if_neg]; change k.1 > i
  exact Nat.not_le_of_lt hlt hinv
State after:
no goals

State before:
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑k
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
have : ⟨i, Nat.lt_of_succ_lt h⟩ = k := Fin.eq_of_val_eq hik
State after:
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑k
this : { val := i, isLt := (_ : i < n) } = k
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑k
this : { val := i, isLt := (_ : i < n) } = k
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
cases this
State after:
case refl
n i : Nat
h : i + 1 < n
hlt : { val := i, isLt := (_ : i < n) } < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑{ val := i, isLt := (_ : i < n) } then { val := i + 1, isLt := h }
    else
      { val := ↑{ val := i, isLt := (_ : i < n) },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i, isLt := (_ : i < n) }) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑{ val := i, isLt := (_ : i < n) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)

State before:
case refl
n i : Nat
h : i + 1 < n
hlt : { val := i, isLt := (_ : i < n) } < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑{ val := i, isLt := (_ : i < n) }] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑{ val := i, isLt := (_ : i < n) } then { val := i + 1, isLt := h }
    else
      { val := ↑{ val := i, isLt := (_ : i < n) },
        isLt :=
          (_ :
            (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h })
              ↑{ val := i, isLt := (_ : i < n) }) }) >
    { val := i, isLt := (_ : i < n) }
hik : i = ↑{ val := i, isLt := (_ : i < n) }
⊢ { fst := { val := i, isLt := (_ : i < n) }, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
rfl
State after:
no goals

State before:
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
hik : ¬i = ↑k
⊢ { fst := k, snd := { val := i + 1, isLt := h }, lt := hlt, inverted := hinv✝ } =
    transposInversion { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h } (_ : i < Nat.succ i)
Tactic:
exfalso
State after:
case h
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
hik : ¬i = ↑k
⊢ False

State before:
case h
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv :
  (if i = ↑k then { val := i + 1, isLt := h }
    else
      { val := ↑k,
        isLt :=
          (_ : (fun x i => i < n) (transpos { val := i, isLt := (_ : i < n) } { val := i + 1, isLt := h }) ↑k) }) >
    { val := i, isLt := (_ : i < n) }
hik : ¬i = ↑k
⊢ False
Tactic:
conv at hinv => simp only [hik, if_neg]; change k.1 > i
State after:
case h
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv : ↑k > i
hik : ¬i = ↑k
⊢ False

State before:
case h
n i : Nat
h : i + 1 < n
k : Fin n
hlt : k < { val := i + 1, isLt := h }
hinv✝ : (transposAdj i h)[↑k] > (transposAdj i h)[↑{ val := i + 1, isLt := h }]
hinv : ↑k > i
hik : ¬i = ↑k
⊢ False
Tactic:
exact Nat.not_le_of_lt hlt hinv
State after:
no goals