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

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ C (i a⁻¹ * i a) = 1

Tactic:
← i.map_mul,

Goal state after:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
⊢ C (i (a⁻¹ * a)) = 1
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L

Tactic:
by
    rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]

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
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
⊢ Group.IsSolvable (minpoly F x).Gal

Tactic:
let p := minpoly F (x ^ n)

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
n : ℕ
hn : n ≠ 0
hα : Group.IsSolvable (minpoly F (x ^ n)).Gal
p : F[X] := minpoly F (x ^ n)
⊢ Group.IsSolvable (minpoly F x).Gal
Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
| (FreeCommRing.lift v) p

Tactic:
rw [← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)]

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
| (FreeCommRing.lift v) (Term.realize FreeCommRing.of (Classical.choose ⋯))
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ castLE mn✝ (castLE km✝ (rel R✝ ts✝)) = castLE ⋯ (rel R✝ ts✝)

Tactic:
simp only [castLE]

Goal state after:
case rel
L : Language
α : Type u'
k n✝¹ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝¹)
m✝ n✝ : ℕ
km✝ : n✝¹ ≤ m✝
mn✝ : m✝ ≤ n✝
⊢ rel R✝ (Term.relabel (Sum.map id (Fin.castLE mn✝)) ∘ Term.relabel (Sum.map id (Fin.castLE km✝)) ∘ ts✝) =
    rel R✝ (Term.relabel (Sum.map id (Fin.castLE ⋯)) ∘ ts✝)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬(∼θ).Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
simp_rw [realize_not, Classical.not_not]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_4
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula Empty n),
    (∀ (xs : Fin n → M), f₁.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₁.Realize default xs) →
      (∀ (xs : Fin n → M), f₂.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ f₂.Realize default xs) →
        ∀ (xs : Fin n → M), (f₁ ⟹ f₂).Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ (f₁ ⟹ f₂).Realize default xs

Tactic:
intro _ _ _ ih1 ih2 _
    simp [ih1, ih2]

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
⊢ Set.range ⇑f = ↑⊤ ↔ Function.Surjective ⇑f

Tactic:
coe_top,

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ Set.range ⇑f = Set.univ ↔ Function.Surjective ⇑f
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (fun x_1 ↦ x (natAdd (Classical.choose ⋯) x_1)) = default

Tactic:
funext i

Goal state after:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
i : Fin 0
⊢ x (natAdd (Classical.choose ⋯) i) = default i
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (fun x_1 ↦ x (natAdd (Classical.choose ⋯) x_1)) = default

Tactic:
funext i

Goal state after:
case e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
i : Fin 0
⊢ x (natAdd (Classical.choose ⋯) i) = default i
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
⊢ listDecode (flatMap (fun φ ↦ φ.snd.listEncode) l) = l

Tactic:
by
  suffices h : ∀ (φ : Σ n, L.BoundedFormula α n)
      (l' : List ((Σ k, L.Term (α ⊕ Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ))),
      (listDecode (listEncode φ.2 ++ l')) = φ::(listDecode l') by
    induction l with
    | nil =>
      simp [listDecode]
    | cons φ l ih => rw [flatMap_cons, h φ _, ih]
  rintro ⟨n, φ⟩
  induction φ with
  | falsum => intro l; rw [listEncode, singleton_append, listDecode]
  | equal =>
    intro l
    rw [listEncode, cons_append, cons_append, listDecode, dif_pos]
    · simp only [eq_mp_eq_cast, cast_eq, nil_append]
    · simp only
  | @rel φ_n φ_l φ_R ts =>
    intro l
    rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode]
    have h : ∀ i : Fin φ_l, ((List.map Sum.getLeft? (List.map (fun i : Fin φ_l =>
      Sum.inl (⟨(⟨φ_n, rel φ_R ts⟩ : Σ n, L.BoundedFormula α n).fst, ts i⟩ :
        Σ n, L.Term (α ⊕ (Fin n)))) (finRange φ_l) ++ l))[↑i]?).join = some ⟨_, ts i⟩ := by
      intro i
      simp only [Option.join, map_append, map_map, getElem?_fin, id, Option.bind_eq_some_iff,
        getElem?_eq_some_iff, length_append, length_map, length_finRange, exists_eq_right]
      refine ⟨lt_of_lt_of_le i.2 le_self_add, ?_⟩
      rw [getElem_append_left, getElem_map]
      · simp only [getElem_finRange, cast_mk, Fin.eta, Function.comp_apply, Sum.getLeft?_inl]
      · simp only [length_map, length_finRange, is_lt]
    rw [dif_pos]
    swap
    · exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩
    rw [dif_pos]
    swap
    · intro i
      obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [h2]
    simp only [Option.join, eq_mp_eq_cast, cons.injEq, Sigma.mk.inj_iff, heq_eq_eq, rel.injEq,
      true_and]
    refine ⟨funext fun i => ?_, ?_⟩
    · obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i)
      rw [cast_eq_iff_heq]
      exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2
    rw [List.drop_append, length_map, length_finRange, Nat.sub_self, drop, drop_eq_nil_of_le,
      nil_append]
    rw [length_map, length_finRange]
  | imp _ _ ih1 ih2 =>
    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]
  | all _ ih =>
    intro l
    simp only at *
    rw [listEncode, cons_append, listDecode]
    simp only [ih, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, sigmaAll_apply, drop_succ_cons, drop_zero]

Goal state after:
Module: Mathlib.ModelTheory.ElementarySubstructures

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

Tactic:
funext i

