mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
y z : E
hy : y ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F y).Gal
q : F[X] := minpoly F y
a : E
hx : a ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮a, y⟯
p : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits

pp: case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x z : E
hx : x ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
p : F[X] := minpoly F x
a : E
hy : a ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮x, a⟯
q : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits

Tactic:
· exact ⟨isIntegral_of_mem_solvableByRad hx, hpq.1⟩

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x z : E
hx : x ∈ solvableByRad F E
hz : z ∈ solvableByRad F E
hx' : Group.IsSolvable (minpoly F x).Gal
p : F[X] := minpoly F x
a : E
hy : a ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F a).Gal
hz' : z ∈ F⟮x, a⟯
q : F[X] := minpoly F a
hpq :
  (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)).Splits ∧
    (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
⊢ IsIntegral F a ∧ (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F a)).Splits
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x✝¹ n' m : ℕ
φ : L.BoundedFormula α x✝¹
x✝ : ℕ
⊢ x✝ + (1 + n') ≤ x✝ + n' + 1

Tactic:
add_comm 1,

Goal state after:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n x✝¹ n' m : ℕ
φ : L.BoundedFormula α x✝¹
x✝ : ℕ
⊢ x✝ + (n' + 1) ≤ x✝ + n' + 1
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x = RelMap r y

Tactic:
← iff_eq_eq

Goal state after:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x ↔ RelMap r y
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ (↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ

Tactic:
by
  simp_rw [Sentence.Realize]
  rw [← realize_formula_cast φ, iff_eq_eq]
  exact congr rfl (Subsingleton.elim _ _)

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
i : Fin k
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') i.castSucc =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x i.castSucc

Tactic:
· simp only [Function.comp_apply, Fin.snoc_castSucc]
      refine (congr rfl (Fin.ext ?_)).trans (snoc_castSucc _ _ _)
      simp only [val_castSucc, val_cast]
      split_ifs <;> simp

Goal state after:
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
φ : M ↪ₑ[L] N
x y : M
⊢ φ x = φ y → x = y

Tactic:
exact (φ.map_formula ((var 0).equal (var 1)) fun i => if i = 0 then x else y).1

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
ih3

Goal state after:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
x✝ : M
⊢ f✝.Realize v' (snoc xs x✝) ↔ f✝.Realize v' (snoc xs x✝)

case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : ↥f✝.freeVarFinset → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : ↥(∀' f✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(∀' f✝).freeVarFinset), v (f a) = v' ↑a
x✝ : M
⊢ ∀ (a : ↥f✝.freeVarFinset), v (f a) = v' ↑a
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{u, w} #↥((closure L).toFun s) ≤ max ℵ₀ (lift.{u, w} #↑s + lift.{w, u} #((i : ℕ) × L.Functions i))

Tactic:
by
  rw [← lift_umax]
  refine lift_card_closure_le_card_term.trans (Term.card_le.trans ?_)
  rw [mk_sum, lift_umax.{w, u}]

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ ∃ (h : ↑i < φ_l + l.length),
    (List.map (Sum.getLeft? ∘ fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ List.map Sum.getLeft? l)[↑i] =
      some ⟨φ_n, ts i⟩

Tactic:
refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩

Goal state after:
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
i : Fin φ_l
⊢ (List.map (Sum.getLeft? ∘ fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l) ++ List.map Sum.getLeft? l)[↑i] =
    some ⟨φ_n, ts i⟩
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case imp
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝ ⟹ f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l'

Tactic:
intro l
    simp only at *
    rw [listEncode, List.append_assoc, cons_append, listDecode]
    simp only [ih1, ih2, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, getElem_cons_succ, sigmaImp_apply, drop_succ_cons, drop_zero]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.mp
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✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
a : M
h' : f✝.Realize (⇑g ∘ v) (⇑g ∘ snoc xs a)
⊢ f✝.Realize v (snoc xs a)

Tactic:
ih3

Goal state after:
case all.mp
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✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
h : ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
a : M
h' : f✝.Realize v (snoc xs a)
⊢ f✝.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

Tactic:
classical
    refine ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩
    have : Inhabited h'.some := Classical.inhabited_of_nonempty'
    exact Model.isSatisfiable (h'.some.defaultExpansion h)

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CompatibleRing K
p✝ : ℕ
inst✝¹ : CharP K p✝
inst✝ : IsAlgClosed K
p : K[X]
left✝ : p.Monic
hn0 : p.natDegree ∈ {n | 0 < n}
⊢ ∃ x, eval x ↑⟨p, ⋯⟩ = 0

Tactic:
exact IsAlgClosed.exists_root p (ne_of_gt
    (natDegree_pos_iff_degree_pos.1 hn0))

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ (∀ (x : Unit → M), f (x ()) = Term.realize x φ) ↔
    ∀ (x : M), f x = ((fun v ↦ Term.realize v φ) ∘ Function.const Unit) x

Tactic:
(Equiv.funUnique Unit M).forall_congr'

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ (∀ (b : M), ?m.36 b) ↔ ∀ (x : M), f x = ((fun v ↦ Term.realize v φ) ∘ Function.const Unit) x

M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ ∀ (b : M), f ((Equiv.funUnique Unit M).symm b ()) = Term.realize ((Equiv.funUnique Unit M).symm b) φ ↔ ?m.36 b

M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
f : M → M
φ : L[[↑A]].Term Unit
⊢ M → Prop
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case refine_1
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
⊢ ℵ₀ < #↑{ Carrier := M, struc := struc✝¹, is_model := is_model✝¹, nonempty' := nonempty'✝¹ }

Tactic:
rw [hM]; exact hκ

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:
cases subsingleton_or_nontrivial R

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

case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ Module.rank R ↥((FreeAlgebra.lift R) Subtype.val).range ≤ max #↑s ℵ₀
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
⊢ Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
intro v hvS
  cases nonempty_fintype ι
  /- `s` is the set of all coefficients of the polynomial, as well as all of
    the coordinates of `v`, the point I am trying to find the preimage of. -/
  let s : Finset R :=
    (Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪
      (univ : Finset ι).image v
  have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
    Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))
  have hs₁ : ∀ (i : ι) (k : ι →₀ ℕ),
      k ∈ (ps i).support → coeff k (ps i) ∈ Algebra.adjoin K (s : Set R) :=
    fun i k hk => Algebra.subset_adjoin
      (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
  have := isNoetherian_adjoin_finset s fun x _ => is_int x
  have : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
  -- The restriction of the polynomial map, `ps`, to the subalgebra generated by `s`
  let S' : Set (ι → Algebra.adjoin K (s : Set R)) :=
    (fun v => Subtype.val ∘ v) ⁻¹' S
  let res : S' → S' := fun x => ⟨fun i =>
    ⟨eval (fun j : ι => (x.1 j : R)) (ps i), eval_mem (hs₁ _) fun i => (x.1 i).2⟩,
      hm x.2⟩
  have hres_surj : Function.Surjective res := by
    rw [← Finite.injective_iff_surjective]
    intro x y hxy
    ext i
    simp only [Subtype.ext_iff, funext_iff] at hxy
    exact congr_fun (hinj x.2 y.2 (funext hxy)) i
  rcases hres_surj ⟨fun i => ⟨v i, hv i⟩, hvS⟩ with ⟨⟨w, hwS'⟩, hw⟩
  refine ⟨fun i => w i, hwS', ?_⟩
  simpa [Subtype.ext_iff, funext_iff] using hw

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

Goal state before:
pp: n : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : b * c = 0
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False

Tactic:
mul_eq_zero

Goal state after:
n : ℕ
h✝ : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : b = 0 ∨ c = 0
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
h : ↑n = 0
⊢ False
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
l : Type u_2
inst✝² : Field l
inst✝¹ : Algebra k l
inst✝ : Finite l
g : Gal(l/k)
n : ℕ := Module.finrank k l
this : NeZero n
i : ℕ
left✝ : i < n
hi : Extension.frob k p n ^ i = (algEquivExtension k p n l ⋯).symm.trans (g.trans (algEquivExtension k p n l ⋯))
x : l
⊢ g x = x ^ Nat.card k ^ i

Tactic:
simpa using (AlgEquiv.congr_arg (f := (algEquivExtension k p n l rfl).symm) <|
    AlgEquiv.congr_fun hi (algEquivExtension k p n l rfl x)).symm

Goal state after:
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

Tactic:
have := Finite.of_injective _ (algebraMap K L).injective
  have := Fintype.ofFinite K
  /- Since `K[X]` is a PID and `L` is a finitely generated `K[X]`-module (with `X` acting as
    the Frobenius automorphism), there exists `x : L` whose `K[X]`-annihilator is equal to the
    `K[X]`-annihilator of `L`, which is generated by `X ^ [L : K] - 1`. -/
  obtain ⟨x, hx⟩ := exists_ker_toSpanSingleton_eq_annihilator K[X]
    (AEval' (frobeniusAlgHom K L).toLinearMap)
  obtain ⟨x, rfl⟩ := (AEval'.of _).surjective x
  use x
  rw [← span_minpoly_eq_annihilator, minpoly_frobeniusAlgHom, eq_comm] at hx
  rw [← linearIndependent_equiv ((finCongr <| natDegree_X_pow_sub_C (R := K)).trans <|
    .ofBijective _ <| bijective_frobeniusAlgEquivOfAlgebraic_pow K L)]
  /- Therefore, `{Frⁱ | 0 ≤ i < [L : K]}` is linearly independent, which implies that
    `{Frⁱ(x) | 0 ≤ i < [L : K]}` is also linearly independent. -/
  convert!
    (AdjoinRoot.powerBasis (X_pow_sub_C_ne_zero Module.finrank_pos 1)).basis.linearIndependent
    |>.map' ((AEval'.of _).symm.toLinearMap ∘ₗ (liftQ _ _ hx.le).restrictScalars K) <| by
    exact congr($(ker_liftQ_eq_bot' _ _ hx).restrictScalars K)
  ext i
  simp_rw [Equiv.coe_trans, Function.comp_apply, finCongr_apply, Equiv.ofBijective_apply,
    AlgEquiv.coe_pow, AdjoinRoot.powerBasis, AdjoinRoot.powerBasisAux, Basis.coe_mk,
    coe_comp, LinearEquiv.coe_coe, LinearMap.coe_restrictScalars]
  refine (LinearEquiv.eq_symm_apply _).mpr (.symm <| (liftQ_apply ..).trans ?_)
  rw [toSpanSingleton_apply, AEval'.X_pow_smul_of, End.smul_def, End.coe_pow]
  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
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    have := Nonempty.intro j
    simp_rw [dif_pos this]
    apply Subalgebra.iSupLift_comp_inclusion

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
⊢ x ∈ {x}

Tactic:
by simp only [Set.mem_singleton_iff]

Goal state after:
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
this : ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1
⊢ IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup)

Tactic:
by
    rw [this]
    exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing K
inst✝⁶ : CommRing L
inst✝⁵ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x : K
⊢ (lift i j p) (i x) = j x

Tactic:
rw [lift_apply i j p _ 0 x (by rw [pow_zero, pow_one]), iterateFrobeniusEquiv_zero]; rfl

Goal state after:
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
this : ⋃ ω, ↑(M ω) = Set.univ
h✝ : Finite F
⊢ ∃ ω, ⊤ ≤ M ω

Tactic:
have ⟨α, hα⟩ := exists_primitive_element_of_finite_bot F FS

Goal state after:
case inl
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this✝ : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
this : ⋃ ω, ↑(M ω) = Set.univ
h✝ : Finite F
α : ↥FS
hα : F⟮α⟯ = ⊤
⊢ ∃ ω, ⊤ ≤ M ω
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
⊢ m i = 0

Tactic:
let b := s.prod fun j ↦ x - algebraMap F E j

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
⊢ m i = 0
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ (mulLeft (↥k) a) c - c * a = 0

Tactic:
← mulRight_apply (R := k)

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
⊢ (mulLeft (↥k) a) c - (mulRight (↥k) a) c = 0
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc : c⁻¹ * (a * (c * c⁻¹)) = c⁻¹ * (c * a) * c⁻¹
⊢ c⁻¹ * a = a * c⁻¹

Tactic:
mul_inv_cancel₀ hb.1,

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc : c⁻¹ * (a * 1) = c⁻¹ * (c * a) * c⁻¹
⊢ c⁻¹ * a = a * c⁻¹