awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
⊢ snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x
      (Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    xs (if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
(congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)

Premises used: Fin.snoc_castSucc, Fin.ext, congr, rfl, Eq.trans
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
all :
  (↑(Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) : ℕ) =
    (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n').castSucc : ℕ)
⊢ snoc (α := fun (a : Fin (k + n' + 1)) ↦ M) xs x
      (Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) =
    xs (if (↑i : ℕ) < m then castAdd n' i else i.addNat n')

Tactic:
refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)

Premises used: Fin.ext, congr, rfl, Eq.trans
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
all :
  (↑(if (↑i : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n') : ℕ) =
    (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n') : ℕ)
⊢ (↑(Fin.cast h (if (↑i.castSucc : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n')) : ℕ) =
    (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n').castSucc : ℕ)

Tactic:
simp only [val_castSucc, val_cast]

Premises used: Fin.val_cast, Fin.val_castSucc
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
pos : (↑i : ℕ) < m → (↑(castAdd n' i.castSucc) : ℕ) = (↑(castAdd n' i) : ℕ)
neg : ¬(↑i : ℕ) < m → (↑(i.castSucc.addNat n') : ℕ) = (↑(i.addNat n') : ℕ)
⊢ (↑(if (↑i : ℕ) < m then castAdd n' i.castSucc else i.castSucc.addNat n') : ℕ) =
    (↑(if (↑i : ℕ) < m then castAdd n' i else i.addNat n') : ℕ)

Tactic:
split_ifs
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
h_1 : (↑i : ℕ) < m
⊢ (↑(castAdd n' i.castSucc) : ℕ) = (↑(castAdd n' i) : ℕ)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M} (hmn : m + n' ≤ k + 1 + 1),
    Realize.{u, v, w, u'} (L := L)
        (mapTermRel (L := L) (α := α) (fun (x : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin x)) ↦ Term.liftAt n' m t)
          (fun (x : ℕ) ↦ id) (fun (x : ℕ) ↦ castLE ⋯) f)
        v xs ↔
      f.Realize v (xs ∘ fun (i : Fin (k + 1)) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n')
xs : Fin (k + n') → M
hmn : m + n' ≤ k + 1
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
h_1 : ¬(↑i : ℕ) < m
⊢ (↑(i.castSucc.addNat n') : ℕ) = (↑(i.addNat n') : ℕ)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
hmn : m ≤ n
⊢ Realize (liftAt 1 m φ) v xs ↔ φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < m then i.castSucc else i.succ)

Tactic:
simp [realize_liftAt, hmn, castSucc]

Premises used: Fin.castSucc, FirstOrder.Language.BoundedFormula.realize_liftAt
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
rw : φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)
⊢ Realize (liftAt 1 n φ) v xs ↔ φ.Realize v (xs ∘ castSucc)

Tactic:
rw [realize_liftAt_one (refl n), iff_eq_eq]

Premises used: FirstOrder.Language.BoundedFormula.realize_liftAt_one, iff_eq_eq, refl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)

Tactic:
congr rfl (congr rfl (funext fun i => ?_))

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
refine : ∀ (i : Fin n), (if (↑i : ℕ) < n then i.castSucc else i.succ) = i.castSucc
⊢ φ.Realize v (xs ∘ fun (i : Fin n) ↦ if (↑i : ℕ) < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)

Tactic:
refine congr rfl (congr rfl (funext fun i => ?_))

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
i : Fin n
rw rw₁ : i.castSucc = i.castSucc
⊢ (if (↑i : ℕ) < n then i.castSucc else i.succ) = i.castSucc

Tactic:
rw [if_pos i.is_lt]

Premises used: Fin.is_lt, if_pos
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
rw :
  realize (fun (a : α ⊕ Fin n) ↦ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t =
    realize (Sum.elim (fun (a : α) ↦ realize v (tf a)) x) t
⊢ realize (Sum.elim v x) (t.subst (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr))) =
    realize (Sum.elim (fun (a : α) ↦ realize v (tf a)) x) t

Tactic:
rw [Term.realize_subst]

Premises used: FirstOrder.Language.Term.realize_subst
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
e_v :
  ∀ (a : α ⊕ Fin n),
    realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a) =
      Sum.elim (fun (a : α) ↦ realize v (tf a)) x a
⊢ realize (fun (a : α ⊕ Fin n) ↦ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t =
    realize (Sum.elim (fun (a : α) ↦ realize v (tf a)) x) t

Tactic:
rcongr a
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
a : α ⊕ Fin n
e_v :
  ∀ (val : α),
    realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val)) =
      Sum.elim (fun (a : α) ↦ realize v (tf a)) x (Sum.inl val)
e_v₁ :
  ∀ (val : Fin n),
    realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val)) =
      Sum.elim (fun (a : α) ↦ realize v (tf a)) x (Sum.inr val)
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x a

Tactic:
cases a
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
val : α
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val)) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x (Sum.inl val)

Tactic:
simp only [Sum.elim_inl, Function.comp_apply, Term.realize_relabel, Sum.elim_comp_inl]

Premises used: Sum.elim_comp_inl, FirstOrder.Language.Term.realize_relabel, Sum.elim_inl, Function.comp_apply
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n_1 : ℕ
φ : L.BoundedFormula α n_1
tf : α → L.Term β
v : β → M
xs : Fin n_1 → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
x : Fin n → M
val : Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val)) =
    Sum.elim (fun (a : α) ↦ realize v (tf a)) x (Sum.inr val)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n : ℕ
φ : L.BoundedFormula α n
tf : α → L.Term β
v : β → M
xs : Fin n → M
⊢ ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (id R) x = RelMap R x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
f : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n_1) falsum) → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n_1) falsum)), v (f a) = v' (↑a : α)
⊢ (restrictFreeVar falsum f).Realize v xs ↔ Realize.{u, v, w, u'} (L := L) falsum v' xs

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)
equal :
  realize (Sum.elim v xs)
        (t₁.restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑t₁.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
              ⋯)) =
      realize (Sum.elim v xs)
        (t₂.restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑t₂.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
              ⋯)) ↔
    realize (Sum.elim v' xs) t₁ = realize (Sum.elim v' xs) t₂
