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

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

pp: case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x z : E
hx : x ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
p : F[X] := minpoly F x
a : E
hy : a ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮x, a⟯
q : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits

Tactic:
·

Goal state after:
case inl
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
q : F[X] := minpoly F y
a : E
hx : a ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮a, y⟯
p : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
Module: Mathlib.FieldTheory.AbelRuffini

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

Tactic:
·

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x z : E
hx : x ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
p : F[X] := minpoly F x
a : E
hy : a ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮x, a⟯
q : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
Module: Mathlib.ModelTheory.Syntax

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

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

Tactic:
·

Goal state after:
case inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
·

Goal state after:
case inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)
Module: Mathlib.ModelTheory.Syntax

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

Tactic:
·

Goal state after:
case inl
α : Type u'
n k : ℕ
val✝ : α
⊢ relabelAux Sum.inl k (Sum.inl val✝) = Sum.map id (natAdd n) (Sum.inl val✝)
Module: Mathlib.ModelTheory.Semantics

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

pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
α : Type u'
n k : ℕ
val✝ : Fin k
⊢ relabelAux Sum.inl k (Sum.inr val✝) = Sum.map id (natAdd n) (Sum.inr val✝)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ

Tactic:
·

Goal state after:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : p = 0
⊢ K ⊨ (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K p

pp: case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : Nat.Prime p
⊢ K ⊨ {eqZero p} ↔ CharP K p

pp: case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p

Tactic:
·

Goal state after:
case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : p = 0
⊢ K ⊨ (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K p
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : Nat.Prime p
⊢ K ⊨ {eqZero p} ↔ CharP K p

pp: case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p

Tactic:
·

Goal state after:
case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : Nat.Prime p
⊢ K ⊨ {eqZero p} ↔ CharP K p
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p

Tactic:
·

Goal state after:
case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
f : L[[α]].Functions 0
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)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

pp: case func.succ
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✝ : ℕ
f : L[[α]].Functions (n✝ + 1)
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)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
·

Goal state after:
case func.zero
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
f : L[[α]].Functions 0
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)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)
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
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

pp: case func.zero.inr
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✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)

Tactic:
·

Goal state after:
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
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_1
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨i, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

pp: case refine_2
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨j, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

pp: case refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s

Tactic:
·

Goal state after:
case refine_1
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨i, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_2
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨j, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

pp: case refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s

Tactic:
·

Goal state after:
case refine_2
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨j, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s

Tactic:
·

Goal state after:
case refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero.inr
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✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)

Tactic:
·

Goal state after:
case func.zero.inr
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✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.succ
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✝ : ℕ
f : L[[α]].Functions (n✝ + 1)
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)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
·

Goal state after:
case func.succ
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✝ : ℕ
f : L[[α]].Functions (n✝ + 1)
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)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)
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)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

pp: case func.succ.inr
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)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)

Tactic:
·

Goal state after:
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)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.succ.inr
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)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)

Tactic:
·

Goal state after:
case func.succ.inr
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)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case var
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
a✝ : α
⊢ Term.realize (⇑g ∘ v) (var a✝) = g (Term.realize v (var a✝))

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))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))

Tactic:
·

Goal state after:
case var
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
a✝ : α
⊢ Term.realize (⇑g ∘ v) (var a✝) = g (Term.realize v (var a✝))
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))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))

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))
⊢ Term.realize (⇑g ∘ v) (func _f✝ _ts✝) = g (Term.realize v (func _f✝ _ts✝))
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 : RelMap r x
⊢ RelMap r y

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 : RelMap r y
⊢ RelMap r x

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 : RelMap r x
⊢ RelMap r y
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 : RelMap r y
⊢ RelMap r x

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 : RelMap r y
⊢ RelMap r x
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_1
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)
⊢ realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0

pp: case refine_2
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)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ

Tactic:
·

Goal state after:
case refine_1
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)
⊢ realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_2
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)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ

Tactic:
·

Goal state after:
case refine_2
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)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case all.h₁
α : 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
⊢ (∀ (x_1 : Quotient ((↑u).productSetoid M)),
      φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (fun i ↦ Quotient.mk' (v i)) x_1)) ↔
    ∀ (m : (a : α) → M a), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))

pp: case all.h₂
α : 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), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))) ↔
    ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)

Tactic:
·

Goal state after:
case all.h₁
α : 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
⊢ (∀ (x_1 : Quotient ((↑u).productSetoid M)),
      φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (fun i ↦ Quotient.mk' (v i)) x_1)) ↔
    ∀ (m : (a : α) → M a), φ.Realize (fun i ↦ Quotient.mk' (x i)) (Fin.snoc (Quotient.mk' ∘ v) (Quotient.mk' m))