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

Proof state:
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 β
val✝ : Fintype β
x : α → M
⊢ x ∈
      (fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.ofInjective ⇑f ⋯).sumCongr (Fintype.equivFin ↑(range ⇑f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range ⇑f))) '' s)) ↔
    x ∈ (fun g => g ∘ ⇑f) '' s

Tactic:
simp only [mem_preimage, mem_image, exists_exists_and_eq_and]

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 β
val✝ : Fintype β
x : α → M
⊢ (∃ a ∈ s,
      ((a ∘ ⇑(Equiv.Set.sumCompl (range ⇑f))) ∘
            ⇑((Equiv.ofInjective ⇑f ⋯).sumCongr (Fintype.equivFin ↑(range ⇑f)ᶜ).symm)) ∘
          Sum.inl =
        x) ↔
    ∃ 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 β
⊢ A.Definable L ((fun g => g ∘ ⇑f) '' 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_preimage, mem_image, exists_exists_and_eq_and]
  refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)
  simp

Result:
no goals

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

Proof state:
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 β
val✝ : Fintype β
x : α → M
y : β → M
x✝ : y ∈ s
a : α
⊢ (((y ∘ ⇑(Equiv.Set.sumCompl (range ⇑f))) ∘
          ⇑((Equiv.ofInjective ⇑f ⋯).sumCongr (Fintype.equivFin ↑(range ⇑f)ᶜ).symm)) ∘
        Sum.inl)
      a =
    (y ∘ ⇑f) a

Tactic:
simp

Result:
no goals

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

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

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 β
val✝ : Fintype β
x : α → M
⊢ x ∈
      (fun g => g ∘ Sum.inl) ''
        ((fun g => g ∘ ⇑((Equiv.ofInjective ⇑f ⋯).sumCongr (Fintype.equivFin ↑(range ⇑f)ᶜ).symm)) ''
          ((fun g => g ∘ ⇑(Equiv.Set.sumCompl (range ⇑f))) '' s)) ↔
    x ∈ (fun g => g ∘ ⇑f) '' s

Proof state:
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 β
val✝ : Fintype β
x : α → M
⊢ (∃ a ∈ s,
      ((a ∘ ⇑(Equiv.Set.sumCompl (range ⇑f))) ∘
            ⇑((Equiv.ofInjective ⇑f ⋯).sumCongr (Fintype.equivFin ↑(range ⇑f)ᶜ).symm)) ∘
          Sum.inl =
        x) ↔
    ∃ x_1 ∈ s, x_1 ∘ ⇑f = x

Tactic:
refine exists_congr fun y => and_congr_right fun _ => Eq.congr_left (funext fun a => ?_)

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 β
val✝ : Fintype β
x : α → M
y : β → M
x✝ : y ∈ s
a : α
⊢ (((y ∘ ⇑(Equiv.Set.sumCompl (range ⇑f))) ∘
          ⇑((Equiv.ofInjective ⇑f ⋯).sumCongr (Fintype.equivFin ↑(range ⇑f)ᶜ).symm)) ∘
        Sum.inl)
      a =
    (y ∘ ⇑f) a