-- Mathlib/Data/Set/Card.lean
theorem Finite.exists_injOn_of_encard_le [Nonempty β] {s : Set α} {t : Set β} (hs : s.Finite)
    (hle : s.encard ≤ t.encard) : ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ s ⊆ Function.update f₀ a b ⁻¹' t ∧ InjOn (Function.update f₀ a b) s

Tactic:
rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ insert a (s \ {a}) ⊆ Function.update f₀ a b ⁻¹' t ∧
    InjOn (Function.update f₀ a b) (s \ {a}) ∧ Function.update f₀ a b a ∉ Function.update f₀ a b '' (s \ {a})

Proof state:
case inr.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
use Function.update f₀ a b

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ s ⊆ Function.update f₀ a b ⁻¹' t ∧ InjOn (Function.update f₀ a b) s

Proof state:
case inr.inr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'

Result:
case inr.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})
hinj : InjOn f₀ (s \ {a})
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ (∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t) ∧
    InjOn (Function.update f₀ a b) (s \ {a}) ∧ ∀ x ∈ s, ¬x = a → ¬x = a ∧ ¬f₀ x = b

Tactic:
refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩

Result:
case h.refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ ∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t

case h.refine_2
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ InjOn (Function.update f₀ a b) (s \ {a})

Proof state:
case inr.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})
hinj : InjOn f₀ (s \ {a})
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s

Result:
case inr.inr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s