awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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']
-- 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_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)

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

Premises used: forall_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 : ℕ
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 : α)
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)
⊢ (∀ (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)

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

Premises used: forall_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 : ℕ
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
all : ∀ (a : ↥f_1.freeVarFinset), v (f a) = v' (↑a : α)
⊢ (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:
rw [ih3]
-- 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_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
⊢ ∀ (a : ↥f_1.freeVarFinset), v (f a) = v' (↑a : α)

Tactic:
simp [hv']
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : DecidableEq α
n : ℕ
φ : L.BoundedFormula α n
s : Set α
h : (↑φ.freeVarFinset : Set α) ⊆ s
v : α → M
xs : Fin n → M
⊢ ∀ (a : ↥φ.freeVarFinset),
    (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Set.inclusion (s := (↑φ.freeVarFinset : Set α)) (t := s) h a) =
      v (↑a : α)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
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

Tactic:
realize_mapTermRel_id (fun n t xs => realize_constantsVarsEquivLeft) fun n R xs => ?_

Premises used: FirstOrder.Language.Term.realize_constantsVarsEquivLeft, FirstOrder.Language.BoundedFormula.realize_mapTermRel_id
-- Module: Mathlib.ModelTheory.Semantics
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
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
⊢ Realize (L := L) (α := α ⊕ β) ((constantsVarsEquiv : (a : L[[α]].BoundedFormula β n) → L.BoundedFormula (α ⊕ β) n) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs ↔
    φ.Realize v xs

Tactic:
refine realize_mapTermRel_id (fun n t xs => realize_constantsVarsEquivLeft) fun n R xs => ?_

Premises used: FirstOrder.Language.Term.realize_constantsVarsEquivLeft, FirstOrder.Language.BoundedFormula.realize_mapTermRel_id
-- Module: Mathlib.ModelTheory.Semantics
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
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
⊢ 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:
erw [← (lhomWithConstants L α).map_onRelation
      (Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n) R) xs]

Premises used: FirstOrder.Language.constantsOn, FirstOrder.Language.Relations, FirstOrder.Language.LHom.map_onRelation, FirstOrder.Language.lhomWithConstants, DFunLike.coe, Equiv.sumEmpty
-- Module: Mathlib.ModelTheory.Semantics
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 :
  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
⊢ 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
-- Module: Mathlib.ModelTheory.Semantics
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
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
⊢ 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:
obtain - | R := R
-- Module: Mathlib.ModelTheory.Semantics
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 : ℕ
xs : Fin n → M
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:
simp
-- Module: Mathlib.ModelTheory.Semantics
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 : ℕ
xs : Fin n → M
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:
isEmptyElim R

Premises used: isEmptyElim
-- Module: Mathlib.ModelTheory.Semantics
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 : ℕ
xs : Fin n → M
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:
exact isEmptyElim R
-- Module: Mathlib.ModelTheory.Semantics
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
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
⊢ Realize.{u, v, w, v'} (L := L) ((relabelEquiv g : (a : L.BoundedFormula α k) → L.BoundedFormula β k) φ) v xs ↔
    φ.Realize (v ∘ (⇑g : (a : α) → β)) xs

Tactic:
simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]

Premises used: Equiv.coe_refl, FirstOrder.Language.BoundedFormula.mapTermRelEquiv_apply, FirstOrder.Language.BoundedFormula.relabelEquiv
-- Module: Mathlib.ModelTheory.Semantics
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

Tactic:
realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl

Premises used: FirstOrder.Language.BoundedFormula.realize_mapTermRel_id, rfl
-- Module: Mathlib.ModelTheory.Semantics
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
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
⊢ 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:
refine realize_mapTermRel_id (fun n t xs => ?_) fun _ _ _ => rfl

Premises used: FirstOrder.Language.BoundedFormula.realize_mapTermRel_id, rfl
-- Module: Mathlib.ModelTheory.Semantics
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
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
⊢ 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:
simp only [relabelEquiv_apply, Term.realize_relabel]

Premises used: FirstOrder.Language.Term.realize_relabel, FirstOrder.Language.Term.relabelEquiv_apply
-- Module: Mathlib.ModelTheory.Semantics
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

Tactic:
congr (congr rfl ?_) rfl

Premises used: congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
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
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)
⊢ 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:
refine congr (congr rfl ?_) rfl

Premises used: congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
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)
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)
⊢ 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:
ext (i | i)
-- Module: Mathlib.ModelTheory.Semantics
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
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:
rfl
-- Module: Mathlib.ModelTheory.Semantics
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
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:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : Nonempty M
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (∀' liftAt 1 n φ).Realize v xs ↔ φ.Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
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 : ℕ
xs : Fin n_1 → M
⊢ Realize (φ.onBoundedFormula falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) falsum v xs

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
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
equal : Term.realize (Sum.elim v xs) t₁ = Term.realize (Sum.elim v xs) t₂ ↔ (BoundedFormula.equal t₁ t₂).Realize v xs
⊢ (φ.onBoundedFormula (BoundedFormula.equal t₁ t₂)).Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v xs

Tactic:
simp only [onBoundedFormula, realize_bdEqual, realize_onTerm]

Premises used: FirstOrder.Language.LHom.realize_onTerm, FirstOrder.Language.BoundedFormula.realize_bdEqual, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Semantics
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
⊢ Term.realize (Sum.elim v xs) t₁ = Term.realize (Sum.elim v xs) t₂ ↔ (equal t₁ t₂).Realize v xs

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
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
rel :
  (RelMap.{u, v, w} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)) ↔
    (BoundedFormula.rel R ts).Realize v xs
⊢ (φ.onBoundedFormula (BoundedFormula.rel R ts)).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v xs

Tactic:
simp only [onBoundedFormula, realize_rel, LHom.map_onRelation,
      Function.comp_apply, realize_onTerm]

Premises used: FirstOrder.Language.LHom.map_onRelation, FirstOrder.Language.LHom.realize_onTerm, FirstOrder.Language.BoundedFormula.realize_rel, Function.comp_apply, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Semantics
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
⊢ (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:
rfl
-- Module: Mathlib.ModelTheory.Semantics
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 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : ∀ {xs : Fin n_1 → M}, (φ.onBoundedFormula f₁).Realize v xs ↔ f₁.Realize v xs
ih2 : ∀ {xs : Fin n_1 → M}, (φ.onBoundedFormula f₂).Realize v xs ↔ f₂.Realize v xs
xs : Fin n_1 → M
⊢ (φ.onBoundedFormula (f₁ ⟹ f₂)).Realize v xs ↔ (f₁ ⟹ f₂).Realize v xs

Tactic:
simp only [onBoundedFormula, ih1, ih2, realize_imp]

Premises used: FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Semantics
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 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : ∀ {xs : Fin (n_1 + 1) → M}, (φ.onBoundedFormula f).Realize v xs ↔ f.Realize v xs
xs : Fin n_1 → M
⊢ (φ.onBoundedFormula (∀' f)).Realize v xs ↔ (∀' f).Realize v xs

Tactic:
simp only [onBoundedFormula, ih3, realize_all]

Premises used: FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Semantics
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
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    Realize (φ.onBoundedFormula BoundedFormula.falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (φ.onBoundedFormula (BoundedFormula.equal t₁ t₂)).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)) {xs : Fin n → M},
    (φ.onBoundedFormula (BoundedFormula.rel R ts)).Realize v xs ↔ (BoundedFormula.rel R ts).Realize v xs
imp :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 : ∀ {xs : Fin n → M}, (φ.onBoundedFormula f₁).Realize v xs ↔ f₁.Realize v xs)
    (ih2 : ∀ {xs : Fin n → M}, (φ.onBoundedFormula f₂).Realize v xs ↔ f₂.Realize v xs) {xs : Fin n → M},
    (φ.onBoundedFormula (f₁ ⟹ f₂)).Realize v xs ↔ (f₁ ⟹ f₂).Realize v xs
all :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
    (ih3 : ∀ {xs : Fin (n + 1) → M}, (φ.onBoundedFormula f).Realize v xs ↔ f.Realize v xs) {xs : Fin n → M},
    (φ.onBoundedFormula (∀' f)).Realize v xs ↔ (∀' f).Realize v xs
⊢ (φ.onBoundedFormula ψ).Realize v xs ↔ ψ.Realize 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]

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.LHom.map_onRelation, FirstOrder.Language.LHom.realize_onTerm, FirstOrder.Language.BoundedFormula.realize_rel, FirstOrder.Language.BoundedFormula.realize_bdEqual, Function.comp_apply, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.LHom.onBoundedFormula, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel