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

Goal state before:
pp: L : Language
L' : Language
α : Type u'
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
t : L.Term α
⊢ (φ.comp ψ).onTerm t = (φ.onTerm ∘ ψ.onTerm) t

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp_rw [onTerm, ih]; rfl

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval x) q = 0
this : Group.IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ Group.IsSolvable q.Gal

Tactic:
refine Group.isSolvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval x) q = 0
this : Group.IsSolvable (q * C q.leadingCoeff⁻¹).Gal
⊢ q * C q.leadingCoeff⁻¹ ≠ 0
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p

Tactic:
simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize,
      forall_eq, Formula.realize_bot, false_iff]
    intro H
    cases (CharP.char_is_prime_or_zero K p) <;> simp_all

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
f : L[[α]].Functions 0
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
cases f

Goal state after:
case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

case func.zero.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = g (funMap _f✝ fun i ↦ Term.realize v (_ts✝ i))

Tactic:
HomClass.map_fun

Goal state after:
case func
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : L.HomClass F M N
g : F
v : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), Term.realize (⇑g ∘ v) (_ts✝ a) = g (Term.realize v (_ts✝ a))
⊢ (funMap _f✝ fun i ↦ Term.realize (⇑g ∘ v) (_ts✝ i)) = funMap _f✝ (⇑g ∘ fun i ↦ Term.realize v (_ts✝ i))
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: 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
f g : M ↪ₑ[L] N
h : (fun f ↦ ↑f) f = (fun f ↦ ↑f) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
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
g : M ↪ₑ[L] N
toFun✝ : M → N
map_formula'✝ : ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (toFun✝ ∘ x) ↔ φ.Realize x
h : (fun f ↦ ↑f) { toFun := toFun✝, map_formula' := map_formula'✝ } = (fun f ↦ ↑f) g
⊢ { toFun := toFun✝, map_formula' := map_formula'✝ } = g
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize (↑f ∘ v ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
← Function.comp_assoc

Goal state after:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
n : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin n → M
h :
  (φ.restrictFreeVar id).Realize ((↑f ∘ v) ∘ Subtype.val) (↑f ∘ xs) ↔
    (φ.restrictFreeVar id).Realize
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inl)
      (((Sum.elim (v ∘ Subtype.val) xs ∘ ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n)).symm) ∘
          ⇑(Fintype.equivFin (↥φ.freeVarFinset ⊕ Fin n))) ∘
        Sum.inr)
⊢ (φ.restrictFreeVar id).Realize ((⇑f ∘ v) ∘ Subtype.val) (⇑f ∘ xs) ↔ φ.Realize v xs
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:
by
  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
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a ↦ ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔
    (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a ↦ ↑(L.con a)) default) default

Tactic:
rw [iff_iff_eq]

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a ↦ ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default =
    (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a ↦ ↑(L.con a)) default) default
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' : Language
inst✝¹ : L'.Structure M
h : A.Definable L s
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
⊢ A.Definable L' s

Tactic:
obtain ⟨ψ, rfl⟩ := h

Goal state after:
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
L' : Language
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L[[↑A]].Formula α
⊢ A.Definable L' (ofPred ψ.Realize)
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 ⊨ ψ
⊢ (equivSentence.symm ψ).Realize (⇑S.subtype ∘ fun a ↦ ↑(L.con a))

Tactic:
Formula.realize_equivSentence_symm

Goal state after:
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 ⊨ ψ
⊢ M ⊨ ψ
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.ElementarySubstructure M
⊢ MeetsDefinable ↑S

Tactic:
rintro D ⟨x, hx⟩ ⟨φ, hφ⟩
  have hφx : φ.Realize ![x] := by
    simp [Set.ext_iff] at hφ
    simp [← hφ, hx]
  let ψ : L[[(S : Set M)]].Sentence := (φ.relabel Sum.inr).iExs
  have hψM : ψ.Realize M := by
    simpa only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
      Formula.realize_relabel, Sum.elim_comp_inr, ψ] using
        (⟨![x], hφx⟩ : ∃ w : Fin 1 → M, φ.Realize w)
  have hψS : ψ.Realize S := by
    rwa [← Formula.realize_equivSentence_symm_con, ← S.subtype.map_formula,
      Formula.realize_equivSentence_symm]
  simp only [Sentence.Realize, SetLike.coe_sort_coe, Formula.realize_iExs,
    Formula.realize_relabel, Sum.elim_comp_inr, ψ] at hψS
  obtain ⟨v', hv'⟩ := hψS
  refine ⟨v' 0, ?_, by simp⟩
  have hv'' : φ.Realize (Subtype.val ∘ v') := by
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv,
      ← S.subtype.map_boundedFormula] at hv'
    simp only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv]
    convert! hv' using 1
    funext i
    cases i <;> rfl
  change (Subtype.val ∘ v') ∈ {x | x 0 ∈ D}
  simpa [hφ] using hv''

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
rw [iff_iff_eq]

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

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ IsSatisfiable
    (⋃ i,
      (L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i))

Tactic:
isSatisfiable_directed_union_iff

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∀ (i : Finset ↑s),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i))

L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) i)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
L' : Language
inst✝² : L.Structure M
inst✝¹ : L'.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
⊢ A.TermDefinable L' f

Tactic:
obtain ⟨ψ, rfl⟩ := h

Goal state after:
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 α
⊢ A.TermDefinable L' fun v ↦ Term.realize v ψ
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs

Tactic:
simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'

Goal state after:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h' : φ.Realize v xs
⊢ φ.Realize v xs
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
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs

Tactic:
simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'

Goal state after:
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
h' : φ.Realize v xs
⊢ φ.Realize v xs
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}
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'✝ }
⊢ (∼(eqZero p)).Realize v✝ xs✝

Tactic:
have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq

Goal state after:
case inr
φ : 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'✝ }
hqp : q ≠ p
⊢ (∼(eqZero p)).Realize v✝ xs✝
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
  refine le_antisymm ?_ (radical_le_vanishingIdeal_zeroLocus _)
  rw [I.radical_eq_jacobson]
  apply le_sInf
  rintro J ⟨hJI, hJ⟩
  obtain ⟨x, hx⟩ := eq_vanishingIdeal_singleton_of_isMaximal K hJ
  refine hx.symm ▸ vanishingIdeal_anti_mono fun y hy p hp => ?_
  rw [← mem_vanishingIdeal_singleton_iff, Set.mem_singleton_iff.1 hy, ← hx]
  exact hJI hp

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
  rw [Theory.models_iff_finset_models] at h
  rcases h with ⟨T0, hT0, h⟩
  have f : ∀ ψ ∈ Theory.ACF 0,
      { s : Finset Nat.Primes // ∀ q : Nat.Primes, q ∉ s → Theory.ACF q ⊨ᵇ ψ } := by
    intro ψ hψ
    rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ
    apply Classical.choice
    rcases hψ with h | ⟨p, hp, rfl⟩
    · refine ⟨⟨∅, ?_⟩⟩
      intro q _
      exact Theory.models_sentence_of_mem
        (by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm];
            exact Set.mem_union_left _ h)
    · 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
  let s : Finset Nat.Primes := T0.attach.biUnion (fun φ => f φ.1 (hT0 φ.2))
  have hs : ∀ (p : Nat.Primes) ψ, ψ ∈ T0 → p ∉ s → Theory.ACF p ⊨ᵇ ψ := by
    intro p ψ hψ hpψ
    simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and,
      Subtype.exists, not_exists] at hpψ
    exact (f ψ (hT0 hψ)).2 p (hpψ _ hψ)
  refine Set.Finite.subset (Finset.finite_toSet s) (Set.compl_subset_comm.2 ?_)
  intro p hp
  exact Theory.models_of_models_theory (fun ψ hψ => hs p ψ hψ hp) h

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
  refine ⟨fun h => Set.infinite_of_finite_compl
      (finite_ACF_prime_not_realize_of_ACF_zero_realize φ h),
    not_imp_not.1 ?_⟩
  simpa [(ACF_isComplete (Or.inr rfl)).models_not_iff,
      fun p : Nat.Primes => (ACF_isComplete (Or.inl p.2)).models_not_iff] using
    finite_ACF_prime_not_realize_of_ACF_zero_realize φ.not

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
this : #(Localization S) ≤ #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R

Tactic:
rwa [← lift_le.{v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

Goal state after:
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a b : R
ha : a ≠ 0
hb : b ≠ 0
⊢ logDeriv (a / b) = logDeriv a - logDeriv b

Tactic:
unfold logDeriv
  simp [field, Derivation.leibniz_div]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ mk K p x ^ (n + 1) = mk K p (x.1, x.2 ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, ih, mk_mul_mk, mk_eq_iff]

Goal state after:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ ∃ z,
    (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + z]
        ((x.1, x.2 ^ n).1 + x.1,
            (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).2 =
      (⇑(frobenius K
              p))^[((x.1, x.2 ^ n).1 + x.1,
                (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).1 +
            z]
        (x.1, x.2 ^ n * x.2).2
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (C 1 - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False

Tactic:
← map_sub

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (C (1 - a))
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this : Fact (Irreducible (X ^ n - C a))
h : ¬root (X ^ n - C a) = 0
⊢ σ (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
rw [div_mul_cancel₀ _ h]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hcovers : ⋃ p ∈ s, ↑p = Set.univ
⊢ ⊤ ∈ s

Tactic:
contrapose! hcovers
  exact Subspace.biUnion_ne_univ_of_top_notMem hcovers

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
x✝ : L
⊢ (mk K x✝).minpoly.Separable

Tactic:
exact Algebra.IsSeparable.isSeparable K _

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict ∘ₗ
        includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range)
      (⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩) =
    LinearMap.id (⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩)

Tactic:
LinearMap.comp_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict)
      ((includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range) (⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩)) =
    LinearMap.id (⟨x ⊗ₜ[R] 1, ⋯⟩ ⊗ₜ[R] ⟨1 ⊗ₜ[R] y, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range ∘ₗ
        _root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict)
      (x ⊗ₜ[R] y) =
    LinearMap.id (x ⊗ₜ[R] y)

Tactic:
LinearMap.comp_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
x : S
y : T
⊢ (includeLeft.toLinearMap.range.mulMap includeRight.toLinearMap.range)
      ((_root_.TensorProduct.map includeLeft.toLinearMap.rangeRestrict includeRight.toLinearMap.rangeRestrict)
        (x ⊗ₜ[R] y)) =
    LinearMap.id (x ⊗ₜ[R] y)
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
hE : E ≠ ⊥
⊢ IsAlgebraic (↥E) X

Tactic:
rw [ne_eq, ← le_bot_iff, SetLike.not_le_iff_exists] at hE

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
hE : ∃ x ∈ E, x ∉ ⊥
⊢ IsAlgebraic (↥E) X
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : E →ₐ[F] L
⊢ Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
by
  rw [← lift_relrank_comap, comap_map]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
this : (map (↑(LinearEquiv.prodComm R M N)) F).IsFaceOf (map (↑(LinearEquiv.prodComm R M N)) (prod C₁ C₂))
⊢ IsFaceOf ?m.128 (prod ?m.126 ?m.127)

Tactic:
by simpa [PointedCone.map, Submodule.map]

Goal state after: