awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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_1 : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {f : ↥f_1.freeVarFinset → β} {xs : Fin (n_1 + 1) → M} (hv' : ∀ (a : ↥f_1.freeVarFinset), v (f a) = v' (↑a : α)),
    (f_1.restrictFreeVar f).Realize v xs ↔ f_1.Realize v' xs
f : ↥(∀' f_1).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(∀' f_1).freeVarFinset), v (f a) = v' (↑a : α)
⊢ (∀ (x : M), (f_1.restrictFreeVar f).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)) ↔
    ∀ (x : M), f_1.Realize v' (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
have all : ∀ (x : M),
  (f_1.restrictFreeVar f).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x) ↔
    f_1.Realize v' (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
Tactic: refine forall_congr' (fun _ => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
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_1 : L.BoundedFormula α (n_1 + 1)
ih3 :
  ∀ {f : ↥f_1.freeVarFinset → β} {xs : Fin (n_1 + 1) → M} (hv' : ∀ (a : ↥f_1.freeVarFinset), v (f a) = v' (↑a : α)),
    (f_1.restrictFreeVar f).Realize v xs ↔ f_1.Realize v' xs
f : ↥(∀' f_1).freeVarFinset → β
xs : Fin n_1 → M
hv' : ∀ (a : ↥(∀' f_1).freeVarFinset), v (f a) = v' (↑a : α)
x : M
⊢ (f_1.restrictFreeVar f).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x) ↔
    f_1.Realize v' (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs x)
