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

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case refine_2
p : ℕ
κ : Cardinal.{u_2}
hκ : ℵ₀ < κ
M : Type u_2
struc✝¹ : Language.ring.Structure M
is_model✝¹ : M ⊨ Theory.ACF p
nonempty'✝¹ : Nonempty M
N : Type u_2
struc✝ : Language.ring.Structure N
is_model✝ : N ⊨ Theory.ACF p
nonempty'✝ : Nonempty N
hM : #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ } = κ
hN : #↑{ Carrier := N, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ } = κ
x✝³ : Field M := fieldOfModelACF p M
this✝⁴ : M ⊨ Theory.field
x✝² : CompatibleRing M := compatibleRingOfModelField M
this✝³ : IsAlgClosed M
this✝² : CharP M p
x✝¹ : Field N := fieldOfModelACF p N
this✝¹ : N ⊨ Theory.field
x✝ : CompatibleRing N := compatibleRingOfModelField N
this✝ : IsAlgClosed N
this : CharP N p
⊢ κ = κ

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ

Tactic:
]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬(T ∪ {Formula.not φ}).IsSatisfiable
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
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 ⊨ φ ∧ M ⊨ T

Tactic:
]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
⊢ φ.Realize fun a ↦ ↑(L.con a)

Tactic:
]

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
⊢ φ.Realize fun a ↦ ↑(L.con a)
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

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

Tactic:
]

Goal state after:
φ : Language.ring.Sentence
h : ∃ T0, ↑T0 ⊆ Theory.ACF 0 ∧ ↑T0 ⊨ᵇ φ
⊢ {p | ¬Theory.ACF ↑p ⊨ᵇ φ}.Finite
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
]

Goal state after:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
⊢ φ.Realize v
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} ∨ ∃ x ∈ {q | Nat.Prime q}, ∼(eqZero x) = ψ
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }

Tactic:
]

Goal state after:
φ : 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} ∨ ∃ x ∈ {q | Nat.Prime q}, ∼(eqZero x) = ψ
⊢ { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
⊢ (¬∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable

Tactic:
]

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (¬∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∃ T0, ↑T0 ⊆ T ∧ ¬(↑T0 ∪ {Formula.not φ}).IsSatisfiable
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.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∪
      if ↑q = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime ↑q then {eqZero ↑q} else {⊥}

Tactic:
]

Goal state after:
φ : 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.field ∪ genericMonicPolyHasRoot '' {n | 0 < n} ∪
      if ↑q = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime ↑q then {eqZero ↑q} else {⊥}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ

Tactic:
]

Goal state after:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ
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)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → K
hx : x ∈ zeroLocus K I
⊢ p ∈ vanishingIdeal k {x}

Tactic:
]

Goal state after:
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)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → K
hx : x ∈ zeroLocus K I
⊢ p ∈ vanishingIdeal k {x}
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
hφ : ∀ (M : T.ModelType), ↑M ⊨ φ
⊢ False

Tactic:
]

Goal state after:
case inr
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφn : ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
hφ : ∀ (M : T.ModelType), ↑M ⊨ φ
⊢ False
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)
p : MvPolynomial σ k
hp : p ∈ sInf {J | I ≤ J ∧ J.IsPrime}
x : σ → K
hx : x ∈ zeroLocus K I
⊢ p ∈ vanishingIdeal k {x}

Tactic:
]

Goal state after:
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)
p : MvPolynomial σ k
hp : p ∈ sInf {J | I ≤ J ∧ J.IsPrime}
x : σ → K
hx : x ∈ zeroLocus K I
⊢ p ∈ vanishingIdeal k {x}
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
⊢ (algebraMap k (MvPolynomial σ k ⧸ I)).IsIntegral

Tactic:
]

Goal state after:
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
⊢ (algebraMap k (MvPolynomial σ k ⧸ I)).IsIntegral
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case inr
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
p : ℕ
hp : p ∈ {q | Nat.Prime q}
⊢ Nonempty { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ∼(eqZero p) }

Tactic:
· refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
      rintro ⟨q, _⟩ hq ⟨K⟩ _ _
      have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
      let _ := fieldOfModelACF q K
      have := modelField_of_modelACF q K
      let _ := compatibleRingOfModelField K
      have := charP_of_model_fieldOfChar q K
      simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
      intro _
      exact hqp <| CharP.eq K this inferInstance

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inr
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : ¬M ⊨ φ
⊢ T ⊨ᵇ φ

Tactic:
]

Goal state after:
case inr
L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
φ : L.BoundedFormula Empty 0
h_realize : M ⊨ φ
hT : T ⊨ᵇ Formula.not φ
this : ¬M ⊨ φ
⊢ T ⊨ᵇ φ
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.jacobson

Tactic:
]

Goal state after:
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.jacobson
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
hcomp : T.IsComplete
M N : T.ModelType
⊢ ↑M ≅[L] ↑N

Tactic:
ElementarilyEquivalent,

Goal state after:
case mp
L : Language
T : L.Theory
hcomp : T.IsComplete
M N : T.ModelType
⊢ L.completeTheory ↑M = L.completeTheory ↑N
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
hcomp : T.IsComplete
M N : T.ModelType
⊢ {φ | T ⊨ᵇ φ} = {φ | T ⊨ᵇ φ}

Tactic:
]

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:
ElementarilyEquivalent,

Goal state after:
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
⊢ L.completeTheory M = L.completeTheory N
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 J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal k {x}
y : σ → K
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ J

Tactic:
]

Goal state after:
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 J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal k {x}
y : σ → K
hy : y ∈ {x}
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ J
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
⊢ {φ | T ⊨ᵇ φ} = {φ | T ⊨ᵇ φ}

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬T.IsSatisfiable
con : Formula.not φ ∈ T
⊢ False

Tactic:
]

Goal state after:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬T.IsSatisfiable
con : Formula.not φ ∈ T
⊢ False
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
w✝ : T.ModelType
h✝ : #↑w✝ = κ
⊢ (∀ (M : T.ModelType), ↑M ⊨ φ) ∨ ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ

Tactic:
]

Goal state after:
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
w✝ : T.ModelType
h✝ : #↑w✝ = κ
⊢ (∀ (M : T.ModelType), ↑M ⊨ φ) ∨ ∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
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
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
⊢ False

Tactic:
]

Goal state after:
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
w✝ : T.ModelType
h✝ : #↑w✝ = κ
MF : T.ModelType
hMF : ¬↑MF ⊨ φ
MT : T.ModelType
hMT : ↑MT ⊨ φ
⊢ False
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #↑M = κ
hN : #↑N = κ
⊢ lift.{w, w} κ = lift.{w, w} κ

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeAlgebra

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

Tactic:
]

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 ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ 1 ≤ max #↑s ℵ₀

Tactic:
]

Goal state after:
case inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Subsingleton R
⊢ 1 ≤ max #↑s ℵ₀
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{max u v, v} (Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range) ≤ lift.{max u v, v} (max #↑s ℵ₀)

Tactic:
]

Goal state after:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ lift.{max u v, v} (Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range) ≤ lift.{max u v, v} (max #↑s ℵ₀)
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ max ℵ₀ #↑s

Tactic:
]

Goal state after:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ max ℵ₀ #↑s
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1

Tactic:
]

Goal state after:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ s ^ j • x = s ^ j • x

Tactic:
]

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

Goal state before:
pp: case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1

Tactic:
]

Goal state after:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = s ^ j • x

Tactic:
]

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

Goal state before:
pp: case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
]

Goal state after:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
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.Injective res

Tactic:
]

Goal state after:
ι : 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.Injective res
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inr.inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Finite ↥S
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
]

Goal state after:
case inr.inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Finite ↥S
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
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
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ lift.{v, u} #↥S * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
]

Goal state after:
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 * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inl
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✝ : Finite X
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
]

Goal state after:
case inl
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✝ : Finite X
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
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'
⊢ ∃ u v, u • x = v • x ∧ ↑u * ↑s' = v * ↑s

Tactic:
]

Goal state after:
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'
⊢ ∃ u v, u • x = v • x ∧ ↑u * ↑s' = v * ↑s
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
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
]

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