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

Proof state:
case of_isAtomic
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
xs : Fin n → M
φ✝ : L.BoundedFormula α n
hA : φ✝.IsAtomic
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ✝.Realize v xs

Tactic:
induction hA with
| equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
(EmbeddingLike.injective f).eq_iff]
| rel R ts =>
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Result:
no goals

Proof state:
case of_isAtomic.rel
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
xs : Fin n → M
φ✝ : L.BoundedFormula α n
l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (α ⊕ Fin n)
⊢ (R.boundedFormula ts).Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ (R.boundedFormula ts).Realize v xs

Tactic:
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]

Result:
case of_isAtomic.rel
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
xs : Fin n → M
φ✝ : L.BoundedFormula α n
l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (α ⊕ Fin n)
⊢ (RelMap R fun i => f (Term.realize (Sum.elim v xs) (ts i))) ↔ RelMap R fun i => Term.realize (Sum.elim v xs) (ts i)

Proof state:
case imp
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
xs : Fin n → M
φ₁✝ φ₂✝ : L.BoundedFormula α n
h₁✝ : φ₁✝.IsQF
h₂✝ : φ₂✝.IsQF
ihφ : φ₁✝.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ₁✝.Realize v xs
ihψ : φ₂✝.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ₂✝.Realize v xs
⊢ (φ₁✝ ⟹ φ₂✝).Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ (φ₁✝ ⟹ φ₂✝).Realize v xs

Tactic:
simp only [realize_imp, ihφ, ihψ]

Result:
no goals

Proof state:
case of_isAtomic.rel
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
xs : Fin n → M
φ✝ : L.BoundedFormula α n
l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (α ⊕ Fin n)
⊢ (RelMap R fun i => f (Term.realize (Sum.elim v xs) (ts i))) ↔ RelMap R fun i => Term.realize (Sum.elim v xs) (ts i)

Tactic:
exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Result:
no goals

Proof state:
case of_isAtomic.equal
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
xs : Fin n → M
φ✝ : L.BoundedFormula α n
t₁ t₂ : L.Term (α ⊕ Fin n)
⊢ (t₁ =' t₂).Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ (t₁ =' t₂).Realize v xs

Tactic:
simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
(EmbeddingLike.injective f).eq_iff]

Result:
no goals

Proof state:
case falsum
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
xs : Fin n → M
⊢ BoundedFormula.falsum.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ BoundedFormula.falsum.Realize v xs

Tactic:
rfl

Result:
no goals

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
hQF : φ.IsQF
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
induction hQF with
| falsum => rfl
| of_isAtomic hA => induction hA with
  | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
      (EmbeddingLike.injective f).eq_iff]
  | rel R ts =>
    simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
    exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
| imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]

Result:
no goals