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

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
k : ℕ
R : L.Relations k
ts : Fin k → L.Term α
⊢ (RelMap R fun i ↦ Term.realize (Sum.elim v default) (Term.relabel Sum.inl (ts i))) ↔
    RelMap R fun i ↦ Term.realize v (ts i)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
⊢ BoundedFormula.Realize φ x y ↔ φ.Realize x

Tactic:
rw [Formula.Realize, iff_iff_eq]
  congr
  ext i; exact Fin.elim0 i

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L.Formula α
x✝ : α → M
⊢ x✝ ∈ Set.ofPred (φ.onFormula ψ).Realize ↔ x✝ ∈ Set.ofPred ψ.Realize

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__v.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
val✝ : α
⊢ ((fun a ↦ ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) (Sum.inl val✝) =
    Sum.elim (fun a ↦ ↑(L.con a)) default (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
P : Type u_2
inst✝ : L.Structure P
S : L.Substructure P
⊢ ∀ (x : P), x ∈ comap (Hom.id L P) S ↔ x ∈ S

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ M ⊨ {φ} ↔ M ⊨ φ

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
s : Set M
m : ↥⊤
⊢ (fun m ↦ ⟨m, ⋯⟩) (⊤.subtype m) = m

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
n : ℕ
φ : L.BoundedFormula α n
v : α → ↥⊤
xs : Fin n → ↥⊤
⊢ φ.Realize (⇑topEquiv ∘ v) (⇑topEquiv ∘ xs) ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
⊢ φ.Realize (⇑topEquiv ∘ v) ↔ φ.Realize (Subtype.val ∘ v)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) ↔ x✝ ∈ S

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ Substructure.map f ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
⊢ funMap fn x ∈ {x | f x = g x}

Tactic:
have h : f ∘ x = g ∘ x := by
      ext
      repeat' rw [Function.comp_apply]
      apply hx
    simp [h]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f✝ : M ↪[L] N
s : L.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → ↥s
⊢ (codRestrict (Substructure.map f✝.toHom s) (f✝.domRestrict s) ⋯) (funMap f x) =
    funMap f (⇑(codRestrict (Substructure.map f✝.toHom s) (f✝.domRestrict s) ⋯) ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f : M ↪[L] N
s : L.Substructure M
n : ℕ
R : L.Relations n
x : Fin n → ↥s
⊢ RelMap R (⇑(codRestrict (Substructure.map f.toHom s) (f.domRestrict s) ⋯) ∘ x) ↔ RelMap R x

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f✝ : M ↪[L] N
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ (codRestrict f✝.toHom.range f✝ ⋯) (funMap f x) = funMap f (⇑(codRestrict f✝.toHom.range f✝ ⋯) ∘ x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f : M ↪[L] N
n : ℕ
R : L.Relations n
x : Fin n → M
⊢ RelMap R (⇑(codRestrict f.toHom.range f ⋯) ∘ x) ↔ RelMap R x

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ φ, s = ofPred φ.Realize) ↔ ∃ b, s = ofPred ((LEquiv.addEmptyConstants L ↑∅).onFormula.symm b).Realize

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ ofPred ⊥.Realize

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ univ ↔ x✝ ∈ ofPred ⊤.Realize

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
x✝ : α → M
⊢ x✝ ∈ ofPred φ.Realize ∩ ofPred θ.Realize ↔ x✝ ∈ ofPred (φ ⊓ θ).Realize

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
ι : Type u_2
inst✝ : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ ⋂ i, f i = Finset.univ.inf f

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝¹ : L.Structure M
α : Type u₁
ι : Type u_2
inst✝ : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ ⋃ i, f i = Finset.univ.sup f

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_8.last
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) (Fin.last n) =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      (Fin.last n)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_8.cast
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x : Fin n → ↥((closure L).toFun A)
a : M
hφ : φ.Realize default (Fin.snoc (Subtype.val ∘ x) a)
D : Set M := {y | φ.Realize default (Fin.snoc (Subtype.val ∘ x) y)}
hD_ne : D.Nonempty
v : Fin 1 → M
i✝ : Fin n
⊢ Fin.snoc (Subtype.val ∘ x) (v 0) i✝.castSucc =
    ((Sum.elim (fun a ↦ Term.realize v (Fin.lastCases (var 0) (fun j ↦ (L.con ⟨↑(x j), ⋯⟩).term) a)) default ∘
          Sum.inl ∘ Sum.elim Empty.elim id) ∘
        Sum.inr)
      i✝.castSucc

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.e__v.inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
val✝ : α
⊢ Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
      (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x)) (Sum.inl val✝)) =
    Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h₁
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 : α ≃ β
i : β → M
⊢ (fun g ↦ g ∘ ⇑f.symm) ((fun g ↦ g ∘ ⇑f) i) = i

