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
⊢ (aeval ⟨z, hz'⟩) (minpoly F z) = 0

Tactic:
]

Goal state after:
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
⊢ (aeval ⟨z, hz'⟩) (minpoly F z) = 0
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x✝¹ n' m : ℕ
φ : L.BoundedFormula α x✝¹
x✝ : ℕ
⊢ x✝ + (n' + 1) ≤ x✝ + (n' + 1)

Tactic:
]

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⟯
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
key : minpoly F z = minpoly F (f ⟨z, hz'⟩)
⊢ Group.IsSolvable (minpoly F (f ⟨z, hz'⟩)).Gal

Tactic:
]

Goal state after:
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
key : minpoly F z = minpoly F (f ⟨z, hz'⟩)
⊢ Group.IsSolvable (minpoly F (f ⟨z, hz'⟩)).Gal
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
⊢ (funMap f fun i ↦ realize v (![t] i)) = funMap f ![realize v t]

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ (funMap f fun i ↦ realize v (![t] i)) = funMap f ![realize v t]
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case mem
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
y : F
⊢ Group.IsSolvable (X - C y).Gal

Tactic:
]

Goal state after:
case mem
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
y : F
⊢ Group.IsSolvable (X - C y).Gal
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
⊢ (funMap f fun i ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ (funMap f fun i ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ (castLE ⋯ (mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ)).all =
    (mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ).all

Tactic:
]

Goal state after:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α (k + 1)
⊢ (castLE ⋯ (mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ)).all =
    (mapTermRel (fun x t ↦ Term.relabel (relabelAux g x) t) (fun x ↦ id) (fun x ↦ castLE ⋯) φ).all
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 (minpoly F x).Gal

Tactic:
]

Goal state after:
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 (minpoly F x).Gal
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ equal t₁✝ t₂✝ = equal t₁✝ t₂✝

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ((LHom.id L).onRelation R✝).boundedFormula (id ∘ ts✝) = id (rel R✝ ts✝)

Tactic:
]

Goal state after:
case rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ((LHom.id L).onRelation R✝).boundedFormula (id ∘ ts✝) = id (rel R✝ ts✝)
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
a : FieldAxiom
⊢ toProp K a

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
a : FieldAxiom
⊢ toProp K a
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (LHom.id L).onBoundedFormula f₁✝ = id f₁✝
ih2 : (LHom.id L).onBoundedFormula f₂✝ = id f₂✝
⊢ f₁✝.imp f₂✝ = f₁✝.imp f₂✝

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (LHom.id L).onBoundedFormula f✝ = id f✝
⊢ f✝.all = f✝.all

Tactic:
]

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 x⟧ = ⟦funMap f x⟧

Tactic:
]

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 x ↔ RelMap r x

Tactic:
]

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'
⊢ id = id

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
α : Type u'
s : Set α
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
      ((⋃ i,
          ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)) ∩
        (diagonal α)ᶜ)

Tactic:
]

Goal state after:
L : Language
α : Type u'
s : Set α
⊢ (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab ↦ ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
      ((⋃ i,
          ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)) ∩
        (diagonal α)ᶜ)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ (funMap val✝ fun i ↦ realize v (ts i)) = funMap val✝ fun i ↦ realize v (ts i)

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.succ.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions (n✝ + 1)
⊢ (funMap val✝ fun i ↦ realize v (ts i)) = funMap val✝ fun i ↦ realize v (ts i)

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term (α ⊕ β)
ih : ∀ (a : Fin l✝), realize v (ts a).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a)
⊢ (funMap f fun i ↦ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts i)) =
    funMap f fun i ↦ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts i)

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
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
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = funMap _f✝ (⇑g ∘ fun i ↦ Term.realize v (_ts✝ i))

Tactic:
]

Goal state after:
case func
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
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = funMap _f✝ (⇑g ∘ fun i ↦ Term.realize v (_ts✝ i))
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:
]

Goal state after:
α : 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
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)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t] i)) = RelMap R ![realize (Sum.elim v xs) t]

Tactic:
]

Goal state after:
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)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t] i)) = RelMap R ![realize (Sum.elim v xs) t]
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_1
α : 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
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ x i a
a : α
ha1 : RelMap r fun i ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x_1 ↦ x x_1 a

Tactic:
]

Goal state after:
case refine_1
α : 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
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ x i a
a : α
ha1 : RelMap r fun i ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x_1 ↦ x x_1 a
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_1
α : 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
hx : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ x i a
a : α
ha1 : RelMap r fun i ↦ x i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x_1 ↦ x x_1 a

Tactic:
exact ha1

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)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
]

Goal state after:
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)
⊢ (RelMap R fun i ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_2
α : 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
hy : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ y i a
a : α
ha1 : RelMap r fun i ↦ y i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x ↦ y x a

Tactic:
]

Goal state after:
case refine_2
α : 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
hy : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ y i a
a : α
ha1 : RelMap r fun i ↦ y i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x ↦ y x a
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case refine_2
α : 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
hy : ∀ᶠ (a : α) in ↑u, RelMap r fun i ↦ y i a
a : α
ha1 : RelMap r fun i ↦ y i a
ha2 : ∀ (i : Fin n), x i a = y i a
⊢ RelMap r fun x ↦ y x a

Tactic:
exact ha1

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case equal
α : 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✝ : ℕ
t₁✝ t₂✝ : 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
⊢ ((Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₁✝) =
      Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₂✝) ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝

Tactic:
]

Goal state after:
case equal
α : 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✝ : ℕ
t₁✝ t₂✝ : 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
⊢ ((Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₁✝) =
      Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₂✝) ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case rel
α : 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
⊢ (RelMap R✝ fun i ↦ Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)

Tactic:
]

Goal state after:
case rel
α : 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
⊢ (RelMap R✝ fun i ↦ Term.realize (Quotient.mk' ∘ Sum.elim x v) (ts✝ i)) ↔
    ∀ᶠ (a : α) in ↑u, RelMap R✝ fun i ↦ Term.realize (fun i ↦ Sum.elim x v i a) (ts✝ i)
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
⊢ (∃ x, ¬(∼θ).Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬(∼θ).Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case imp
α : 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✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula β n✝
ih :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₁✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a
ih' :
  ∀ (v : Fin n✝ → (a : α) → M a),
    (f₂✝.Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a
v : Fin n✝ → (a : α) → M a
⊢ ((∀ᶠ (a : α) in ↑u, f₁✝.Realize (fun i ↦ x i a) fun i ↦ v i a) →
      ∀ᶠ (a : α) in ↑u, f₂✝.Realize (fun i ↦ x i a) fun i ↦ v i a) ↔
    (∀ᶠ (x_1 : α) in ↑u, f₁✝.Realize (fun i ↦ x i x_1) fun i ↦ v i x_1) →
      ∀ᶠ (x_1 : α) in ↑u, f₂✝.Realize (fun i ↦ x i x_1) fun i ↦ v i x_1

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all.h₂.refine_2
α : 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
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : {x_1 | ∀ (x_2 : M x_1), φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) x_2)} ∈ ↑u
m : (a : α) → M a
⊢ {x_1 | φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) (m x_1))} ∈ ↑u

Tactic:
]

Goal state after:
case all.h₂.refine_2
α : 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
h' : ∀ (m : (a : α) → M a) (a : α), (fun i ↦ Fin.snoc v m i a) = Fin.snoc (fun i ↦ v i a) (m a)
h : {x_1 | ∀ (x_2 : M x_1), φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) x_2)} ∈ ↑u
m : (a : α) → M a
⊢ {x_1 | φ.Realize (fun i ↦ x i x_1) (Fin.snoc (fun i ↦ v i x_1) (m x_1))} ∈ ↑u
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case var
L : Language
α : Type u'
l✝ : List (L.Term α)
a✝ : α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ var a✝ :: listDecode l = var a✝ :: listDecode l

Tactic:
]

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
⊢ Formula.Realize φ default = Formula.Realize φ fun i ↦ Quotient.mk' fun a ↦ default 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)
φ : L.Sentence
⊢ Formula.Realize φ default = Formula.Realize φ fun i ↦ Quotient.mk' fun a ↦ default i
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func
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)
⊢ (if h : n ≤ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun i ↦ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))[i]) ::
        drop n (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l

Tactic:
]

Goal state after:
case func
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)
⊢ (if h : n ≤ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun i ↦ (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))[i]) ::
        drop n (listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l
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
⊢ (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')

Tactic:
]

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.Encoding

Goal state before:
pp: case cons
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)
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun i ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ ts i :: (List.map ts l' ++ listDecode l) = ts i :: (List.map ts l' ++ listDecode l)

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
]

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs