-- Mathlib/ModelTheory/Definability.lean
theorem Definable.image_comp {s : Set (β → M)} (h : A.Definable L s) (f : α → β) [Finite α]
    [Finite β] : A.Definable L ((fun g : β → M => g ∘ f) '' s)

Proof state:
case intro.intro
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ A.Definable L ((fun g => g ∘ f) '' s)

Tactic:
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_finset_biInter h' Finset.univ)
  simp

Result:
case intro.intro
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ A.Definable L ((fun g => g ∘ f) '' s)

Proof state:
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
refine (congr rfl (ext ?_)).mp (definable_finset_biInter h' Finset.univ)

Result:
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ ∀ (x : α → M),
    x ∈ ⋂ i ∈ Finset.univ, {x | x i = x (rangeSplitting f (rangeFactorization f i))} ↔
      x ∈ {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Proof state:
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ ∀ (a : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
refine fun a => ⟨(var a).equal (var (rangeSplitting f (rangeFactorization f a))), ext ?_⟩

Result:
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
a : α
⊢ ∀ (x : α → M),
    x ∈ {x | x a = x (rangeSplitting f (rangeFactorization f a))} ↔
      x ∈ setOf ((var a).equal (var (rangeSplitting f (rangeFactorization f a)))).Realize

Proof state:
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
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

Result:
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
h' : ∀ (a : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Proof state:
case intro.intro
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
⊢ A.Definable L ((fun g => g ∘ f) '' s)

Tactic:
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)

Result:
case intro.intro
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✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g => g ∘ rangeSplitting f) ⁻¹'
      ((fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s))))
⊢ A.Definable L ((fun g => g ∘ f) '' s)