-- 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
⊢ 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₂✝

Tactic:
rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])]

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' (Sum.elim v xs ∘ Sum.inr)) t₁✝ = realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₂✝ ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : { x // x ∈ f✝.freeVarFinset } → β} {xs : Fin (n✝ + 1) → 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✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (∀'f✝).freeVarFinset }), v (f a) = v' ↑a
x✝ : M
⊢ ∀ (a : { x // x ∈ f✝.freeVarFinset }), v (f 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 : ℕ
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
⊢ ∀ (a : { x // x ∈ t₁✝.varFinsetLeft }), Sum.elim v xs (Sum.inl ((f ∘ Set.inclusion ⋯) a)) = v' ↑a

Tactic:
simp [hv']

Result:
no goals

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : { x // x ∈ f✝.freeVarFinset } → β} {xs : Fin (n✝ + 1) → 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✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (∀'f✝).freeVarFinset }), v (f a) = v' ↑a
x✝ : M
⊢ (f✝.restrictFreeVar f).Realize v (snoc xs x✝) ↔ f✝.Realize v' (snoc xs x✝)

Tactic:
rw [ih3]

Result:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : { x // x ∈ f✝.freeVarFinset } → β} {xs : Fin (n✝ + 1) → 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✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (∀'f✝).freeVarFinset }), v (f a) = v' ↑a
x✝ : M
⊢ ∀ (a : { x // x ∈ f✝.freeVarFinset }), v (f a) = v' ↑a

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 xs) ((ts✝ x✝).restrictVarLeft (f ∘ Set.inclusion ⋯)) = realize (Sum.elim v' xs) (ts✝ x✝)

Tactic:
rw [realize_restrictVarLeft v' (by simp [hv'])]

Result:
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✝)

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
⊢ realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₁✝ = realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) t₂✝ ↔
    realize (Sum.elim v' xs) t₁✝ = realize (Sum.elim v' xs) t₂✝

Tactic:
simp [Function.comp_apply]

Result:
no goals

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : { x // x ∈ f✝.freeVarFinset } → β} {xs : Fin (n✝ + 1) → 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✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (∀'f✝).freeVarFinset }), v (f a) = v' ↑a
⊢ (∀ (x : M), (f✝.restrictFreeVar f).Realize v (snoc xs x)) ↔ ∀ (x : M), f✝.Realize v' (snoc xs x)

Tactic:
refine forall_congr' (fun _ => ?_)

Result:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : { x // x ∈ f✝.freeVarFinset } → β} {xs : Fin (n✝ + 1) → 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✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (∀'f✝).freeVarFinset }), v (f a) = v' ↑a
x✝ : M
⊢ (f✝.restrictFreeVar f).Realize v (snoc xs x✝) ↔ f✝.Realize v' (snoc xs x✝)

Proof state:
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
⊢ ∀ (a : { x // x ∈ t₂✝.varFinsetLeft }), Sum.elim v xs (Sum.inl ((f ∘ Set.inclusion ⋯) a)) = v' ↑a

Tactic:
simp [hv']

Result:
no goals

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
⊢ (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)

Tactic:
congr!

Result:
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 xs) ((ts✝ x✝).restrictVarLeft (f ∘ Set.inclusion ⋯)) = realize (Sum.elim v' xs) (ts✝ x✝)