-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
inl :
  ∀ (hs : Set.Finite.{u_1} (α := α) ∅) (hle : encard.{u_1} (α := α) ∅ ≤ t.encard),
    ∃ (f : α → β), ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅
inr : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₁ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₂ : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₃ inr₄ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₅ : ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₆ :
  ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t) (hle' : (s \ {a}).encard ≤ (t \ {b}).encard),
    ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₇ :
  ∀ (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
inr₈ :
  ∀ (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
h :
  ∀ (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 (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧ InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) s
h₁ :
  ∀ (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 (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧
      InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a}) ∧
        Function.update (β := fun (a : α) ↦ β) f₀ a b a ∉ Function.update (β := fun (a : α) ↦ β) f₀ a b '' (s \ {a})
h₂ :
  ∀ (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 (β := fun (a : α) ↦ β) f₀ a b) (s \ {a}) ∧ ∀ x ∈ s, ¬x = a → ¬x = a ∧ ¬f₀ x = b
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have h₃ : ∀ (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
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  have hle' : (s \ {a}).encard ≤ (t \ {b}).encard := by
    rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top,
    encard_diff_singleton_add_one has, encard_diff_singleton_add_one hbt]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  simp only [mem_diff, mem_singleton_iff, insert_diff_singleton, subset_def,
    mem_insert_iff, mem_preimage, Function.update_apply, forall_eq_or_imp, ite_true, and_imp,
    mem_image, ite_eq_left_iff, not_exists, not_and, not_forall, exists_prop, and_iff_right hbt]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])