⊢ ((BoundedFormula.equal t₁ t₂).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v' xs

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

Premises used: FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.restrictFreeVar, FirstOrder.Language.BoundedFormula.freeVarFinset.eq_2
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(equal t₁ t₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)
⊢ ∀ (a : ↥t₁.varFinsetLeft),
    Sum.elim v xs
        (Sum.inl
          ((f ∘
              Set.inclusion (s := (↑t₁.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
                ⋯)
            a)) =
      v' (↑a : α)

Tactic:
simp [hv']
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(equal t₁ t₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)
⊢ ∀ (a : ↥t₂.varFinsetLeft),
    Sum.elim v xs
        (Sum.inl
          ((f ∘
              Set.inclusion (s := (↑t₂.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
                ⋯)
            a)) =
      v' (↑a : α)

Tactic:
simp [hv']
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)
equal :
  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₂
⊢ realize (Sum.elim v xs)
        (t₁.restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑t₁.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
              ⋯)) =
      realize (Sum.elim v xs)
        (t₂.restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑t₂.varFinsetLeft : Set α)) (t := (↑(t₁.varFinsetLeft ∪ t₂.varFinsetLeft) : Set α))
              ⋯)) ↔
    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'])]

Premises used: FirstOrder.Language.Term.realize_restrictVarLeft
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(equal t₁ t₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(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
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(BoundedFormula.rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(BoundedFormula.rel R ts).freeVarFinset), v (f a) = v' (↑a : α)
rel :
  (RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦
      realize (Sum.elim v xs)
        ((ts i).restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑(ts i).varFinsetLeft : Set α)) (t :=
              (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) ⋯))) ↔
    RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ realize (Sum.elim v' xs) (ts i)
⊢ ((BoundedFormula.rel R ts).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v' xs

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

Premises used: FirstOrder.Language.BoundedFormula.freeVarFinset.eq_3, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.restrictFreeVar
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(BoundedFormula.rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(BoundedFormula.rel R ts).freeVarFinset), v (f a) = v' (↑a : α)
rel :
  ∀ (x : Fin l),
    realize (Sum.elim v xs)
        ((ts x).restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑(ts x).varFinsetLeft : Set α)) (t :=
              (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) ⋯)) =
      realize (Sum.elim v' xs) (ts x)
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦
      realize (Sum.elim v xs)
        ((ts i).restrictVarLeft
          (f ∘
            Set.inclusion (s := (↑(ts i).varFinsetLeft : Set α)) (t :=
              (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) ⋯))) ↔
    RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ realize (Sum.elim v' xs) (ts i)

Tactic:
congr!
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(rel R ts).freeVarFinset), v (f a) = v' (↑a : α)
x : Fin l
⊢ ∀ (a : ↥(ts x).varFinsetLeft),
    Sum.elim v xs
        (Sum.inl
          ((f ∘
              Set.inclusion (s := (↑(ts x).varFinsetLeft : Set α)) (t :=
                (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) ⋯)
            a)) =
      v' (↑a : α)

Tactic:
simp [hv']
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(BoundedFormula.rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(BoundedFormula.rel R ts).freeVarFinset), v (f a) = v' (↑a : α)
x : Fin l
rel : realize (Sum.elim v' (Sum.elim v xs ∘ Sum.inr)) (ts x) = realize (Sum.elim v' xs) (ts x)
⊢ realize (Sum.elim v xs)
      ((ts x).restrictVarLeft
        (f ∘
          Set.inclusion (s := (↑(ts x).varFinsetLeft : Set α)) (t :=
            (↑(Finset.biUnion Finset.univ fun (i : Fin l) ↦ (ts i).varFinsetLeft) : Set α)) ⋯)) =
    realize (Sum.elim v' xs) (ts x)

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

Premises used: FirstOrder.Language.Term.realize_restrictVarLeft
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
f : ↥(rel R ts).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(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
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₁.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₁.restrictFreeVar f).Realize v xs ↔ f₁.Realize v' xs
ih2 :
  ∀ {f : ↥f₂.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₂.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₂.restrictFreeVar f).Realize v xs ↔ f₂.Realize v' xs
f : ↥(f₁ ⟹ f₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)
imp :
  (f₁.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₁.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs →
      (f₂.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs ↔
    f₁.Realize v' xs → f₂.Realize v' xs
⊢ ((f₁ ⟹ f₂).restrictFreeVar f).Realize v xs ↔ (f₁ ⟹ f₂).Realize v' xs

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

Premises used: FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.restrictFreeVar, FirstOrder.Language.BoundedFormula.freeVarFinset.eq_4
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₁.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₁.restrictFreeVar f).Realize v xs ↔ f₁.Realize v' xs
ih2 :
  ∀ {f : ↥f₂.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₂.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₂.restrictFreeVar f).Realize v xs ↔ f₂.Realize v' xs
f : ↥(f₁ ⟹ f₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)
imp :
  ∀ (a : ↥f₂.freeVarFinset),
    v
        ((f ∘
            Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α)) ⋯)
          a) =
      v' (↑a : α)
imp₁ :
  ∀ (a : ↥f₁.freeVarFinset),
    v
        ((f ∘
            Set.inclusion (s := (↑f₁.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α)) ⋯)
          a) =
      v' (↑a : α)
⊢ (f₁.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₁.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs →
      (f₂.restrictFreeVar
            (f ∘
              Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α))
                ⋯)).Realize
        v xs ↔
    f₁.Realize v' xs → f₂.Realize v' xs

Tactic:
rw [ih1, ih2]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₁.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₁.restrictFreeVar f).Realize v xs ↔ f₁.Realize v' xs
ih2 :
  ∀ {f : ↥f₂.freeVarFinset → β} {xs : Fin n_1 → M} (hv' : ∀ (a : ↥f₂.freeVarFinset), v (f a) = v' (↑a : α)),
    (f₂.restrictFreeVar f).Realize v xs ↔ f₂.Realize v' xs
f : ↥(f₁ ⟹ f₂).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)
⊢ ∀ (a : ↥f₂.freeVarFinset),
    v
        ((f ∘
            Set.inclusion (s := (↑f₂.freeVarFinset : Set α)) (t := (↑(f₁.freeVarFinset ∪ f₂.freeVarFinset) : Set α)) ⋯)
          a) =
      v' (↑a : α)

Tactic:
simp [hv']