-- Mathlib/ModelTheory/Semantics.lean
theorem realize_restrictFreeVar [DecidableEq α] {n : ℕ} {φ : L.BoundedFormula α n}
    {f : φ.freeVarFinset → β} {v : β → M} {xs : Fin n → M}
    (v' : α → M) (hv' : ∀ a, v (f a) = v' a) :
    (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs

Proof state:
case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
f : { x // x ∈ (equal t₁✝ t₂✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (equal t₁✝ t₂✝).freeVarFinset }), v (f a) = v' ↑a
⊢ ((equal t₁✝ t₂✝).restrictFreeVar f).Realize v xs ↔ (equal t₁✝ t₂✝).Realize v' xs

Tactic:
simp only [Realize, restrictFreeVar, freeVarFinset.eq_2]

Result:
case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
f : { x // x ∈ (equal t₁✝ t₂✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (equal t₁✝ t₂✝).freeVarFinset }), v (f a) = v' ↑a
⊢ realize (Sum.elim v xs) (t₁✝.restrictVarLeft (f ∘ Set.inclusion ⋯)) =
      realize (Sum.elim v xs) (t₂✝.restrictVarLeft (f ∘ Set.inclusion ⋯)) ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝

Proof state:
case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : { x // x ∈ (rel R✝ ts✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (rel R✝ ts✝).freeVarFinset }), v (f a) = v' ↑a
⊢ ((rel R✝ ts✝).restrictFreeVar f).Realize v xs ↔ (rel R✝ ts✝).Realize v' xs

Tactic:
simp only [Realize, freeVarFinset.eq_3, Finset.biUnion_val, restrictFreeVar]

Result:
case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : { x // x ∈ (rel R✝ ts✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (rel R✝ ts✝).freeVarFinset }), v (f a) = v' ↑a
⊢ (RelMap R✝ fun i => realize (Sum.elim v xs) ((ts✝ i).restrictVarLeft (f ∘ Set.inclusion ⋯))) ↔
    RelMap R✝ fun i => realize (Sum.elim v' xs) (ts✝ i)

Proof state:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : { x // x ∈ f₁✝.freeVarFinset } → β} {xs : Fin n✝ → M},
    (∀ (a : { x // x ∈ f₁✝.freeVarFinset }), v (f a) = v' ↑a) →
      ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : { x // x ∈ f₂✝.freeVarFinset } → β} {xs : Fin n✝ → M},
    (∀ (a : { x // x ∈ f₂✝.freeVarFinset }), v (f a) = v' ↑a) →
      ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : { x // x ∈ (f₁✝ ⟹ f₂✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (f₁✝ ⟹ f₂✝).freeVarFinset }), v (f a) = v' ↑a
⊢ ((f₁✝ ⟹ f₂✝).restrictFreeVar f).Realize v xs ↔ (f₁✝ ⟹ f₂✝).Realize v' xs

Tactic:
simp only [Realize, restrictFreeVar, freeVarFinset.eq_4]

Result:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : { x // x ∈ f₁✝.freeVarFinset } → β} {xs : Fin n✝ → M},
    (∀ (a : { x // x ∈ f₁✝.freeVarFinset }), v (f a) = v' ↑a) →
      ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : { x // x ∈ f₂✝.freeVarFinset } → β} {xs : Fin n✝ → M},
    (∀ (a : { x // x ∈ f₂✝.freeVarFinset }), v (f a) = v' ↑a) →
      ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : { x // x ∈ (f₁✝ ⟹ f₂✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (f₁✝ ⟹ f₂✝).freeVarFinset }), v (f a) = v' ↑a
⊢ (f₁✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs → (f₂✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs ↔
    f₁✝.Realize v' xs → f₂✝.Realize v' xs

Proof state:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : { x // x ∈ f₁✝.freeVarFinset } → β} {xs : Fin n✝ → M},
    (∀ (a : { x // x ∈ f₁✝.freeVarFinset }), v (f a) = v' ↑a) →
      ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : { x // x ∈ f₂✝.freeVarFinset } → β} {xs : Fin n✝ → M},
    (∀ (a : { x // x ∈ f₂✝.freeVarFinset }), v (f a) = v' ↑a) →
      ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : { x // x ∈ (f₁✝ ⟹ f₂✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (f₁✝ ⟹ f₂✝).freeVarFinset }), v (f a) = v' ↑a
⊢ (f₁✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs → (f₂✝.restrictFreeVar (f ∘ Set.inclusion ⋯)).Realize v xs ↔
    f₁✝.Realize v' xs → f₂✝.Realize v' xs

Tactic:
rw [ih1, ih2] <;> simp [hv']

Result:
no goals

Proof state:
case rel.a.h.e'_6.h
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : { x // x ∈ (rel R✝ ts✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (rel R✝ ts✝).freeVarFinset }), v (f a) = v' ↑a
x✝ : Fin l✝
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) (ts✝ x✝) = realize (Sum.elim v' xs) (ts✝ x✝)

Tactic:
simp [Function.comp_apply]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : { x // x ∈ (rel R✝ ts✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (rel R✝ ts✝).freeVarFinset }), v (f a) = v' ↑a
x✝ : Fin l✝
⊢ ∀ (a : { x // x ∈ (ts✝ x✝).varFinsetLeft }), Sum.elim v xs (Sum.inl ((f ∘ Set.inclusion ⋯) a)) = v' ↑a

Tactic:
simp [hv']

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : { x // x ∈ φ.freeVarFinset } → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : { x // x ∈ φ.freeVarFinset }), v (f a) = v' ↑a
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs

Tactic:
induction φ with
| falsum => rfl
| equal =>
  simp only [Realize, restrictFreeVar, freeVarFinset.eq_2]
  rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]
  simp [Function.comp_apply]
| rel =>
  simp only [Realize, freeVarFinset.eq_3, Finset.biUnion_val, restrictFreeVar]
  congr!
  rw [realize_restrictVarLeft v' (by simp [hv'])]
  simp [Function.comp_apply]
| imp _ _ ih1 ih2 =>
  simp only [Realize, restrictFreeVar, freeVarFinset.eq_4]
  rw [ih1, ih2] <;> simp [hv']
| all _ ih3 =>
  simp only [restrictFreeVar, Realize]
  refine forall_congr' (fun _ => ?_)
  rw [ih3]; simp [hv']

Result:
no goals