mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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
⊢ (fun p i ↦ coeff (↑i.snd) (↑p i.fst))
      ((fun p ↦
          ⟨fun i ↦
            AddMonoidAlgebra.ofCoeff
              { support := {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0},
                toFun := fun m ↦ if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0, mem_support_toFun := ⋯ },
            ⋯⟩)
        p) =
    p

Tactic:
by

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
f : (α → M) → M
g : α → (β → M) → M
hf : A.TermDefinable L f
hg : ∀ (i : α), A.TermDefinable L (g i)
⊢ A.TermDefinable L fun b ↦ f fun x ↦ g x b

Tactic:
by

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
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
⊢ Small.{w, w'} ↥S

Tactic:
by

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
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Tactic:
by

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 (κ →₀ ℕ)
f : (i : ι) × ↥(monoms i) ⊕ κ → R
i : ι
⊢ (lift f) (genericPolyMap monoms i) =
    (eval (f ∘ Sum.inr)) (↑((mvPolynomialSupportLEEquiv monoms).symm (f ∘ Sum.inl)) i)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{w, max (max w' u) v} L[[M]].card ≤ lift.{max (max w' u) v, w} κ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ #↑N0 ≤ lift.{w, max (max (max u v) w) w'} #↑N0

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{w, w'} #M ≤ lift.{w', w} κ
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Definability

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i).support ⊕ ι) := genericPolyMap fun p ↦ (↑p).support
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
i : ↥S
p : (i : ↥S) × ↥(↑i).support
⊢ coeff ↑p.snd ↑p.fst ∈ ⋃ p ∈ S, (fun m ↦ coeff m p) '' ↑p.support

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, #↑N = κ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Definability

