-- 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.mp.intro.intro.intro.h
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))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a = x a

Tactic:
rw [hx a, ← Function.comp_apply (f := x), ← hy]

Result:
case intro.intro.mp.intro.intro.intro.h
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))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a =
    (((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
        Sum.inl)
      (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 β
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)

Tactic:
refine (congr rfl (ext fun x => ?_)).mp (h.inter h')

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))}
x : α → M
⊢ x ∈
      (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))) ∩
        {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))} ↔
    x ∈ (fun g => g ∘ f) '' s

Proof state:
case intro.intro.mpr.intro.intro.refine_2
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))}
y : β → M
ys : y ∈ s
a : α
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
  rangeFactorization_coe]

Result:
no goals

Proof state:
case intro.intro.mp
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))}
x : α → M
⊢ ((∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1 ∈ s, x_1 ∘ f = x

Tactic:
rintro ⟨⟨y, ys, hy⟩, hx⟩

Result:
case intro.intro.mp.intro.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))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
⊢ ∃ x_1 ∈ s, x_1 ∘ f = x

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 β
⊢ A.Definable L ((fun g => g ∘ f) '' s)

Tactic:
cases nonempty_fintype α

Result:
case 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 α
⊢ 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))}
⊢ ∀ (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))}

Tactic:
simp

Result:
no goals