Tactic:
ext b

Goal state after:
case h₁
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 : α ≃ β
i : β → M
b : β
⊢ (fun g ↦ g ∘ ⇑f.symm) ((fun g ↦ g ∘ ⇑f) i) b = i b
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h₂
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 : α ≃ β
i : α → M
a : α
⊢ (fun g ↦ g ∘ ⇑f) ((fun g ↦ g ∘ ⇑f.symm) i) a = i a

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ ∀ (a : ↥(BoundedFormula.freeVarFinset φ)),
    Sum.elim Subtype.val x✝
        (Sum.rec (motive := fun x ↦ x ∈ BoundedFormula.freeVarFinset φ → ↥A0 ⊕ α) (fun val hx ↦ Sum.inl ⟨↑val, ⋯⟩)
          (fun val x ↦ Sum.inr val) ↑a ⋯) =
      Sum.elim Subtype.val x✝ ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
D : Set M
x : M
hx : x ∈ D
φ : L[[↑↑S]].Formula (Fin 1)
hφ : {x | x 0 ∈ D} = ofPred φ.Realize
hφx : φ.Realize ![x]
ψ : L[[↑↑S]].Sentence := iExs (Fin 1) (relabel Sum.inr φ)
hψM : M ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ ↑(v' 0) ∈ ↑S

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.e__v.inr.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ ∀ (i : Fin n✝), v (Sum.inr i) = snoc (fun x ↦ v (Sum.inr x)) a i.castSucc

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
rw [mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0, max_le_iff]

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

Goal state before:
pp: case all.e__v.inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
x : Fin (n✝ + 1)
⊢ Sum.elim v (fun x ↦ snoc default a (castAdd 0 x))
      (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) (fun x ↦ Sum.map Sum.inr id (finSumFinEquiv.symm x)) (Sum.inr x)) =
    Sum.elim (fun x ↦ v (Sum.inl x)) (snoc (fun x ↦ v (Sum.inr x)) a) (Sum.inr x)

Tactic:
· refine Fin.lastCases ?_ ?_ x
        · simp [Fin.snoc]
        · simp only [castSucc, Sum.elim_inr,
            finSumFinEquiv_symm_apply_castAdd, Sum.map_inl, Sum.elim_inl]
          rw [← castSucc]
          simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro
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 β
val✝ : Fintype β
x : α → M
y : β → M
x✝ : y ∈ s
a : α
⊢ (((y ∘ ⇑(Equiv.Set.sumCompl (range ⇑f))) ∘
          ⇑((Equiv.ofInjective ⇑f ⋯).sumCongr (Fintype.equivFin ↑(range ⇑f)ᶜ).symm)) ∘
        Sum.inl)
      a =
    (y ∘ ⇑f) a

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case h₁.e__v.inl
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val✝ : α
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inl val✝)) =
    Sum.elim v y (Sum.inl val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case h₁.e__v.inr
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
val✝ : γ
⊢ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr (Sum.inr val✝)) =
    Sum.elim v y (Sum.inr val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: 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)
a : α
⊢ ∀ (x : α → M),
    x ∈ {x | x a = x (rangeSplitting f (rangeFactorization f a))} ↔
      x ∈ ofPred ((var a).equal (var (rangeSplitting f (rangeFactorization f a)))).Realize

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: 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 : α), A.Definable L {x | x a = x (rangeSplitting f (rangeFactorization f a))}
⊢ ∀ (x : α → M),
    x ∈ ⋂ i ∈ Finset.univ, {x | x i = x (rangeSplitting f (rangeFactorization f i))} ↔
      x ∈ {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}

