-- Mathlib/Logic/Equiv/Set.lean
theorem Equiv.swap_bijOn_exchange (ha : a ∈ s) (hb : b ∉ s) :
    BijOn (Equiv.swap a b) s (insert b (s \ {a}))

Proof state:
case refine_1.inl
α : Type u_1
inst✝ : DecidableEq α
b : α
s : Set α
hb : b ∉ s
x : α
hx ha : x ∈ s
⊢ (swap x b) x ∈ insert b (s \ {x})

Tactic:
simp [swap_apply_left]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ x ≠ b

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
ha : a ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
hb : x ∉ s
⊢ False

Proof state:
case refine_1.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ (swap a b) x ∈ insert b (s \ {a})

Tactic:
rw [swap_apply_of_ne_of_ne hxa (by rintro rfl; contradiction)]

Result:
case refine_1.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ x ∈ insert b (s \ {a})

Proof state:
case refine_2.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ insert b (s \ {a})
hxb : x ≠ b
⊢ x ∈ ⇑(swap a b) '' s

Tactic:
simp only [mem_insert_iff, mem_diff, mem_singleton_iff, or_iff_right hxb] at hx

Result:
case refine_2.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hxb : x ≠ b
hx : x ∈ s ∧ ¬x = a
⊢ x ∈ ⇑(swap a b) '' s

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ insert b (s \ {a})

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

Result:
case refine_1.inl
α : Type u_1
inst✝ : DecidableEq α
b : α
s : Set α
hb : b ∉ s
x : α
hx ha : x ∈ s
⊢ (swap x b) x ∈ insert b (s \ {x})

case refine_1.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ (swap a b) x ∈ insert b (s \ {a})

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
ha : a ∈ s
x : α
hx : x ∈ s
hxa : x ≠ a
hb : x ∉ s
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case refine_2.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
ha : a ∈ s
x : α
hb : x ∉ s
hx : x ∈ insert x (s \ {a})
⊢ x ∈ ⇑(swap a x) '' s

Tactic:
exact ⟨a, ha, by simp⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ insert b (s \ {a})
⊢ x ∈ ⇑(swap a b) '' s

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

Result:
case refine_2.inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
ha : a ∈ s
x : α
hb : x ∉ s
hx : x ∈ insert x (s \ {a})
⊢ x ∈ ⇑(swap a x) '' s

case refine_2.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ insert b (s \ {a})
hxb : x ≠ b
⊢ x ∈ ⇑(swap a b) '' s

Proof state:
case refine_2.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hxb : x ≠ b
hx : x ∈ s ∧ ¬x = a
⊢ x ∈ ⇑(swap a b) '' s

Tactic:
exact ⟨x, hx.1, swap_apply_of_ne_of_ne hx.2 hxb⟩

Result:
no goals

Proof state:
case refine_1.inr
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ s
hxa : x ≠ a
⊢ x ∈ insert b (s \ {a})

Tactic:
exact .inr ⟨hx, hxa⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
⊢ BijOn (⇑(swap a b)) s (insert b (s \ {a}))

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

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ insert b (s \ {a})

case refine_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Set α
ha : a ∈ s
hb : b ∉ s
x : α
hx : x ∈ insert b (s \ {a})
⊢ x ∈ ⇑(swap a b) '' s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Set α
ha : a ∈ s
x : α
hb : x ∉ s
hx : x ∈ insert x (s \ {a})
⊢ (swap a x) a = x

Tactic:
simp

Result:
no goals