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

State before:
n : Nat
i j : Fin n
h : i ≠ j
⊢ Nonempty (Inversion (transpos i j))
Tactic:
cases Nat.lt_or_ge i.1 j.1 with
| inl hlt => exact ⟨transposInversion i j hlt⟩
| inr hge =>
  rewrite [transpos_comm]
  refine ⟨transposInversion j i ?_⟩
  exact Nat.lt_of_le_of_ne hge fun hcntr =>
    h <| Fin.eq_of_val_eq hcntr.symm
State after:
no goals

State before:
case inl
n : Nat
i j : Fin n
h : i ≠ j
hlt : ↑i < ↑j
⊢ Nonempty (Inversion (transpos i j))
Tactic:
exact ⟨transposInversion i j hlt⟩
State after:
no goals

State before:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos i j))
Tactic:
rewrite [transpos_comm]
State after:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos j i))

State before:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ Nonempty (Inversion (transpos j i))
Tactic:
refine ⟨transposInversion j i ?_⟩
State after:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ ↑j < ↑i

State before:
case inr
n : Nat
i j : Fin n
h : i ≠ j
hge : ↑i ≥ ↑j
⊢ ↑j < ↑i
Tactic:
exact Nat.lt_of_le_of_ne hge fun hcntr =>
  h <| Fin.eq_of_val_eq hcntr.symm
State after:
no goals