-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
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
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
have 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 : α) → β) sorry).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
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