Tactic:
simp

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 φ
⊢ M ⊨ φ.exClosure

Tactic:
rw [Formula.realize_exClosure]

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
S : (L.sum L.skolem₁).Substructure M
⊢ (LHom.sumInl.substructureReduct S).IsElementary

Tactic:
apply (LHom.sumInl.substructureReduct S).isElementary_of_exists
  intro n φ x a h
  let φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
  use ⟨funMap φ' ((↑) ∘ x), ?_⟩
  · exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default
          (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩
  · exact S.fun_mem (LHom.sumInr.onFunction φ) ((↑) ∘ x) (by
      exact fun i => (x i).2)

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:
simp

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 ↔ Std.Refl fun x y ↦ RelMap r ![x, y]

Tactic:
rw [refl_def]

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

Goal state before:
pp: case h
M : Type w
A : Set M
L : Language
L' : Language
inst✝² : L.Structure M
inst✝¹ : L'.Structure M
α : Type u₁
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Term α
⊢ (fun v ↦ Term.realize v ψ) = fun v ↦ Term.realize v ((LHom.addConstants (↑A) φ).onTerm ψ)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ (∃ φ, f = fun v ↦ Term.realize v φ) ↔ ∃ b, f = fun v ↦ Term.realize v ((LEquiv.addEmptyConstants L ↑∅).onTerm.symm b)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.FreeCommRing

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
inst✝² : DecidableEq κ
inst✝¹ : CommRing R
inst✝ : DecidableEq R
monoms : ι → Finset (κ →₀ ℕ)
p : (i : ι) × ↥(monoms i) → R
i : ι
⊢ ∀ (a : κ →₀ ℕ),
    a ∈ {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0} ↔
      (if hm : a ∈ monoms i then p ⟨i, ⟨a, hm⟩⟩ else 0) ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case e'_2
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
h✝ : TermDefinable₁ L f
t : L[[↑A]].Formula (Option Unit)
h : (Function.tupleGraph fun v ↦ f (v ())) = ofPred t.Realize
v : Fin 2 → M
⊢ v ∈ ofPred (Formula.relabel (fun x ↦ x.elim 1 fun x ↦ 0) t).Realize ↔
    (v ∘ fun x ↦ x.elim 1 fun x ↦ 0) ∈ ofPred t.Realize

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ lift.{w, w'} #↑∅ ≤ lift.{w', w} κ

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
⊢ ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
T0

Goal state after:
case mp
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
⊢ ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
⊢ ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0

Tactic:
T0

Goal state after:
case mpr
L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
⊢ ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
x✝ : MvPolynomial σ k
⊢ x✝ ∈ vanishingIdeal k {x} ↔ x✝ ∈ RingHom.ker (aeval x)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
this : DecidableEq L.Sentence := Classical.decEq L.Sentence
h : ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → (↑T0 ∪ {Formula.not φ}).IsSatisfiable
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑T0 ⊆ ↑(T0.erase (Formula.not φ)) ∪ {Formula.not φ}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: case e'_3
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
e_2✝ : AddMonoidAlgebra.semiring = AddMonoidAlgebra.ring.toSemiring
x✝ : MvPolynomial σ K
⊢ x✝ ∈ vanishingIdeal K {x} ↔ x✝ ∈ RingHom.ker (aeval x)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
x : σ → K
z : K
⊢ (aeval x) (C z) = z

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: ⊢ lift.{0, 0} Language.empty.card ≤ lift.{0, 0} ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case refine_1
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ ℵ₀ ≤ lift.{v, u} #↥S

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case refine_2
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ ℵ₀ ≤ lift.{u, v} #X

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this✝ : Injective j
this : #(OreLocalization S X) ≤ lift.{u, v} #X * lift.{u, v} #X
⊢ ℵ₀ ≤ lift.{u, v} #X

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inl.inl
a : Cardinal.{u}
ha : ℵ₀ ≤ a
c : Cardinal.{u}
hbc : a ∣ 0 * c
hz : 0 * c = 0
⊢ a ∣ 0 ∨ a ∣ c

Tactic:
simp

Goal state after: