-- Lean 4 proof step from Mathlib.Data.Fintype.Sum (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
f : α → β
hfst : image f s ⊆ t
hfs : Set.InjOn f (↑s : Set α)
empty :
  ∀ {f : α → β} (hfst : image f ∅ ⊆ t) (hfs : Set.InjOn f (↑∅ : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t),
      ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → (↑((g : (a : α) → ↥t) i) : β) = f i
insert insert₁ :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (H :
      ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
        ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i)
    {f : α → β} (hfst : image f (Insert.insert a s) ⊆ t) (hfs : Set.InjOn f (↑(Insert.insert a s) : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
insert₂ :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (H :
      ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
        ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i)
    {f : α → β} (hfst : image f (Insert.insert a s) ⊆ t) (hfs : Set.InjOn f (↑(Insert.insert a s) : Set α))
    (hfst' : image f s ⊆ t),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
insert₃ :
  ∀ (a : α) (s : Finset α) (has : a ∉ s)
    (H :
      ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
        ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i)
    {f : α → β} (hfst : image f (Insert.insert a s) ⊆ t) (hfs : Set.InjOn f (↑(Insert.insert a s) : Set α))
    (hfst' : image f s ⊆ t) (hfs' : Set.InjOn f (↑s : Set α)),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i
have insert₄ : ∀ (a : α) (s : Finset α) (has : a ∉ s)
  (H :
    ∀ {f : α → β} (hfst : image f s ⊆ t) (hfs : Set.InjOn f (↑s : Set α)),
      ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ s, (↑((g : (a : α) → ↥t) i) : β) = f i)
  {f : α → β} (hfst : image f (Insert.insert a s) ⊆ t) (hfs : Set.InjOn f (↑(Insert.insert a s) : Set α))
  (hfst' : image f s ⊆ t) (hfs' : Set.InjOn f (↑s : Set α)) (g' : Equiv.{u_1 + 1, u_2 + 1} α ↥t)
  (hg' : ∀ i ∈ s, (↑((g' : (a : α) → ↥t) i) : β) = f i),
  ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
Tactic: classical
    induction s using Finset.induction generalizing f with
    | empty =>
      obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
      use e
      simp
    | insert a s has H => ?_
    have hfst' : Finset.image f s ⊆ t := (Finset.image_mono _ (s.subset_insert a)).trans hfst
    have hfs' : Set.InjOn f s := hfs.mono (s.subset_insert a)
    obtain ⟨g', hg'⟩ := H hfst' hfs'
    have hfat : f a ∈ t := hfst (mem_image_of_mem _ (s.mem_insert_self a))
    use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))
    simp_rw [mem_insert]
    rintro i (rfl | hi)
    · simp
    rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]
    · exact
        ne_of_apply_ne Subtype.val
          (ne_of_eq_of_ne (hg' _ hi) <|
            hfs.ne (subset_insert _ _ hi) (mem_insert_self _ _) <| ne_of_mem_of_not_mem hi has)
    · exact g'.injective.ne (ne_of_mem_of_not_mem hi has)
Cleared hypotheses: s, f, hfst, hfs