-- Mathlib/ModelTheory/Semantics.lean
theorem realize_mapTermRel_id [L'.Structure M]
    {ft : ∀ n, L.Term (α ⊕ (Fin n)) → L'.Term (β ⊕ (Fin n))}
    {fr : ∀ n, L.Relations n → L'.Relations n} {n} {φ : L.BoundedFormula α n} {v : α → M}
    {v' : β → M} {xs : Fin n → M}
    (h1 :
      ∀ (n) (t : L.Term (α ⊕ (Fin n))) (xs : Fin n → M),
        (ft n t).realize (Sum.elim v' xs) = t.realize (Sum.elim v xs))
    (h2 : ∀ (n) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x) :
    (φ.mapTermRel ft fr fun _ => id).Realize v' xs ↔ φ.Realize v xs

Proof state:
case equal
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x => id) (equal t₁✝ t₂✝)).Realize v' xs ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
simp [mapTermRel, Realize, h1]

Result:
no goals

Proof state:
case all
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih : ∀ {xs : Fin (n✝ + 1) → M}, (mapTermRel ft fr (fun x => id) f✝).Realize v' xs ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x => id) (∀'f✝)).Realize v' xs ↔ (∀'f✝).Realize v xs

Tactic:
simp only [mapTermRel, Realize, ih, id]

Result:
no goals

Proof state:
case falsum
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x => id) falsum).Realize v' xs ↔ falsum.Realize v xs

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
v : α → M
v' : β → M
xs : Fin n → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
⊢ (mapTermRel ft fr (fun x => id) φ).Realize v' xs ↔ φ.Realize v xs

Tactic:
induction φ with
| falsum => rfl
| equal => simp [mapTermRel, Realize, h1]
| rel => simp [mapTermRel, Realize, h1, h2]
| imp _ _ ih1 ih2 => simp [mapTermRel, Realize, ih1, ih2]
| all _ ih => simp only [mapTermRel, Realize, ih, id]

Result:
no goals

Proof state:
case rel
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x => id) (rel R✝ ts✝)).Realize v' xs ↔ (rel R✝ ts✝).Realize v xs

Tactic:
simp [mapTermRel, Realize, h1, h2]

Result:
no goals

Proof state:
case imp
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, (mapTermRel ft fr (fun x => id) f₁✝).Realize v' xs ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, (mapTermRel ft fr (fun x => id) f₂✝).Realize v' xs ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x => id) (f₁✝ ⟹ f₂✝)).Realize v' xs ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
simp [mapTermRel, Realize, ih1, ih2]

Result:
no goals