-- Mathlib/Logic/Equiv/Set.lean
theorem Equiv.swap_bijOn_self (hs : a ∈ s ↔ b ∈ s) : BijOn (Equiv.swap a b) s s

Proof state:
case refine_2.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ x ∈ ⇑(swap a b) '' s

Tactic:
obtain (rfl | hxb) := eq_or_ne x b

Result:
case refine_2.inr.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
x : α
hx : x ∈ s
hxa : x ≠ a
hs : a ∈ s ↔ x ∈ s
⊢ x ∈ ⇑(swap a x) '' s

case refine_2.inr.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
hxb : x ≠ b
⊢ x ∈ ⇑(swap a b) '' s

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
⊢ x ∈ ⇑(swap a b) '' s

Tactic:
obtain (rfl | hxa) := eq_or_ne x a

Result:
case refine_2.inl
α : Type u_1
inst✝ : DecidableEq α
b : α
s : Set α
x : α
hx : x ∈ s
hs : x ∈ s ↔ b ∈ s
⊢ x ∈ ⇑(swap x b) '' s

case refine_2.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ x ∈ ⇑(swap a b) '' s

Proof state:
case refine_1.inl
α : Type u_1
inst✝ : DecidableEq α
b : α
s : Set α
x : α
hx : x ∈ s
hs : x ∈ s ↔ b ∈ s
⊢ (swap x b) x ∈ s

Tactic:
rwa [swap_apply_left, ← hs]

Result:
no goals

Proof state:
case refine_1.inr.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
x : α
hx : x ∈ s
hxa : x ≠ a
hs : a ∈ s ↔ x ∈ s
⊢ (swap a x) x ∈ s

Tactic:
rwa [swap_apply_right, hs]

Result:
no goals

Proof state:
case refine_2.inr.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
hxb : x ≠ b
⊢ x ∈ ⇑(swap a b) '' s

Tactic:
exact ⟨x, hx, swap_apply_of_ne_of_ne hxa hxb⟩

Result:
no goals

Proof state:
case refine_1.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ (swap a b) x ∈ s

Tactic:
obtain (rfl | hxb) := eq_or_ne x b

Result:
case refine_1.inr.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
x : α
hx : x ∈ s
hxa : x ≠ a
hs : a ∈ s ↔ x ∈ s
⊢ (swap a x) x ∈ s

case refine_1.inr.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
hxb : x ≠ b
⊢ (swap a b) x ∈ s

Proof state:
case refine_2.inl
α : Type u_1
inst✝ : DecidableEq α
b : α
s : Set α
x : α
hx : x ∈ s
hs : x ∈ s ↔ b ∈ s
⊢ x ∈ ⇑(swap x b) '' s

Tactic:
simp [hs.1 hx]

Result:
no goals

Proof state:
case refine_1.inr.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
hxb : x ≠ b
⊢ (swap a b) x ∈ s

Tactic:
rwa [swap_apply_of_ne_of_ne hxa hxb]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
⊢ BijOn (⇑(swap a b)) s s

Tactic:
refine ⟨fun x hx ↦ ?_, (Equiv.injective _).injOn, fun x hx ↦ ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ s

case refine_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
⊢ x ∈ ⇑(swap a b) '' s

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ s

Tactic:
obtain (rfl | hxa) := eq_or_ne x a

Result:
case refine_1.inl
α : Type u_1
inst✝ : DecidableEq α
b : α
s : Set α
x : α
hx : x ∈ s
hs : x ∈ s ↔ b ∈ s
⊢ (swap x b) x ∈ s

case refine_1.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
hs : a ∈ s ↔ b ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ (swap a b) x ∈ s

Proof state:
case refine_2.inr.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
x : α
hx : x ∈ s
hxa : x ≠ a
hs : a ∈ s ↔ x ∈ s
⊢ x ∈ ⇑(swap a x) '' s

Tactic:
simp [hs.2 hx]

Result:
no goals