-- 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 α
inst_2 : Finite β
intro : ∀ (val : Fintype α), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
intro₁ : ∀ (val : Fintype α) (val : Fintype β), Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
intro₂ :
  ∀ (val : Fintype α) (val_1 : Fintype β)
    (h :
      Definable.{u, v, w, u₁} A L (α := α)
        (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
          ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
            (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
                g ∘
                  (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                        (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                    (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                      (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
              (fun (g : β → M) ↦
                  g ∘
                    (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
                s))),
    Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
have intro₃ : ∀ (val : Fintype α) (val_1 : Fintype β)
  (h :
    Definable.{u, v, w, u₁} A L (α := α)
      (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
        ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
          (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
              g ∘
                (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                      (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                  (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                    (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
            (fun (g : β → M) ↦
                g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
              s)))
  (h' :
    Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}),
  Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ f) '' s)
Tactic: classical
    cases nonempty_fintype α
    cases nonempty_fintype β
    have h :=
      (((h.image_comp_equiv (Equiv.Set.sumCompl (range f))).image_comp_equiv
                (Equiv.sumCongr (_root_.Equiv.refl _)
                  (Fintype.equivFin _).symm)).image_comp_sumInl_fin
            _).preimage_comp
        (rangeSplitting f)
    have h' :
      A.Definable L { x : α → M | ∀ a, x a = x (rangeSplitting f (rangeFactorization f a)) } := by
      have h' : ∀ a,
        A.Definable L { x : α → M | x a = x (rangeSplitting f (rangeFactorization f a)) } := by
          refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩
          simp
      refine (congr rfl (ext ?_)).mp (definable_biInter_finset h' Finset.univ)
      simp
    refine (congr rfl (ext fun x => ?_)).mp (h.inter h')
    simp only [mem_inter_iff, mem_preimage, mem_image, exists_exists_and_eq_and,
      mem_setOf_eq]
    constructor
    · rintro ⟨⟨y, ys, hy⟩, hx⟩
      refine ⟨y, ys, ?_⟩
      ext a
      rw [hx a, ← Function.comp_apply (f := x), ← hy]
      simp
    · rintro ⟨y, ys, rfl⟩
      refine ⟨⟨y, ys, ?_⟩, fun a => ?_⟩
      · ext
        simp [Set.apply_rangeSplitting f]
      · rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]