Goal state before:
pp: ι : Type u_1
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
S : Finset (MvPolynomial ι K)
⊢ (⋃ p ∈ S, (fun m ↦ coeff m p) '' ↑p.support).Definable ring (zeroLocus K (Ideal.span ↑S))

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ¬(T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
⊢ κ.Categorical (Theory.ACF p)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsComplete

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L.Formula α
⊢ T ⊨ᵇ φ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
⊢ φ.Realize v

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
T' : L.Theory
h : ∀ φ ∈ T', T ⊨ᵇ φ
φ : L.Formula α
hφ : T' ⊨ᵇ φ
M : T.ModelType
⊢ ∀ (v : α → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
by

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 ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset L.Sentence
hT0 : ↑T0 ⊆ T
⊢ ↑(T0 ∪ {Formula.not φ}) ⊆ T ∪ {Formula.not φ}

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h✝ : ↑T0 ⊨ᵇ φ
ψ : Language.ring.Sentence
h : ψ ∈ Theory.field ∪ genericMonicPolyHasRoot '' {n | 0 < n}
q : Nat.Primes
a✝ : q ∉ ∅
⊢ ψ ∈ Theory.ACF ↑q

Tactic:
by

Goal state after:
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
V : Set (σ → K)
p q : MvPolynomial σ k
hp : p ∈ {p | ∀ x ∈ V, (aeval x) p = 0}
hq : q ∈ {p | ∀ x ∈ V, (aeval x) p = 0}
x : σ → K
hx : x ∈ V
⊢ (aeval x) (p + q) = 0

Tactic:
by

Goal state after:
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
V : Set (σ → K)
p q : MvPolynomial σ k
hq : q ∈ {p | ∀ x ∈ V, (aeval x) p = 0}
x : σ → K
hx : x ∈ V
⊢ (aeval x) (p • q) = 0

Tactic:
by

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.erase (Formula.not φ)) ⊆ T

Tactic:
by

Goal state after:
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
⊢ (vanishingIdeal k {x}).IsPrime

Tactic:
by

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

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
q : ℕ
property✝ : Nat.Prime q
hq : ⟨q, property✝⟩ ∉ {⟨p, hp⟩}
K : Type
struc✝ : Language.ring.Structure K
is_model✝ : K ⊨ Theory.ACF ↑⟨q, property✝⟩
nonempty'✝ : Nonempty K
v✝ : Empty → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
xs✝ : Fin 0 → ↑{ Carrier := K, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
⊢ q ≠ p

Tactic:
by

Goal state after:
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
⊢ (vanishingIdeal K {x}).IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ

Tactic:
by

Goal state after:
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
I : Ideal (MvPolynomial σ k)
⊢ I.radical ≤ vanishingIdeal k (zeroLocus K I)

Tactic:
by

Goal state after:
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
V : Set (σ → K)
x✝ : MvPolynomial σ k
hp : x✝ ∈ PrimeSpectrum.vanishingIdeal (pointToPoint '' V)
x : σ → K
hx : x ∈ V
⊢ (vanishingIdeal k {x}).IsPrime

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ ↔ T ⊨ᵇ φ

Tactic:
by

Goal state after:
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
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
⊢ Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
⊢ (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
by

Goal state after:
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
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this✝ : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
this : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K := fun s ↦ φ ((Ideal.Quotient.mk I) (X s))
⊢ aeval x = φ.comp (Quotient.mkₐ k I)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ {φ | T ⊨ᵇ φ} = L.completeTheory M

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ ↦ ↑(f ↑φ ⋯)
⊢ ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ

Tactic:
by

Goal state after:
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
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
⊢ ∃ x, I = vanishingIdeal k {x}

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mpr
L : Language
T : L.Theory
⊢ (T.IsSatisfiable ∧ ∀ (M N : T.ModelType), ↑M ≅[L] ↑N) → T.IsComplete

Tactic:
rintro ⟨hsat, h⟩
    refine ⟨hsat, ?_⟩
    intro φ
    obtain ⟨M⟩ := hsat
    by_cases hφ : M ⊨ φ
    · left
      exact models_sentence_iff.2 fun N => (elementarilyEquivalent_iff.1 (h M N) φ).1 hφ
    · right
      exact models_sentence_iff.2 fun N => (Sentence.realize_not N).2
        (mt (elementarilyEquivalent_iff.1 (h M N) φ).2 hφ)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
⊢ T.IsComplete ↔ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), ↑M ≅[L] ↑N

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
N : Type u_2
inst✝⁵ : L.Structure M
inst✝⁴ : L.Structure N
inst✝³ : M ⊨ T
inst✝² : N ⊨ T
inst✝¹ : Nonempty M
inst✝ : Nonempty N
⊢ M ≅[L] N

Tactic:
by

Goal state after:
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
inst✝¹ : IsAlgClosed K
inst✝ : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal k (zeroLocus K I) = I.radical

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
h : Theory.ACF 0 ⊨ᵇ φ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ φ ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
⊢ Theory.ACF 0 ⊨ᵇ φ ↔ {p | Theory.ACF ↑p ⊨ᵇ φ}.Infinite

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ φ ∈ L.completeTheory M ∨ Formula.not φ ∈ L.completeTheory M

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
κ : Cardinal.{w}
T : L.Theory
h : κ.Categorical T
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
hS : T.IsSatisfiable
hT : ∀ (M : T.ModelType), Infinite ↑M
φ : L.Sentence
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #↑M = κ
hN : #↑N = κ
⊢ Nonempty (↑M ≃[Language.empty] ↑N)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: ⊢ Language.empty.infiniteTheory.ModelType

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: R : Type u
X : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
⊢ Module.rank R ↥(adjoin R s) ≤ max #↑s ℵ₀

Tactic:
by

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
inst✝ : Finite ↥S
⊢ Surjective fun x ↦ x /ₒ 1

Tactic:
by

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
inst✝ : Finite X
⊢ Surjective fun x ↦ x /ₒ 1

Tactic:
by

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
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
⊢ #(OreLocalization S R) ≤ #R

Tactic:
by

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
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ x /ₒ s = x /ₒ s'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
this✝ : IsNoetherian K ↥(Algebra.adjoin K ↑s)
this : Finite ↥(Algebra.adjoin K ↑s)
S' : Set (ι → ↥(Algebra.adjoin K ↑s)) := (fun v ↦ Subtype.val ∘ v) ⁻¹' S
res : ↑S' → ↑S' := fun x ↦ ⟨fun i ↦ ⟨(eval fun j ↦ ↑(↑x j)) (ps i), ⋯⟩, ⋯⟩
⊢ Function.Surjective res

Tactic:
by

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

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
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
⊢ Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
by

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'
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
L : Type u
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
⊢ #L ≤ #R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
hS : S ≤ R⁰
⊢ #(Localization S) = #R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
L : Type v
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
⊢ Cardinal.lift.{u, v} #L = Cardinal.lift.{v, u} #R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Cardinality

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
L : Type u
inst✝² : CommRing L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
hS : S ≤ R⁰
⊢ #L = #R

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ a = 1 → IsUnit a

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ IsUnit a ↔ a = 1

Tactic:
by

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

Goal state before:
pp: a b : Cardinal.{u_1}
hb : b ≠ 0
hdiv : a ∣ b
⊢ a ≤ b

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ Prime a

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬Irreducible a

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ ↑n ∣ ↑m ↔ n ∣ m

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (Field α) ↔ IsPrimePow ‖α‖

Tactic:
by

Goal state after: