-- Mathlib/Data/Set/Function.lean
theorem BijOn.insert_iff (ha : a ∉ s) (hfa : f a ∉ t) :
    BijOn f (insert a s) (insert (f a) t) ↔ BijOn f s t where
  mp h

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Tactic:
refine (bijOn_singleton.mpr rfl).union h ?_

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ InjOn f ({a} ∪ s)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ MapsTo f s t

Tactic:
simp [← this, mapsTo']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ SurjOn f s t

Tactic:
simp [← this, surjOn_image]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬f x = f a

Tactic:
rw [h.injOn.eq_iff (by simp [hx]) (by simp)]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬x = a

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ a ∈ insert a s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t \ {f a}
⊢ BijOn f s t

Tactic:
rw [diff_singleton_eq_self hfa, diff_singleton_eq_self] at this

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ BijOn f s t

α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
⊢ f a ∉ f '' s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) (insert (f a) t)

Tactic:
rw [insert_eq]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : (fun x => x \ {f a}) (insert (f a) (f '' s)) = (fun x => x \ {f a}) (insert (f a) t)
⊢ BijOn f s t

Tactic:
simp only [mem_singleton_iff, insert_diff_of_mem] at this

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t \ {f a}
⊢ BijOn f s t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ BijOn f (insert a s) (insert (f a) t)

Tactic:
repeat rw [insert_eq]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ ∀ x ∈ s, ¬f x = f a

Tactic:
exact fun _ hx h₂ ↦ hfa (h₂ ▸ h.mapsTo hx)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ InjOn f ({a} ∪ s)

Tactic:
simp only [singleton_union, injOn_insert fun x ↦ (hfa (h.mapsTo x)), h.injOn, mem_image,
  not_exists, not_and, true_and]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f s t
⊢ ∀ x ∈ s, ¬f x = f a

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ BijOn f s t

Tactic:
exact ⟨by simp [← this, mapsTo'], h.injOn.mono (subset_insert ..),
  by simp [← this, surjOn_image]⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
⊢ ∀ x ∈ s, ¬f x = f a

Tactic:
intro x hx

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬f x = f a

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
⊢ f a ∉ f '' s

Tactic:
simp only [mem_image, not_exists, not_and]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : a ∉ s
hfa : f a ∉ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
⊢ ∀ x ∈ s, ¬f x = f a