mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
f : ↥F⟮x, y⟯ →ₐ[F] (p * q).SplittingField
⊢ minpoly F z = minpoly F (f ⟨z, hz'⟩)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) φ) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
v : Fin n → M
f : L.Functions n
⊢ realize v f.term = funMap f v

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) φ = φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n ≃ L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun n ↦ ⇑(ft n).symm) (fun n ↦ ⇑(fr n).symm) (fun x ↦ id)
      (mapTermRel (fun n ↦ ⇑(ft n)) (fun n ↦ ⇑(fr n)) (fun x ↦ id) φ) =
    φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
g : α → β
v : β → M
⊢ realize v (relabel g t) = realize (v ∘ g) t

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n ≃ L'.Relations n
n : ℕ
φ : L'.BoundedFormula β n
⊢ mapTermRel (fun n ↦ ⇑(ft n)) (fun n ↦ ⇑(fr n)) (fun x ↦ id)
      (mapTermRel (fun n ↦ ⇑(ft n).symm) (fun n ↦ ⇑(fr n).symm) (fun x ↦ id) φ) =
    φ

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x y z : E
hx : x ∈ solvableByRad F E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
hy' : Group.IsSolvable (minpoly F y).Gal
hz' : z ∈ F⟮x, y⟯
⊢ Group.IsSolvable (minpoly F z).Gal

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ realize v (f.apply₁ t) = funMap f ![realize v t]

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
⊢ Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: α : Type u'
n k : ℕ
⊢ relabelAux Sum.inl k = Sum.map id (natAdd n)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α k
⊢ relabel g φ.not = (relabel g φ).not

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (f.apply₂ t₁ t₂) = funMap f ![realize v t₁, realize v t₂]

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
tf : α → L.Term β
v : β → M
⊢ realize v (t.subst tf) = realize (fun a ↦ realize v (tf a)) t

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ relabel g φ.all = (relabel g φ).all

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
⊢ Group.IsSolvable (minpoly F x).Gal

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ relabel g φ.ex = (relabel g φ).ex

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval x) q = 0
⊢ Group.IsSolvable (q * C q.leadingCoeff⁻¹).Gal

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
β : Type v'
inst✝ : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
x : L.Term β
⊢ realize v (x.substFunc fun {n} ↦ c) = realize v x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval x) q = 0
⊢ Group.IsSolvable q.Gal

Tactic:
by

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✝ : DecidableEq α
v : β → M
v' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih :
  ∀ (a : Fin l✝) {f : ↥(_ts✝ a).varFinset → β},
    (∀ (a_1 : ↥(_ts✝ a).varFinset), v (f a_1) = v' ↑a_1) → realize v ((_ts✝ a).restrictVar f) = realize v' (_ts✝ a)
f : ↥(func _f✝ _ts✝).varFinset → β
hv' : ∀ (a : ↥(func _f✝ _ts✝).varFinset), v (f a) = v' ↑a
i : Fin l✝
⊢ ∀ (a : ↥(_ts✝ i).varFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a

Tactic:
by

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✝ : DecidableEq α
t : L.Term α
f : ↥t.varFinset → β
v : β → M
v' : α → M
hv' : ∀ (a : ↥t.varFinset), v (f a) = v' ↑a
⊢ realize v (t.restrictVar f) = realize v' t

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ relabel Sum.inl φ = castLE ⋯ φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
t : L.Term α
s : Set α
h : ↑t.varFinset ⊆ s
v : α → M
⊢ ∀ (a : ↥t.varFinset), (v ∘ Subtype.val) (Set.inclusion h a) = v ↑a

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : CompatibleRing K
n : ℕ
v : Empty → K
⊢ Formula.Realize (eqZero n) v ↔ ↑n = 0

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
ax : FieldAxiom
⊢ K ⊨ ax.toSentence ↔ toProp K ax

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: p : ℕ
K : Type u_1
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : CharP K p
⊢ K ⊨ Theory.fieldOfChar p

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: case oneMul
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ toProp K oneMul

Tactic:
exact one_mul

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ ∀ φ ∈ Theory.field, K ⊨ φ

Tactic:
by

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✝ : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term (α ⊕ γ)
ih :
  ∀ (a : Fin l✝) {f : ↥(_ts✝ a).varFinsetLeft → β},
    (∀ (a_1 : ↥(_ts✝ a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' ↑a_1) →
      realize xs ((_ts✝ a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts✝ a)
f : ↥(func _f✝ _ts✝).varFinsetLeft → β
hxs' : ∀ (a : ↥(func _f✝ _ts✝).varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
i : Fin l✝
⊢ ∀ (a : ↥(_ts✝ i).varFinsetLeft), xs (Sum.inl ((f ∘ Set.inclusion ⋯) a)) = xs' ↑a

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
⊢ (LHom.id L).onBoundedFormula = id

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ (funMap f fun i ↦ ⟦x i⟧) = ⟦funMap f x⟧

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ (RelMap r fun i ↦ ⟦x i⟧) ↔ RelMap r x

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Quotients

Goal state before:
pp: L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
t : L.Term β
x : β → M
⊢ realize (fun i ↦ ⟦x i⟧) t = ⟦realize x t⟧

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ (φ.comp ψ).onBoundedFormula = φ.onBoundedFormula ∘ ψ.onBoundedFormula

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ Theory.fieldOfChar p ↔ CharP K p

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.LeftInverse φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula

Tactic:
by

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✝ : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
f : ↥t.varFinsetLeft → β
xs : β ⊕ γ → M
xs' : α → M
hxs' : ∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' ↑a
⊢ realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
s : Set α
h : ↑t.varFinsetLeft ⊆ s
v : α → M
xs : γ → M
⊢ ∀ (a : ↥t.varFinsetLeft), Sum.elim (v ∘ Subtype.val) xs (Sum.inl (Set.inclusion h a)) = v ↑a

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.RightInverse φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
⊢ L.distinctConstantsTheory s =
    ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) t)

Tactic:
by

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✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L[[α]].Term β
v : β → M
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) t.constantsToVars = realize v t

Tactic:
by

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✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L.Term (α ⊕ β)
v : β → M
⊢ realize v t.varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) t

Tactic:
by

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✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs) (constantsVarsEquivLeft t) = realize (Sum.elim v xs) t

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
t : L.Term α
v : α → M
⊢ Term.realize v (φ.onTerm t) = Term.realize v t

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
t : L.Term α
v : α → M
⊢ Term.realize (⇑g ∘ v) t = g (Term.realize v t)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
⊢ ⊤.Realize v xs ↔ True

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ l).Realize v xs ↔ ∀ φ ∈ l, φ.Realize v xs

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
⊢ ∀ (v : α → M) (xs : Fin k → M), (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)

Tactic:
by

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)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ funMap f x ≈ funMap f y

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t]

Tactic:
by

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)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x = RelMap r y

Tactic:
by

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)
n : ℕ
f : L.Functions n
x : Fin n → (a : α) → M a
⊢ (funMap f fun i ↦ Quotient.mk' (x i)) = Quotient.mk' fun a ↦ funMap f fun i ↦ x i a

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
by

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)
β : 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:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ ∈ l, φ.Realize v xs

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃' θ).Realize v xs ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⇔ ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
m n : ℕ
h : m = n
h' : m ≤ n
φ : L.BoundedFormula α m
v : α → M
xs : Fin n → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

Tactic:
by

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
k : ℕ
φ : L.BoundedFormula β (k + 1)
ih :
  ∀ (v : Fin (k + 1) → (a : α) → M a),
    (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin k → (a : α) → M a
⊢ ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
by

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 : ℕ
φ : L.BoundedFormula β n
x : β → (a : α) → M a
v : Fin n → (a : α) → M a
⊢ (φ.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) fun i ↦ v i a

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
xs : Fin (k + n) → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) φ).Realize v' xs ↔ φ.Realize (v xs) (xs ∘ natAdd k)

Tactic:
by

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
φ : L.Formula β
x : β → (a : α) → M a
⊢ (φ.Realize fun i ↦ Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i ↦ x i a

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List (L.Term α)
h : ∀ (t : L.Term α) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l
⊢ listDecode (flatMap listEncode l) = l

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
m n : ℕ
φ : L.BoundedFormula α n
g : α → β ⊕ Fin m
v : β → M
xs : Fin (m + n) → M
⊢ (relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)

Tactic:
by

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)
φ : L.Sentence
⊢ (↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
inst✝ : L.Structure Q
f g : M ↪ₑ[L] N
h : (fun f ↦ ↑f) f = (fun f ↦ ↑f) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: 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
⊢ k + 1 + n' = k + n' + 1

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List (L.Term α)
⊢ listDecode (flatMap listEncode l) = l

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ (do
        let a ← (listDecode t.listEncode).head?
        pure (some a)).join =
    some t

Tactic:
by

Goal state after: