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

Goal state before:
pp: case nil
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode (flatMap (fun i ↦ (ts i).listEncode) [] ++ l) = List.map ts [] ++ listDecode l

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f : ↥falsum.freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥falsum.freeVarFinset), v (f a) = v' ↑a
⊢ (falsum.restrictFreeVar f).Realize v xs ↔ falsum.Realize v' xs

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_1.refl
L : Language
α : Type u'
i : ℕ
⊢ i = i

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_2
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : L.Structure M
inst✝⁶ : L.Structure N✝
inst✝⁵ : L.Structure P
inst✝⁴ : L.Structure Q
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ BoundedFormula.Realize φ (fun a ↦ Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) default ↔
    BoundedFormula.Realize φ x default

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case inl
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
i : α
⊢ (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) (Sum.inl i) = Sum.elim (v ∘ ⇑g) xs (Sum.inl i)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case inr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
g : α ≃ β
k : ℕ
φ : L.BoundedFormula α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : L.Term (α ⊕ Fin n)
xs : Fin n → M
i : Fin n
⊢ (Sum.elim v xs ∘ ⇑(g.sumCongr (_root_.Equiv.refl (Fin n)))) (Sum.inr i) = Sum.elim (v ∘ ⇑g) xs (Sum.inr i)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
xs : Fin n✝ → M
⊢ (φ.onBoundedFormula falsum).Realize v xs ↔ falsum.Realize v xs

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ Term.realize (Sum.elim v xs) t₁✝ = Term.realize (Sum.elim v xs) t₂✝ ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case rel
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (RelMap R✝ fun i ↦ Term.realize (Sum.elim v xs) (ts✝ i)) ↔ (rel R✝ ts✝).Realize v xs

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
⊢ ((equivSentence.symm (equivSentence φ)).Realize fun a ↦ ↑(L.con a)) ↔ φ.Realize fun a ↦ ↑(L.con a)

Tactic:
_root_.Equiv.symm_apply_apply

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
⊢ (φ.Realize fun a ↦ ↑(L.con a)) ↔ φ.Realize fun a ↦ ↑(L.con a)
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
p : L.Substructure N
f : M ↪[L] N
h : ∀ (c : M), f c ∈ p
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ RelMap r (⇑f.toHom ∘ x) ↔ RelMap r (⇑f ∘ x)

Tactic:
rfl

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
s : L.Substructure M
x✝ : ↥s
⊢ ((Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding) x✝ = (f.comp s.subtype) x✝

Tactic:
rfl

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✝ : M
⊢ (f.toHom.range.subtype.comp f.equivRange.toEmbedding) x✝ = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
v : α ⊕ Fin n✝ → M
⊢ falsum.toFormula.Realize v ↔ falsum.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
rfl

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₁
s : Set (α → M)
⊢ (∃ φ, s = ofPred φ.Realize) ↔ ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
Equiv.exists_congr_left (BoundedFormula.constantsVarsEquiv)

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ b, s = ofPred (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm b))) ↔
    ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case e_v.inl.inl
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : ↑A
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inl (Sum.inl val✝)) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inl (Sum.inl val✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case e_v.inl.inr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : α
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inl (Sum.inr val✝)) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inl (Sum.inr val✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case e_v.inr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
val✝ : Fin n✝
⊢ (Sum.elim (fun a ↦ ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) (Sum.inr val✝) =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ ↑((closure L).toFun A) ⊆ A

Tactic:
rw [coe_closure_eq_range_term_realize]

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
⊢ range (Term.realize Subtype.val) ⊆ A
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ v ∈ {a | ¬φ.Realize a} ↔ v ∈ ofPred φ.not.Realize

Tactic:
mem_ofPred,

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ ¬φ.Realize v ↔ v ∈ ofPred φ.not.Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ ¬φ.Realize v ↔ v ∈ ofPred φ.not.Realize

Tactic:
mem_ofPred,

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = ofPred φ.Realize
v : α → M
⊢ ¬φ.Realize v ↔ φ.not.Realize v
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: 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
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)

Tactic:
have hD : A.Definable₁ L D := by
    simp only [Definable₁, Definable, Fin.isValue]
    refine ⟨((L.lhomWithConstants A).onBoundedFormula φ).toFormula.relabel
      (Sum.elim Empty.elim id) |>.subst fun i => Fin.lastCases (Term.var 0)
        (fun j => (L.con ⟨x j, by
        nth_rw 1 [← hA.closure_eq_self]
        simp only [Subtype.coe_prop]
        ⟩).term) i, ?_⟩
    ext v
    simp only [Fin.isValue, mem_ofPred_eq, Formula.relabel, Formula.Realize,
      BoundedFormula.realize_subst, BoundedFormula.realize_relabel, Nat.add_zero, Fin.castAdd_zero,
      Fin.cast_refl, Function.comp_id, Fin.natAdd_zero, D]
    rw [← Formula.Realize, BoundedFormula.realize_toFormula, LHom.realize_onBoundedFormula]
    congr! 1
    ext i; cases i using Fin.lastCases <;> simp

Goal state after:
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
hD : A.Definable₁ L D
⊢ ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
h : listDecode φ.snd.listEncode = [φ]
⊢ [φ][0]? = some φ

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_7.inl
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' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
val✝ : ↑↑S
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') (Sum.inl val✝) =
    (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: case e'_7.inr
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' :
  (BoundedFormula.constantsVarsEquiv φ).Realize (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (⇑S.subtype ∘ default)
val✝ : Fin 1
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') (Sum.inr val✝) =
    (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: case H
L : Language
n : ℕ
f : L.Functions n
⊢ f = f

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
⊢ lift.{max u v, max u v} (max ℵ₀ L.card) ≤ lift.{max u v, max u v} (max ℵ₀ L.card)

Tactic:
rfl

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✝ : Nonempty M
φ : L.Formula α
h : M ⊨ φ.exClosure
v : ↥(BoundedFormula.freeVarFinset φ) → M
hv : Realize (BoundedFormula.restrictFreeVar φ id) v
v' : α → M := fun a ↦ if hmem : a ∈ BoundedFormula.freeVarFinset φ then v ⟨a, hmem⟩ else Classical.choice ⋯
⊢ ∀ (a : ↥(BoundedFormula.freeVarFinset φ)), v (id a) = v' ↑a

Tactic:
grind

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case falsum
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✝ : ℕ
xs : Fin n✝ → M
⊢ BoundedFormula.falsum.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ BoundedFormula.falsum.Realize v xs

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr.refine_1
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
x✝ : ↑(range f)
⊢ (((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
        Sum.inl)
      x✝ =
    ((y ∘ f) ∘ rangeSplitting f) x✝

Tactic:
simp [Set.apply_rangeSplitting f]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤
            (List.map (fun ij ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun ij ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).exs.Realize
      default ↔
    Nonempty (Fin n ↪ M)

Tactic:
BoundedFormula.realize_exs

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ (∃ xs,
      (List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤
            (List.map (fun ij ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun ij ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).Realize
        default xs) ↔
    Nonempty (Fin n ↪ M)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
⊢ TermDefinable₁ L f ↔ A.TermDefinable L fun v ↦ f (v ())

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p
⊢ IsAlgClosed K

Tactic:
by
  refine IsAlgClosed.of_exists_root _ ?_
  intro p hpm hpi
  have h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n} :=
    Theory.Model.mono h (by simp [Theory.ACF])
  simp only [Theory.model_iff, Set.mem_image,
    forall_exists_index, and_imp] at h
  have := h _ p.natDegree (natDegree_pos_iff_degree_pos.2
    (degree_pos_of_irreducible hpi)) rfl
  rw [realize_genericMonicPolyHasRoot] at this
  exact this ⟨_, hpm, rfl⟩

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₁
C : L[[↑A]].Constants
⊢ Function.const (α → M) ↑C = fun v ↦ ↑C

Tactic:
rfl

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

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

Tactic:
rw [models_sentence_iff, IsSatisfiable]

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

Goal state before:
pp: case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ 5 ≤ Order.succ ℵ₀

Tactic:
exact le_trans (le_of_lt (lt_aleph0_of_finite _)) (Order.le_succ _)

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:
intro p hp x hx

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
⊢ (aeval x) p = 0
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case intro
ι : 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), ⋯⟩, ⋯⟩
hres_surj : Function.Surjective res
w : ι → ↥(Algebra.adjoin K ↑s)
hwS' : w ∈ S'
hw : res ⟨w, hwS'⟩ = ⟨fun i ↦ ⟨v i, ⋯⟩, hvS⟩
⊢ ((fun v i ↦ (eval v) (ps i)) fun i ↦ ↑(w i)) = v

Tactic:
simpa [Subtype.ext_iff, funext_iff] using hw

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

Goal state before:
pp: case inr
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
a₁✝ : OreLocalization S X
⊢ ∀ ⦃a₂ : OreLocalization S X⦄, j a₁✝ = j a₂ → a₁✝ = a₂

Tactic:
grind

Goal state after:
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ Nat.card (Extension k p n) = Nat.card k ^ n

Tactic:
← pow_finrank_eq_natCard p,

Goal state after:
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ p ^ Module.finrank (ZMod p) (Extension k p n) = Nat.card k ^ n
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ p ^ Module.finrank (ZMod p) (Extension k p n) = Nat.card k ^ n

Tactic:
← pow_finrank_eq_natCard p,

Goal state after:
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ p ^ Module.finrank (ZMod p) (Extension k p n) = (p ^ Module.finrank (ZMod p) k) ^ n
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ p ^ Module.finrank (ZMod p) (Extension k p n) = (p ^ Module.finrank (ZMod p) k) ^ n

Tactic:
finrank_zmod_extension,

Goal state after:
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ p ^ (Module.finrank (ZMod p) k * n) = (p ^ Module.finrank (ZMod p) k) ^ n
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a✝ b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
a : F
⊢ (AdjoinRoot.mk p).toIntAlgHom (C a′) = (algebraMap F (AdjoinRoot p)) a′

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * Multiset.count n {n} = Fintype.card K - 1

Tactic:
Multiset.count_singleton_self,

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ (Fintype.card K - 1) * 1 = Fintype.card K - 1
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgHom K L).toLinearMap)^[↑i] x) =
    (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x)

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ adjoin F (⇑b ∘ φ '' Iio i ∪ {(⇑b ∘ φ) i}) = adjoin F (⇑b ∘ φ '' Iio i ∪ {b (φ i)})

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
x✝ : ↥(adjoin F (⇑b ∘ φ '' Iio i))
⊢ ((succEquiv i) f).1 x✝ = (f.comp (Subalgebra.inclusion ⋯)) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
succ_top

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
⊢ filtration ⊤ = filtration ⊤