mathlib-initiative/mathlib-tactics huggingface dataset:
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)
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 : α
⊢ Fin.snoc v m (Fin.last k) a = Fin.snoc (fun i ↦ v i a) (m a) (Fin.last k)

pp: case 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
m : (a : α) → M a
a : α
i : Fin k
x✝ : Fin.snoc v m i.succ a = Fin.snoc (fun i ↦ v i a) (m a) i.succ
⊢ Fin.snoc v m i.castSucc a = Fin.snoc (fun i ↦ v i a) (m a) i.castSucc

Tactic:
·

Goal state after:
case refine_1
α : 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 : α
⊢ Fin.snoc v m (Fin.last k) a = Fin.snoc (fun i ↦ v i a) (m a) (Fin.last k)
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)
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 : α
i : Fin k
x✝ : Fin.snoc v m i.succ a = Fin.snoc (fun i ↦ v i a) (m a) i.succ
⊢ Fin.snoc v m i.castSucc a = Fin.snoc (fun i ↦ v i a) (m a) i.castSucc

Tactic:
·

Goal state after:
case 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
m : (a : α) → M a
a : α
i : Fin k
x✝ : Fin.snoc v m i.succ a = Fin.snoc (fun i ↦ v i a) (m a) i.succ
⊢ Fin.snoc v m i.castSucc a = Fin.snoc (fun i ↦ v i a) (m a) i.castSucc
Module: Mathlib.ModelTheory.Ultraproducts

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

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 : ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) (m a))

Tactic:
·

Goal state after:
case all.h₂.refine_1
α : 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 : ∀ (m : (a : α) → M a), ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) (m a))
⊢ ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
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 : ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) (m a))

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 : ∀ᶠ (a : α) in ↑u, ∀ (x_1 : M a), φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) x_1)
m : (a : α) → M a
⊢ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i ↦ x i a) (Fin.snoc (fun i ↦ v i a) (m a))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func.refine_1
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)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
i : Fin n
⊢ (List.map ts (finRange n) ++ listDecode l)[↑i] = ts i

pp: case func.refine_2
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)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Tactic:
·

Goal state after:
case func.refine_1
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)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
i : Fin n
⊢ (List.map ts (finRange n) ++ listDecode l)[↑i] = ts i
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.refine_1
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
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') (last k) =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x (last k)

pp: case all.refine_2
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
i : Fin k
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') i.castSucc =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x i.castSucc

Tactic:
·

Goal state after:
case all.refine_1
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
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') (last k) =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x (last k)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case func.refine_2
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)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Tactic:
·

Goal state after:
case func.refine_2
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)
h : listDecode (flatMap (fun i ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ #((n : ℕ) × L.Term (α ⊕ Fin n)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

pp: case refine_2
L : Language
α : Type u'
⊢ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
·

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ #((n : ℕ) × L.Term (α ⊕ Fin n)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.refine_2
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
i : Fin k
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') i.castSucc =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x i.castSucc

Tactic:
·

Goal state after:
case all.refine_2
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
i : Fin k
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') i.castSucc =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x i.castSucc
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ∀ (i : ℕ), #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

pp: case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Tactic:
·

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ∀ (i : ℕ), #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ (liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ castSucc)

Tactic:
rw [realize_liftAt_one (refl n), iff_eq_eq]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
⊢ φ.Realize v (xs ∘ fun i ↦ if ↑i < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v.inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
val✝ : α
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val✝)) =
    Sum.elim (fun a ↦ realize v (tf a)) x (Sum.inl val✝)

pp: case e_v.inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
val✝ : Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val✝)) =
    Sum.elim (fun a ↦ realize v (tf a)) x (Sum.inr val✝)

Tactic:
·

Goal state after:
case e_v.inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
val✝ : α
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inl val✝)) =
    Sum.elim (fun a ↦ realize v (tf a)) x (Sum.inl val✝)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e_v.inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
val✝ : Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val✝)) =
    Sum.elim (fun a ↦ realize v (tf a)) x (Sum.inr val✝)

Tactic:
·

Goal state after:
case e_v.inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
n✝ : ℕ
φ : L.BoundedFormula α n✝
tf : α → L.Term β
v : β → M
xs : Fin n✝ → M
n : ℕ
t : L.Term (α ⊕ Fin n)
x : Fin n → M
val✝ : Fin n
⊢ realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) (Sum.inr val✝)) =
    Sum.elim (fun a ↦ realize v (tf a)) x (Sum.inr val✝)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Tactic:
·

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2
L : Language
α : Type u'
⊢ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
·

Goal state after:
case refine_2
L : Language
α : Type u'
⊢ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_1
L : Language
α : Type u'
i j : ℕ
ij : (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) i = (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) j
⊢ i = j

pp: case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
·

Goal state after:
case refine_2.refine_1
L : Language
α : Type u'
i j : ℕ
ij : (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) i = (fun i ↦ ⟨i + 1, var (Sum.inr (last i))⟩) j
⊢ i = j
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
·

Goal state after:
case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inl a = Sum.inl b

pp: case refine_2.refine_2.inl.inr
L : Language
α : Type u'
a : α
b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inl a = Sum.inr b

pp: case refine_2.refine_2.inr.inl
L : Language
α : Type u'
a : (i : ℕ) × L.Functions i
b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inr a = Sum.inl b

pp: case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b

Tactic:
·

Goal state after:
case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inl a = Sum.inl b
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inl.inr
L : Language
α : Type u'
a : α
b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inl a = Sum.inr b

pp: case refine_2.refine_2.inr.inl
L : Language
α : Type u'
a : (i : ℕ) × L.Functions i
b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inr a = Sum.inl b

pp: case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b

Tactic:
·

Goal state after:
case refine_2.refine_2.inl.inr
L : Language
α : Type u'
a : α
b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inl a = Sum.inr b
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inr.inl
L : Language
α : Type u'
a : (i : ℕ) × L.Functions i
b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inr a = Sum.inl b

pp: case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b

Tactic:
·

Goal state after:
case refine_2.refine_2.inr.inl
L : Language
α : Type u'
a : (i : ℕ) × L.Functions i
b : α
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inr a = Sum.inl b
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b

Tactic:
·

Goal state after:
case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i ↦ ⟨0, var (Sum.inl i)⟩) (fun F ↦ ⟨1, func F.snd fun x ↦ var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_1
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
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ φ.Realize ((constantMap ∘ Sum.inr) ∘ x) ↔
    N ⊨ (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls

pp: case refine_2
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
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ M ⊨ (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls ↔ φ.Realize x

Tactic:
·

Goal state after:
case refine_1
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
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ φ.Realize ((constantMap ∘ Sum.inr) ∘ x) ↔
    N ⊨ (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls