-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ↪ β
inst_1 : Finite β
intro : ∀ (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
intro₁ :
  ∀ (val : Fintype β) (x : α → M),
    Membership.mem (γ := Set (α → M))
        ((fun (g : α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)) → M) ↦
            g ∘ Sum.inl) ''
          (fun
                (g :
                  (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
                      (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1) →
                    M) ↦
              g ∘
                (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                      (Equiv.symm
                        (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
                  (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                    (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) ''
            (fun (g : β → M) ↦
                g ∘
                  (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                    (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β)) ''
              s)
        x ↔
      Membership.mem (γ := Set (α → M)) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s) x
intro₂ :
  ∀ (val : Fintype β) (x : α → M),
    (∃ a ∈ s,
        Function.comp (β :=
            α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))
            (Function.comp (β :=
              (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
                (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1))
              (a ∘
                (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                  (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β))
              (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                    (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
                (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                  (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)))
            Sum.inl =
          x) ↔
      ∃ x_1 ∈ s, x_1 ∘ (⇑f : (a : α) → β) = x
intro₃ :
  ∀ (val : Fintype β) (x : α → M),
    ∀ y ∈ s,
      ∀ (a : α),
        Function.comp (β :=
            α ⊕ Fin (Fintype.card.{u_1} (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))
            (Function.comp (β :=
              (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β)) : Type u_1) ⊕
                (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1))
              (y ∘
                (⇑(Equiv.Set.sumCompl (range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))) :
                  (a : (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)) → β))
              (⇑((Equiv.ofInjective (⇑f : (a : α) → β) ⋯).sumCongr
                    (Equiv.symm (Fintype.equivFin (↑(range.{u_1, u₁ + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_1)))) :
                (a : α ⊕ Fin (Fintype.card (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1))) →
                  (↑(range (⇑f : (a : α) → β)) : Type u_1) ⊕ (↑(range (⇑f : (a : α) → β))ᶜ : Type u_1)))
            Sum.inl a =
          (y ∘ (⇑f : (a : α) → β)) a
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)

Tactic:
classical
    cases nonempty_fintype β
    refine
      (congr rfl (ext fun x => ?_)).mp
        (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
              (Equiv.sumCongr (Equiv.ofInjective f f.injective)
                (Fintype.equivFin (↥(range f)ᶜ)).symm)).image_comp_sumInl_fin
          _)
    simp only [mem_image, exists_exists_and_eq_and]
    refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)
    simp

Premises used: Set.mem_image, Eq.congr_left, and_congr_right, funext, exists_congr, nonempty_fintype, exists_exists_and_eq_and