have all : ∀ (a : ↥f_1.freeVarFinset), v (f a) = v' (↑a : α)
Tactic: rw [ih3]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' (↑a : α)
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs
have falsum : ∀ {n : ℕ} {f : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) falsum) → β} {xs : Fin n → M}
  (hv' : ∀ (a : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) falsum)), v (f a) = v' (↑a : α)),
  (restrictFreeVar falsum f).Realize v xs ↔ Realize.{u, v, w, u'} (L := L) falsum 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
  | rel =>
    simp only [Realize, freeVarFinset.eq_3, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | 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']
Cleared hypotheses: φ, f, xs, hv'
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' (↑a : α)
falsum :
  ∀ {n : ℕ} {f : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum) → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum)), v (f a) = v' (↑a : α)),
    (restrictFreeVar BoundedFormula.falsum f).Realize v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v' xs
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {f : ↥(equal t₁ t₂).freeVarFinset → β} {xs : Fin n → M}
  (hv' : ∀ (a : ↥(equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)),
  ((equal t₁ t₂).restrictFreeVar f).Realize v xs ↔ (equal t₁ t₂).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
  | rel =>
    simp only [Realize, freeVarFinset.eq_3, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | 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']
Cleared hypotheses: φ, f, xs, hv'
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' (↑a : α)
falsum :
  ∀ {n : ℕ} {f : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum) → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum)), v (f a) = v' (↑a : α)),
    (restrictFreeVar BoundedFormula.falsum f).Realize v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v' xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {f : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset → β}
    {xs : Fin n → M} (hv' : ∀ (a : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)),
    ((BoundedFormula.equal t₁ t₂).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v' xs
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {f : ↥(rel R ts).freeVarFinset → β}
  {xs : Fin n → M} (hv' : ∀ (a : ↥(rel R ts).freeVarFinset), v (f a) = v' (↑a : α)),
  ((rel R ts).restrictFreeVar f).Realize v xs ↔ (rel R ts).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
  | rel =>
    simp only [Realize, freeVarFinset.eq_3, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | 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']
Cleared hypotheses: φ, f, xs, hv'
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' (↑a : α)
falsum :
  ∀ {n : ℕ} {f : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum) → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum)), v (f a) = v' (↑a : α)),
    (restrictFreeVar BoundedFormula.falsum f).Realize v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v' xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {f : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset → β}
    {xs : Fin n → M} (hv' : ∀ (a : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)),
    ((BoundedFormula.equal t₁ t₂).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v' xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n))
    {f : ↥(BoundedFormula.rel R ts).freeVarFinset → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(BoundedFormula.rel R ts).freeVarFinset), v (f a) = v' (↑a : α)),
    ((BoundedFormula.rel R ts).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v' xs
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs
have imp : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (ih1 :
    ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n → 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 → 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 → M} (hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)),
  ((f₁ ⟹ f₂).restrictFreeVar f).Realize v xs ↔ (f₁ ⟹ f₂).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
  | rel =>
    simp only [Realize, freeVarFinset.eq_3, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | 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']
Cleared hypotheses: φ, f, xs, hv'
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
f : ↥φ.freeVarFinset → β
v : β → M
xs : Fin n → M
v' : α → M
hv' : ∀ (a : ↥φ.freeVarFinset), v (f a) = v' (↑a : α)
falsum :
  ∀ {n : ℕ} {f : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum) → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(freeVarFinset.{u, v, u'} (L := L) (n := n) BoundedFormula.falsum)), v (f a) = v' (↑a : α)),
    (restrictFreeVar BoundedFormula.falsum f).Realize v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v' xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {f : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset → β}
    {xs : Fin n → M} (hv' : ∀ (a : ↥(BoundedFormula.equal t₁ t₂).freeVarFinset), v (f a) = v' (↑a : α)),
    ((BoundedFormula.equal t₁ t₂).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v' xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n))
    {f : ↥(BoundedFormula.rel R ts).freeVarFinset → β} {xs : Fin n → M}
    (hv' : ∀ (a : ↥(BoundedFormula.rel R ts).freeVarFinset), v (f a) = v' (↑a : α)),
    ((BoundedFormula.rel R ts).restrictFreeVar f).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v' xs
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 :
      ∀ {f : ↥f₁.freeVarFinset → β} {xs : Fin n → 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 → 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 → M} (hv' : ∀ (a : ↥(f₁ ⟹ f₂).freeVarFinset), v (f a) = v' (↑a : α)),
    ((f₁ ⟹ f₂).restrictFreeVar f).Realize v xs ↔ (f₁ ⟹ f₂).Realize v' xs
⊢ (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs
have all : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 :
    ∀ {f_1 : ↥f.freeVarFinset → β} {xs : Fin (n + 1) → M} (hv' : ∀ (a : ↥f.freeVarFinset), v (f_1 a) = v' (↑a : α)),
      (f.restrictFreeVar f_1).Realize v xs ↔ f.Realize v' xs)
  {f_1 : ↥(∀' f).freeVarFinset → β} {xs : Fin n → M} (hv' : ∀ (a : ↥(∀' f).freeVarFinset), v (f_1 a) = v' (↑a : α)),
  ((∀' f).restrictFreeVar f_1).Realize v xs ↔ (∀' f).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
  | rel =>
    simp only [Realize, freeVarFinset.eq_3, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp
  | 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']
Cleared hypotheses: φ, f, xs, hv'
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
φ : L[[α]].BoundedFormula β n
v : β → M
xs : Fin n → M
⊢ Realize (L := L) (α := α ⊕ β) ((constantsVarsEquiv : (a : L[[α]].BoundedFormula β n) → L.BoundedFormula (α ⊕ β) n) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs ↔
    φ.Realize v xs
have refine : ∀ (n : ℕ) (R : L[[α]].Relations n) (xs : Fin n → M),
  RelMap.{u, v, w} (L := L)
      (((fun (x : ℕ) ↦
              (Equiv.sumEmpty (L.Relations x) (Relations.{u', 0} (constantsOn α) x) :
                L.Relations x ⊕ Relations.{u', 0} (constantsOn α) x ≃ L.Relations x))
            n :
          (a : L[[α]].Relations n) → L.Relations n)
        R)
      xs =
    RelMap R xs
Tactic: refine realize_mapTermRel_id (fun n t xs => realize_constantsVarsEquivLeft) fun n R xs => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n_1 : ℕ
φ : L[[α]].BoundedFormula β n_1
v : β → M
xs_1 : Fin n_1 → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap.{u, v, w} (L := L)
      (((fun (x : ℕ) ↦
              (Equiv.sumEmpty (L.Relations x) (Relations.{u', 0} (constantsOn α) x) :
                L.Relations x ⊕ Relations.{u', 0} (constantsOn α) x ≃ L.Relations x))
            n :
          (a : L[[α]].Relations n) → L.Relations n)
        R)
      xs =
    RelMap R xs
have erw : RelMap
    ((L.lhomWithConstants α).onRelation
      ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
          (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
        R))
    xs =
  RelMap R xs
Tactic: erw [← (lhomWithConstants L α).map_onRelation
      (Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n) R) xs]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n_1 : ℕ
φ : L[[α]].BoundedFormula β n_1
v : β → M
xs_1 : Fin n_1 → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
            (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
          R))
      xs =
    RelMap R xs
have a : RelMap
    ((L.lhomWithConstants α).onRelation
      ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
          (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
        R))
    xs ↔
  RelMap R xs
Tactic: rcongr
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n_1 : ℕ
φ : L[[α]].BoundedFormula β n_1
v : β → M
xs_1 : Fin n_1 → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
            (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
          R))
      xs ↔
    RelMap R xs
have a : ∀ (val : L.Relations n),
  RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
            (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
          (Sum.inl val)))
      xs ↔
    RelMap (L := L[[α]]) (Sum.inl val) xs
Tactic: obtain - | R := R
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
n_1 : ℕ
φ : L[[α]].BoundedFormula β n_1
v : β → M
xs_1 : Fin n_1 → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
a :
  ∀ (val : L.Relations n),
    RelMap
        ((L.lhomWithConstants α).onRelation
          ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
              (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
            (Sum.inl val)))
        xs ↔
      RelMap (L := L[[α]]) (Sum.inl val) xs
⊢ RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
            (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
          R))
      xs ↔
    RelMap R xs
have a₁ : ∀ (R : Relations.{u', 0} (constantsOn α) n),
  RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) (Relations.{u', 0} (constantsOn α) n) :
            (a : L.Relations n ⊕ (constantsOn α).Relations n) → L.Relations n)
          (Sum.inr R)))
      xs ↔
    RelMap (L := L[[α]]) (Sum.inr R) xs
Tactic: obtain - | R := R
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ Realize.{u, v, w, v'} (L := L) ((relabelEquiv g : (a : L.BoundedFormula α k) → L.BoundedFormula β k) φ) v xs ↔
    φ.Realize (v ∘ (⇑g : (a : α) → β)) xs
have simp : Realize.{u, v, w, v'} (L := L)
    (mapTermRel.{u, v, u', v', u, v} (L' := L) (β := β) (g := fun (n : ℕ) ↦ n)
      (fun (n : ℕ) ↦
        (⇑(Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n)))) : (a : L.Term (α ⊕ Fin n)) → L.Term (β ⊕ Fin n)))
      (fun (n : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ)
    v xs ↔
  φ.Realize (v ∘ (⇑g : (a : α) → β)) xs
Tactic: simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs : Fin k → M
⊢ Realize.{u, v, w, v'} (L := L)
      (mapTermRel.{u, v, u', v', u, v} (L' := L) (β := β) (g := fun (n : ℕ) ↦ n)
        (fun (n : ℕ) ↦
          (⇑(Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n)))) :
            (a : L.Term (α ⊕ Fin n)) → L.Term (β ⊕ Fin n)))
        (fun (n : ℕ) ↦ id) (fun (x : ℕ) ↦ id) φ)
      v xs ↔
    φ.Realize (v ∘ (⇑g : (a : α) → β)) xs
have refine : ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs : Fin n → M),
  realize.{u, v, w, v'} (L := L) (Sum.elim v xs)
      ((Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : L.Term (α ⊕ Fin n)) → L.Term (β ⊕ Fin n)) t) =
    realize (Sum.elim (v ∘ (⇑g : (a : α) → β)) xs) t
Tactic: refine realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs_1 : Fin k → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
xs : Fin n → M
⊢ realize.{u, v, w, v'} (L := L) (Sum.elim v xs)
      ((Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : L.Term (α ⊕ Fin n)) → L.Term (β ⊕ Fin n)) t) =
    realize (Sum.elim (v ∘ (⇑g : (a : α) → β)) xs) t
have simp : realize (Sum.elim v xs ∘ (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n)) t =
  realize (Sum.elim (v ∘ (⇑g : (a : α) → β)) xs) t
Tactic: simp only [relabelEquiv_apply, Term.realize_relabel]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs_1 : Fin k → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs ∘ (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n)) t =
    realize (Sum.elim (v ∘ (⇑g : (a : α) → β)) xs) t
have refine : Eq (α := α ⊕ Fin n → M) (Sum.elim v xs ∘ (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n))
  (Sum.elim (v ∘ (⇑g : (a : α) → β)) xs)
Tactic: refine congr (congr rfl ?_) rfl
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs_1 : Fin k → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
xs : Fin n → M
⊢ Eq (α := α ⊕ Fin n → M) (Sum.elim v xs ∘ (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n))
    (Sum.elim (v ∘ (⇑g : (a : α) → β)) xs)
have h : ∀ (i : α),
  Function.comp (α := α ⊕ Fin n) (Sum.elim v xs)
      (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n) (Sum.inl i) =
    Sum.elim (v ∘ (⇑g : (a : α) → β)) xs (Sum.inl i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs_1 : Fin k → M
n : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
xs : Fin n → M
h :
  ∀ (i : α),
    Function.comp (α := α ⊕ Fin n) (Sum.elim v xs)
        (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n) (Sum.inl i) =
      Sum.elim (v ∘ (⇑g : (a : α) → β)) xs (Sum.inl i)
⊢ Eq (α := α ⊕ Fin n → M) (Sum.elim v xs ∘ (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n))
    (Sum.elim (v ∘ (⇑g : (a : α) → β)) xs)
have h₁ : ∀ (i : Fin n),
  Function.comp.{u' + 1, v' + 1, w + 1} (α := α ⊕ Fin n) (Sum.elim v xs)
      (⇑(g.sumCongr (_root_.Equiv.refl (Fin n))) : (a : α ⊕ Fin n) → β ⊕ Fin n) (Sum.inr i) =
    Sum.elim.{u', 0, w + 1} (α := α) (v ∘ (⇑g : (a : α) → β)) xs (Sum.inr i)
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
n : ℕ
v : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (φ.onBoundedFormula (equal t₁ t₂)).Realize v xs ↔ (equal t₁ t₂).Realize v xs
have equal : Term.realize (Sum.elim v xs) t₁ = Term.realize (Sum.elim v xs) t₂ ↔ (equal t₁ t₂).Realize v xs
Tactic: simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
n : ℕ
v : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (φ.onBoundedFormula (rel R ts)).Realize v xs ↔ (rel R ts).Realize v xs
have rel : (RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)) ↔ (rel R ts).Realize v xs
Tactic: simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
n : ℕ
ψ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize v xs
have falsum : ∀ {n : ℕ} {xs : Fin n → M}, Realize (φ.onBoundedFormula falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) falsum v xs
Tactic: induction ψ with
  | falsum => rfl
  | equal => simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]; rfl
  | rel =>
    simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]
    rfl
  | imp _ _ ih1 ih2 => simp only [onBoundedFormula, ih1, ih2, realize_imp]
  | all _ ih3 => simp only [onBoundedFormula, ih3, realize_all]
Cleared hypotheses: ψ, xs