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

Goal state before:
pp: L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
    ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
]

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
    ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (max ℵ₀ (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
← add_eq_max le_rfl,

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
]

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              ((Formula.relabel (fun a ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ).imp
                (iInf fun g ↦ (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              ((Formula.relabel (fun a ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ).imp
                (iInf fun g ↦ (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃ x, φ.Realize (Sum.elim v x) ∧ ∀ (y : γ → M), φ.Realize (Sum.elim v y) → y = x
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
]

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

Goal state before:
pp: L : Language
⊢ (sum fun i ↦ #(L.BoundedFormula Empty (i + 1))) = sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

pp: L : Language
⊢ (sum fun i ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

pp: L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
]

Goal state after:
L : Language
⊢ (sum fun i ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))

L : Language
⊢ ℵ₀ ≤ sum fun i ↦ #(L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case H
L : Language
n : ℕ
⊢ Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))

Tactic:
]

Goal state after:
case H
L : Language
n : ℕ
⊢ Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))

Tactic:
]

Goal state after:
L : Language
⊢ ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card

Tactic:
]

Goal state after:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
]

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

Goal state before:
pp: L : Language
α : Type u'
⊢ max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u u') v, u} #((l : ℕ) × L.Functions l) +
          lift.{max u (max u u') v, v} #((l : ℕ) × L.Relations l)))

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols ∧ Countable (constantsOn α).Symbols

Tactic:
constructor <;> infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ max ℵ₀ L.card

Tactic:
rw [card_functions_sum_skolem₁]
  trans #(Σ n, L.BoundedFormula Empty n)
  · exact
      ⟨⟨Sigma.map Nat.succ fun _ => id,
          Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩
  · refine _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 ?_)
    simp only [mk_empty, lift_zero, lift_uzero, zero_add]
    rfl

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable α ∧ Countable L.Symbols

Tactic:
constructor <;> infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝³ : L.Structure M
α : Type u'
inst✝² : DecidableEq α
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
h : M ⊨ equivSentence φ
⊢ ∃ v, Realize (BoundedFormula.restrictFreeVar φ id) v

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝³ : L.Structure M
α : Type u'
inst✝² : DecidableEq α
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
h : M ⊨ equivSentence φ
⊢ ∃ v, Realize (BoundedFormula.restrictFreeVar φ id) v
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
⊢ Small.{max u v, w} ↥⊥

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
⊢ Small.{max u v, w} ↥⊥
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ f₁✝.Realize v xs → f₂✝.Realize v xs ↔ f₁✝.Realize v xs → f₂✝.Realize v xs

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a =
    (((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
        Sum.inl)
      (rangeFactorization f a)

Tactic:
]

Goal state after:
case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a =
    (((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
        Sum.inl)
      (rangeFactorization f a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) ↔ ∀ (x : M), f✝.Realize v (snoc xs x)

Tactic:
]

Goal state after:
case all
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) ↔ ∀ (x : M), f✝.Realize v (snoc xs x)
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ lift.{w, w'} κ
h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ lift.{w, w'} κ
h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = #↑s'

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = #↑s'
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
a : M
h' : f✝.Realize v (snoc xs a)
⊢ f✝.Realize v (snoc xs a)

Tactic:
]

Goal state after:
case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
a : M
h' : f✝.Realize v (snoc xs a)
⊢ f✝.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Skolem

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

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'
Module: Mathlib.ModelTheory.Skolem

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

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')) = #↑(⇑Equiv.ulift '' s')
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : M), f✝.Realize v (snoc xs x)
a : N
h' : f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) a)
⊢ f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) a)

Tactic:
]

Goal state after:
case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : M), f✝.Realize v (snoc xs x)
a : N
h' : f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) a)
⊢ f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) a)
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'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ φ.Realize v xs

Tactic:
induction φ with
  | falsum => rfl
  | equal =>
    simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term,
      EmbeddingLike.apply_eq_iff_eq g]
  | rel =>
    simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
    exact StrongHomClass.map_rel g _ _
  | imp _ _ ih1 ih2 => rw [BoundedFormula.Realize, ih1, ih2, BoundedFormula.Realize]
  | all _ ih3 =>
    rw [BoundedFormula.Realize, BoundedFormula.Realize]
    constructor
    · intro h a
      have h' := h (g a)
      rw [← Fin.comp_snoc, ih3] at h'
      exact h'
    · intro h a
      have h' := h (EquivLike.inv g a)
      rw [← ih3, Fin.comp_snoc, EquivLike.apply_inv_apply g] at h'
      exact h'

Goal state after:
Module: Mathlib.ModelTheory.Skolem

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

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

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ #↑s' ∧
    #↑(s ∪ ⇑Equiv.ulift '' s') ≤ #↑(⇑Equiv.ulift '' s') ∧
      lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')

L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s')
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✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
⊢ BoundedFormula.Realize φ (⇑g ∘ v) default = BoundedFormula.Realize φ (⇑g ∘ v) default

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr.refine_2
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
⊢ y (f a) = y (f a)

Tactic:
]

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
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Sentence
⊢ Formula.Realize φ default ↔ Formula.Realize φ default

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.irreflexive ↔ ∀ ⦃a : M⦄, ¬RelMap r ![a, a]

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.irreflexive ↔ ∀ ⦃a : M⦄, ¬RelMap r ![a, a]
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.symmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a]

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.symmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a]
Module: Mathlib.ModelTheory.Skolem

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

Tactic:
]

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

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.antisymmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a] → a = b

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.antisymmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a] → a = b
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]

Tactic:
]

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]