-- Module: Mathlib.Data.Fintype.Sum
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
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
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) (hfat : f a ∈ t),
    ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ Insert.insert a s, (↑((g : (a : α) → ↥t) i) : β) = f i
h :
  ∀ (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) (hfat : f a ∈ t),
    ∀ i ∈ Insert.insert a s,
      (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) :
                (a : α) → ↥t)
              i) :
          β) =
        f i
h₁ :
  ∀ (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) (hfat : f a ∈ t) (i : α),
    i = a ∨ i ∈ s →
      (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) :
                (a : α) → ↥t)
              i) :
          β) =
        f i
h₂ :
  ∀ (s : Finset α)
    (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 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) (i : α) (has : i ∉ s) (hfst : image f (Insert.insert i s) ⊆ t)
    (hfs : Set.InjOn f (↑(Insert.insert i s) : Set α)) (hfat : f i ∈ t),
    (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f i) hfat) ((g' : (a : α) → ↥t) i)) : (a : α) → ↥t)
            i) :
        β) =
      f i
h₃ h₄ :
  ∀ (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) (hfat : f a ∈ t) (i : α) (hi : i ∈ s),
    (↑((g'.trans (Equiv.swap (Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat) ((g' : (a : α) → ↥t) a)) : (a : α) → ↥t)
            i) :
        β) =
      f i
h₅ :
  ∀ (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) (hfat : f a ∈ t) (i : α) (hi : i ∈ s),
    (g' : (a : α) → ↥t) i ≠ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hfat
h₆ h₇ :
  ∀ (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) (hfat : f a ∈ t) (i : α) (hi : i ∈ s),
    Ne.{u_2 + 1} (α := ↥t) ((g' : (a : α) → ↥t) i : ↥t) ((g' : (a : α) → ↥t) a : ↥t)
⊢ ∃ (g : Equiv.{u_1 + 1, u_2 + 1} α ↥t), ∀ i ∈ 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)

Premises used: Equiv.trans_apply, Membership.mem, Equiv, Subtype, Insert.insert, Finset.mem_insert, Equiv.swap_apply_of_ne_of_ne, Nonempty, rfl