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

Proof state:
case all
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✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)
a : M
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ snoc xs a)

Tactic:
rw [Fin.comp_snoc]

Result:
case all
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✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)
a : M
⊢ φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) (f a))

Proof state:
case all
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✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)
a : M
⊢ φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) (f a))

Tactic:
exact h (f a)

Result:
no goals

Proof state:
case all
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✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀'φ✝).Realize (⇑f ∘ v) (⇑f ∘ xs) → (∀'φ✝).Realize v xs

Tactic:
simp only [realize_all, Nat.succ_eq_add_one]

Result:
case all
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✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)) → ∀ (a : M), φ✝.Realize v (snoc xs 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
hU : φ.IsUniversal
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ.Realize v xs

Tactic:
induction hU with
| of_isQF hQF => simp [hQF.realize_embedding]
| all _ ih =>
  simp only [realize_all, Nat.succ_eq_add_one]
  refine fun h a => ih ?_
  rw [Fin.comp_snoc]
  exact h (f a)

Result:
no goals

Proof state:
case all
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✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)) → ∀ (a : M), φ✝.Realize v (snoc xs a)

Tactic:
refine fun h a => ih ?_

Result:
case all
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✝ : φ✝.IsUniversal
ih : ∀ {xs : Fin (n✝ + 1) → M}, φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (a : N), φ✝.Realize (⇑f ∘ v) (snoc (⇑f ∘ xs) a)
a : M
⊢ φ✝.Realize (⇑f ∘ v) (⇑f ∘ snoc xs a)

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 (⇑f ∘ v) (⇑f ∘ xs) → φ✝.Realize v xs

Tactic:
simp [hQF.realize_embedding]

Result:
no goals