-- Mathlib/ModelTheory/Complexity.lean
lemma IsExistential.realize_embedding {φ : L.BoundedFormula α n} (hE : φ.IsExistential)
    (f : F) {v : α → M} {xs : Fin n → M} :
    φ.Realize v xs → φ.Realize (f ∘ v) (f ∘ xs)

Proof state:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
x✝ : ∃ a, φ✝.Realize v (snoc xs a)
a : M
ha : φ✝.Realize v (snoc xs a)
⊢ φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) (f a))

Tactic:
rw [← Fin.comp_snoc]

Result:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
x✝ : ∃ a, φ✝.Realize v (snoc xs a)
a : M
ha : φ✝.Realize v (snoc xs a)
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ snoc xs a)

Proof state:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
⊢ (∃ a, φ✝.Realize v (snoc xs a)) → ∃ a, φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)

Tactic:
refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩

Result:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
x✝ : ∃ a, φ✝.Realize v (snoc xs a)
a : M
ha : φ✝.Realize v (snoc xs a)
⊢ φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) (f a))

Proof state:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hE : φ.IsExistential
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
induction hE with
| of_isQF hQF => simp [hQF.realize_embedding]
| ex _ ih =>
  simp only [realize_ex, Nat.succ_eq_add_one]
  refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩
  rw [← Fin.comp_snoc]
  exact ih ha

Result:
no goals

Proof state:
case of_isQF
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hQF : φ✝.IsQF
xs : Fin n✝ → M
⊢ φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
simp [hQF.realize_embedding]

Result:
no goals

Proof state:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
⊢ (∃'φ✝).Realize v xs → (∃'φ✝).Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
simp only [realize_ex, Nat.succ_eq_add_one]

Result:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
⊢ (∃ a, φ✝.Realize v (snoc xs a)) → ∃ a, φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)

Proof state:
case ex
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsExistential
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)
xs : Fin n✝ → M
x✝ : ∃ a, φ✝.Realize v (snoc xs a)
a : M
ha : φ✝.Realize v (snoc xs a)
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ snoc xs a)

Tactic:
exact ih ha

Result:
no goals