Goal state after:
case e'_7
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)
i : ↑↑S ⊕ Fin 1
⊢ Sum.elim (fun a ↦ ↑(L.con a)) (Subtype.val ∘ v') i = (⇑S.subtype ∘ Sum.elim (fun a ↦ ↑(L.con a)) v') i
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} #((k : ℕ) × L.Term (α ⊕ Fin k)) + lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
Term.card_sigma,

Goal state after:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)) + lift.{max u u', v} #((n : ℕ) × L.Relations n ⊕ ℕ)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
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 ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
⊢ ↑(v' 0) ∈ D

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

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 ⊨ ψ
v' : Fin 1 → ↥S
hv' : φ.Realize v'
hv'' : φ.Realize (Subtype.val ∘ v')
⊢ ↑(v' 0) ∈ D
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
t : L.Term α
⊢ ∃ φ, (tupleGraph fun v ↦ Term.realize v t) = ofPred φ.Realize

Tactic:
refine ⟨(t.relabel some).equal (Term.var none), ?_⟩

Goal state after:
M : Type u_1
L : Language
inst✝ : L.Structure M
α : Type u_2
t : L.Term α
⊢ (tupleGraph fun v ↦ Term.realize v t) = ofPred ((Term.relabel some t).equal (var none)).Realize
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s := by
    refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_
    rw [model_distinctConstantsTheory]
    intro a as b bs ab
    rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
    exact
      h.some.injective
        ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
          (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝¹ : Inhabited M
this✝ : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
this : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
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✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ ∃ x, eval x p = 0

Tactic:
simp only [Theory.model_iff, Set.mem_image,
    forall_exists_index, and_imp] at h

Goal state after:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
⊢ ∃ x, eval x p = 0
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.{v, max u v} (lift.{u, v} #(List { x // x ∈ s })) ≤ lift.{max u v, v} (max #↑s ℵ₀)

Tactic:
lift_id'.{v, u},

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.{u, v} #(List { x // x ∈ s }) ≤ lift.{max u v, v} (max #↑s ℵ₀)
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 + 1)) • s ^ (i - (j + 1)) • x

Tactic:
change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
    rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]

Goal state after:
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 + 1)) • s ^ (i - (j + 1)) • x

Tactic:
change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
    rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]

Goal state after:
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: case inr
α : Type u
h : Infinite α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n

Tactic:
simpa only [← Cardinal.infinite_iff, h, true_or, iff_true] using Infinite.nonempty_field

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
⊢ Module.finrank k (Extension k p n) = n

Tactic:
refine Nat.pow_right_injective (Finite.one_lt_card : 2 ≤ Nat.card k) ?_

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
⊢ (fun x ↦ Nat.card k ^ x) (Module.finrank k (Extension k p n)) = (fun x ↦ Nat.card k ^ x) n
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this : Fact (minpoly F k).Monic
⊢ DifferentialAlgebra F K

Tactic:
have : Fact (Irreducible (minpoly F k)) :=
    ⟨minpoly.irreducible (IsAlgebraic.of_finite ..).isIntegral⟩

Goal state after:
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
k : K := ⋯.choose
h : F⟮k⟯ = ⊤
this✝ : Fact (minpoly F k).Monic
this : Fact (Irreducible (minpoly F k))
⊢ DifferentialAlgebra F K
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ (eval a) (indicator b) = 0

Tactic:
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C,
    Finset.prod_eq_zero_iff]

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ∃ a_1 ∈ Finset.univ, 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)

Tactic:
rcongr e
        apply_fun e at h
        simp only [AlgEquiv.commutes, map_add, map_sum, map_mul] at h
        convert! h using 2
        · rcongr x
          simp [logDeriv, algEquiv_deriv']
        · rw [algEquiv_deriv']

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 * (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)

Tactic:
← iterate_succ_apply,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 * (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1.succ] x * (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 * (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 * (⇑(frobenius K p))^[x.1] (n + 1, (frobenius K p) y).2)

Tactic:
← iterate_succ_apply,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 * (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 * (⇑(frobenius K p))^[x.1.succ] y)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 + (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)

Tactic:
← iterate_succ_apply,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1.succ] x + (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 + (⇑(frobenius K p))^[x.1] (n + 1, (frobenius K p) y).2)

Tactic:
← iterate_succ_apply,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 + (⇑(frobenius K p))^[x.1.succ] y)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
h : Function.Injective ⇑(frobenius R p)
x : R
⊢ x ∈ pNilradical R p → x ∈ ⊥

Tactic:
by
  rw [mem_pNilradical, Ideal.mem_bot]
  exact fun ⟨n, _⟩ ↦ h.iterate n (by rwa [← coe_iterateFrobenius, map_zero])

Goal state after:
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
h2 : lift.{max u v, v} #F ≤ lift.{v, max u v} (Module.rank F K)
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
lift_id'.{v, u},

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} #σ ≤ Module.rank F K ∧ ℵ₀ ≤ Module.rank F K
i : σ
hx : Transcendental F ((algebraMap R K) (MvPolynomial.X i))
h2 : lift.{max u v, v} #F ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
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
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ e (root (X ^ n - C a)) / root (X ^ n - C a) * root (X ^ n - C a) = e (root (X ^ n - C a))

Tactic:
· refine div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ K [α] = ⊤

Tactic:
by
  apply Subalgebra.map_injective (B := K[n√a]) (f := (adjoinRootXPowSubCEquiv hζ H hα).symm)
    (adjoinRootXPowSubCEquiv hζ H hα).symm.injective
  rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
    (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
    Set.image_singleton, AlgEquiv.coe_toAlgHom, adjoinRootXPowSubCEquiv_symm_eq_root,
      adjoinRoot_eq_top]

Goal state after: