mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case e'_3.e'_3.func
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term β
t_ih : ∀ (a_1 : Fin l✝), Term.realize (fun i ↦ x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ (funMap _f✝ fun i ↦ Term.realize x (_ts✝ i) a) = funMap _f✝ (fun i ↦ Term.realize x (_ts✝ i)) a

Tactic:
;

Goal state after:
case e'_3.e'_3.func
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
a : α
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term β
t_ih : ∀ (a_1 : Fin l✝), Term.realize (fun i ↦ x i a) (_ts✝ a_1) = Term.realize x (_ts✝ a_1) a
⊢ (funMap _f✝ fun i ↦ Term.realize x (_ts✝ i) a) = funMap _f✝ (fun i ↦ Term.realize x (_ts✝ i)) a
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
β : Type u_3
x : β → (a : α) → M a
t : L.Term β
⊢ Term.realize (fun i ↦ Quotient.mk' (x i)) t = Quotient.mk' fun a ↦ Term.realize (fun i ↦ x i a) t

Tactic:
convert!
    @Term.realize_quotient_mk' L _ ((u : Filter α).productSetoid M)
      (Ultraproduct.setoidPrestructure M u) _ t x using 2
  ext a
  induction t with
  | var => rfl
  | func _ _ t_ih => simp only [Term.realize, t_ih]; rfl

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
i : Fin l✝
| Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)

Tactic:
;

Goal state after:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
i : Fin l✝
| Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m ≤ n
⊢ (liftAt n' m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
liftAt

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m ≤ n
⊢ (mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ).Realize v xs ↔
    φ.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case pos
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},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
h✝ : k < m
⊢ k = k + n'

Tactic:
;

Goal state after:
case pos
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},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
h✝ : k < m
⊢ k = k + n'
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + n') → M
hmn : m ≤ n
⊢ (liftAt n' m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
by
  rw [liftAt]
  induction φ with
  | falsum => simp [mapTermRel, Realize]
  | equal => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | rel => simp [mapTermRel, Realize, Sum.elim_comp_map]
  | imp _ _ ih1 ih2 => simp only [mapTermRel, Realize, ih1 hmn, ih2 hmn]
  | @all k _ ih3 =>
    have h : k + 1 + n' = k + n' + 1 := by rw [add_assoc, add_comm 1 n', ← add_assoc]
    simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.le_succ)]
    refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))
    · simp only [Function.comp_apply, val_last, snoc_last]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_last _ _)
      split_ifs <;> dsimp; lia
    · simp only [Function.comp_apply, Fin.snoc_castSucc]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
      simp only [val_castSucc, val_cast]
      split_ifs <;> simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
q : L.Substructure M
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝, fun_mem := fun_mem✝ } = ↑q
⊢ { carrier := carrier✝, fun_mem := fun_mem✝ } = q

Tactic:
;

Goal state after:
case mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
q : L.Substructure M
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝, fun_mem := fun_mem✝ } = ↑q
⊢ { carrier := carrier✝, fun_mem := fun_mem✝ } = q
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case mk.mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
carrier✝¹ : Set M
fun_mem✝¹ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝¹
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = ↑{ carrier := carrier✝, fun_mem := fun_mem✝ }
⊢ { carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = { carrier := carrier✝, fun_mem := fun_mem✝ }

Tactic:
;

Goal state after:
case mk.mk
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
carrier✝¹ : Set M
fun_mem✝¹ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝¹
carrier✝ : Set M
fun_mem✝ : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f carrier✝
h : ↑{ carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = ↑{ carrier := carrier✝, fun_mem := fun_mem✝ }
⊢ { carrier := carrier✝¹, fun_mem := fun_mem✝¹ } = { carrier := carrier✝, fun_mem := fun_mem✝ }
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: 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 : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
x✝ : M
⊢ ∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a

Tactic:
;

Goal state after:
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 : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
x✝ : M
⊢ ∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
xs : Fin n → M
R : (constantsOn α).Relations n
⊢ RelMap
      ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) (Sum.inr R)))
      xs ↔
    RelMap (Sum.inr R) xs

Tactic:
· exact isEmptyElim R

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case falsum
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l) = ⟨n✝, falsum⟩ :: listDecode l

Tactic:
;

Goal state after:
case falsum
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ listDecode (⟨n✝, falsum⟩.snd.listEncode ++ l) = ⟨n✝, falsum⟩ :: listDecode l
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ Term.realize (Sum.elim v xs) t₁✝ = Term.realize (Sum.elim v xs) t₂✝ ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
;

Goal state after:
case equal
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ Term.realize (Sum.elim v xs) t₁✝ = Term.realize (Sum.elim v xs) t₂✝ ↔ (equal t₁✝ t₂✝).Realize v xs
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__xs
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
i : Fin 0
⊢ y i = default i

Tactic:
;

Goal state after:
case e__xs
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
i : Fin 0
⊢ y i = default i
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__v.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
a : Empty
⊢ ((fun a ↦ ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) (Sum.inr a) = Sum.elim (fun a ↦ ↑(L.con a)) default (Sum.inr a)

Tactic:
· cases a

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v

Tactic:
;

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iAlls β φ) v v' = (Formula.iAlls β φ).Realize v
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Tactic:
;

Goal state after:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
v' : Fin 0 → M
⊢ v' = default
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
x✝ : ↥s
⊢ ((Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding) x✝ = (f.comp s.subtype) x✝

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
x✝ : ↥s
⊢ ((Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding) x✝ = (f.comp s.subtype) x✝
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
x✝ : M
⊢ (f.toHom.range.subtype.comp f.equivRange.toEmbedding) x✝ = f x✝

Tactic:
;

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
x✝ : M
⊢ (f.toHom.range.subtype.comp f.equivRange.toEmbedding) x✝ = f x✝
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v

Tactic:
;

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExs γ φ) v v' = (Formula.iExs γ φ).Realize v
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default

Tactic:
;

Goal state after:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ v' = default
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_8
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
i : Fin (n + 1)
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) i =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      i

Tactic:
;

Goal state after:
case e'_8
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
i : Fin (n + 1)
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) i =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      i
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (t ⊔ sᶜ)

Tactic:
;

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (t ⊔ sᶜ)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
⊢ (Realize φ (fun x ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) =
    (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)

Tactic:
;

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
⊢ (Realize φ (fun x ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) =
    (Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
i : ℕ
| lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))

Tactic:
;

Goal state after:
L : Language
i : ℕ
| lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v

Tactic:
;

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
v' : Fin 0 → M
⊢ Realize (Formula.iExsUnique γ φ) v v' = (Formula.iExsUnique γ φ).Realize v
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ #↑s + #↑(⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s')

Tactic:
rw [← lift_le, lift_add, h, add_comm, add_eq_max h1]
      exact max_le le_rfl h2

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst✝ : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L {w | w ∘ Sum.inr ∈ S}
⊢ A.Definable L (F ⁻¹' S)

Tactic:
convert! Definable.exists_of_finite (Definable.inter h_graph h_cyl) using 1

Goal state after:
M : Type u_1
L : Language
inst✝¹ : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst✝ : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L {w | w ∘ Sum.inr ∈ S}
⊢ F ⁻¹' S = {v | ∃ u, Sum.elim v u ∈ {w | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w | w ∘ Sum.inr ∈ S}}
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
C : L[[↑A]].Constants
⊢ Function.const (α → M) ↑C = fun v ↦ ↑C

Tactic:
;

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
C : L[[↑A]].Constants
⊢ Function.const (α → M) ↑C = fun v ↦ ↑C
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : (i : ι) × ↥(monoms i) → R
x✝ : (i : ι) × ↥(monoms i)
⊢ (fun p i ↦ coeff (↑i.snd) (↑p i.fst))
      ((fun p ↦
          ⟨fun i ↦
            AddMonoidAlgebra.ofCoeff
              { support := {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0},
                toFun := fun m ↦ if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0, mem_support_toFun := ⋯ },
            ⋯⟩)
        p)
      x✝ =
    p x✝

Tactic:
;

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : (i : ι) × ↥(monoms i) → R
x✝ : (i : ι) × ↥(monoms i)
⊢ (fun p i ↦ coeff (↑i.snd) (↑p i.fst))
      ((fun p ↦
          ⟨fun i ↦
            AddMonoidAlgebra.ofCoeff
              { support := {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0},
                toFun := fun m ↦ if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0, mem_support_toFun := ⋯ },
            ⋯⟩)
        p)
      x✝ =
    p x✝
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case refine_1
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ ℵ₀ < κ

Tactic:
;

Goal state after:
case refine_1
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ ℵ₀ < κ
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
q : Nat.Primes
a✝ : q ∉ ∅
⊢ ψ ∈
    Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∪
      if ↑q = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime ↑q then {eqZero ↑q} else {⊥}

Tactic:
;

Goal state after:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
q : Nat.Primes
a✝ : q ∉ ∅
⊢ ψ ∈
    Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∪
      if ↑q = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime ↑q then {eqZero ↑q} else {⊥}
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
x✝ : MvPolynomial σ k
⊢ x✝ ∈ vanishingIdeal k {x} ↔ x✝ ∈ RingHom.ker (aeval x)

Tactic:
;

Goal state after:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
x✝ : MvPolynomial σ k
⊢ x✝ ∈ vanishingIdeal k {x} ↔ x✝ ∈ RingHom.ker (aeval x)
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: case e'_3
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.ring.toSemiring
x✝ : MvPolynomial σ K
⊢ x✝ ∈ vanishingIdeal K {x} ↔ x✝ ∈ RingHom.ker (aeval x)

Tactic:
;

Goal state after:
case e'_3
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.ring.toSemiring
x✝ : MvPolynomial σ K
⊢ x✝ ∈ vanishingIdeal K {x} ↔ x✝ ∈ RingHom.ker (aeval x)
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
z : K
⊢ ∃ a, (aeval x) a = z

Tactic:
;

Goal state after:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
z : K
⊢ ∃ a, (aeval x) a = z
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
z : K
⊢ (aeval x) (C z) = z

Tactic:
;

Goal state after:
case h
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
z : K
⊢ (aeval x) (C z) = z