Theorem: Equiv.Perm.exists_pair_of_isSwap (Bruhat/Perm.lean)

State before:
α : Type u_1
x y : α
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
hf : IsSwap f
⊢ ∃ p, f = swap p.lo p.hi
Tactic:
obtain ⟨x,y, hxy, rfl⟩ := hf
State after:
case intro.intro.intro
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ p, swap x y = swap p.lo p.hi

State before:
case intro.intro.intro
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ p, swap x y = swap p.lo p.hi
Tactic:
obtain (h | h) := hxy.lt_or_lt
State after:
case intro.intro.intro.inl
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : x < y
⊢ ∃ p, swap x y = swap p.lo p.hi

case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap x y = swap p.lo p.hi

State before:
case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap x y = swap p.lo p.hi
Tactic:
rw [Equiv.swap_comm]
State after:
case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap y x = swap p.lo p.hi

State before:
case intro.intro.intro.inr
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ p, swap y x = swap p.lo p.hi
Tactic:
exact ⟨Pair.mk y x h, rfl⟩
State after:
no goals

State before:
case intro.intro.intro.inl
α : Type u_1
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h : x < y
⊢ ∃ p, swap x y = swap p.lo p.hi
Tactic:
exact ⟨Pair.mk x y h, rfl⟩
State after:
no goals