-- Mathlib/ModelTheory/Definability.lean
theorem Definable.image_comp_sumInl_fin (m : ℕ) {s : Set (Sum α (Fin m) → M)}
    (h : A.Definable L s) : A.Definable L ((fun g : Sum α (Fin m) → M => g ∘ Sum.inl) '' s)

Proof state:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) ↔ ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)

Tactic:
constructor

Result:
case intro.h.mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) → ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)

case intro.h.mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)) → ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Proof state:
case intro.h.mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)) → ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Tactic:
rintro ⟨y, hy⟩

Result:
case intro.h.mpr.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
y : Fin (m + 0) → M
hy : BoundedFormula.Realize φ (Sum.elim x y) (y ∘ Fin.natAdd m)
⊢ ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Proof state:
case intro.h.mp.intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
y : α ⊕ Fin m → M
hy : φ.Realize y
⊢ ∃ xs, BoundedFormula.Realize φ (Sum.elim (y ∘ Sum.inl) xs) (xs ∘ Fin.natAdd m)

Tactic:
exact
  ⟨y ∘ Sum.inr, (congr (congr rfl (Sum.elim_comp_inl_inr y).symm) (funext finZeroElim)).mp hy⟩

Result:
no goals

Proof state:
case intro.h.mpr.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
y : Fin (m + 0) → M
hy : BoundedFormula.Realize φ (Sum.elim x y) (y ∘ Fin.natAdd m)
⊢ ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x

Tactic:
exact ⟨Sum.elim x y, (congr rfl (funext finZeroElim)).mp hy, Sum.elim_comp_inl _ _⟩

Result:
no goals

Proof state:
case intro.h.mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) → ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case intro.h.mp.intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
y : α ⊕ Fin m → M
hy : φ.Realize y
⊢ ∃ xs, BoundedFormula.Realize φ (Sum.elim (y ∘ Sum.inl) xs) (xs ∘ Fin.natAdd m)

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ (fun g => g ∘ Sum.inl) '' setOf φ.Realize = setOf (BoundedFormula.relabel id φ).exs.Realize

Tactic:
ext x

Result:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ x ∈ (fun g => g ∘ Sum.inl) '' setOf φ.Realize ↔ x ∈ setOf (BoundedFormula.relabel id φ).exs.Realize

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ A.Definable L ((fun g => g ∘ Sum.inl) '' setOf φ.Realize)

Tactic:
refine ⟨(BoundedFormula.relabel id φ).exs, ?_⟩

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ (fun g => g ∘ Sum.inl) '' setOf φ.Realize = setOf (BoundedFormula.relabel id φ).exs.Realize

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
s : Set (α ⊕ Fin m → M)
h : A.Definable L s
⊢ A.Definable L ((fun g => g ∘ Sum.inl) '' s)

Tactic:
obtain ⟨φ, rfl⟩ := h

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
⊢ A.Definable L ((fun g => g ∘ Sum.inl) '' setOf φ.Realize)

Proof state:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ x ∈ (fun g => g ∘ Sum.inl) '' setOf φ.Realize ↔ x ∈ setOf (BoundedFormula.relabel id φ).exs.Realize

Tactic:
simp only [Set.mem_image, mem_setOf_eq, BoundedFormula.realize_exs,
  BoundedFormula.realize_relabel, Function.comp_id, Fin.castAdd_zero, Fin.cast_refl]

Result:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) ↔ ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)