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

Goal state before:
pp: case h
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_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
key2 : ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))
⊢ C (i a⁻¹) * ((Multiset.map (fun c ↦ C b) s).prod * (Multiset.map (fun c ↦ X - C (c / b)) s).prod) =
    (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod

Tactic:
Function.const_def (α := E) (y := C b),

Goal state after:
case h
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_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
key2 : ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))
⊢ C (i a⁻¹) * ((Multiset.map (Function.const E (C b)) s).prod * (Multiset.map (fun c ↦ X - C (c / b)) s).prod) =
    (Multiset.map ((fun x ↦ X - C x) ∘ fun c ↦ c / b) s).prod
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
⊢ Function.Injective h.comp

Tactic:
by
  intro f g hfg
  ext x; exact h.injective (DFunLike.congr_fun hfg x)

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
⊢ Function.Injective h.toHom.comp

Tactic:
by
  intro f g hfg
  ext x; exact h.injective (DFunLike.congr_fun hfg x)

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n - C x).Gal

Tactic:
rw [hx, C_0, sub_zero]
    exact gal_X_pow_isSolvable n

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
φ : L ≃ᴸ L'
⊢ Function.RightInverse φ.invLHom.onTerm φ.toLHom.onTerm

Tactic:
rw [Function.rightInverse_iff_comp, ← LHom.comp_onTerm, φ.right_inv, LHom.id_onTerm]

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
h : n✝ ≤ n✝
⊢ castLE h (equal t₁✝ t₂✝) = equal t₁✝ t₂✝

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
k n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ ∀ {m n : ℕ} (km : n✝ ≤ m) (mn : m ≤ n), castLE mn (castLE km (equal t₁✝ t₂✝)) = castLE ⋯ (equal t₁✝ t₂✝)

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
L' : Language
α : Type u'
β : Type v'
γ : Type u_1
L'' : Language
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)
fr' : (n : ℕ) → L'.Relations n → L''.Relations n
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ mapTermRel ft' fr' (fun x ↦ id) (mapTermRel ft fr (fun x ↦ id) (equal t₁✝ t₂✝)) =
    mapTermRel (fun x ↦ ft' x ∘ ft x) (fun x ↦ fr' x ∘ fr x) (fun x ↦ id) (equal t₁✝ t₂✝)

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x ↦ id) (fun x ↦ id) (fun x ↦ id) (equal t₁✝ t₂✝) = equal t₁✝ t₂✝

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ mapTermRel (fun x t ↦ Term.relabel (Sum.map id (natAdd 0)) t) (fun x ↦ id) (fun x ↦ castLE ⋯) (equal t₁✝ t₂✝) =
    castLE ⋯ (equal t₁✝ t₂✝)

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ (LHom.id L).onBoundedFormula (equal t₁✝ t₂✝) = id (equal t₁✝ t₂✝)

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case equal
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ (φ.comp ψ).onBoundedFormula (equal t₁✝ t₂✝) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁✝ t₂✝)

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
⊢ ((BoundedFormula.equal t₁✝ t₂✝).Realize (fun i ↦ Quotient.mk' (x i)) fun i ↦ Quotient.mk' (v i)) ↔
    ∀ᶠ (a : α) in ↑u, (BoundedFormula.equal t₁✝ t₂✝).Realize (fun i ↦ x i a) fun i ↦ v i a

Tactic:
| equal =>

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'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x ↦ id) (equal t₁✝ t₂✝)).Realize v' xs ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, (mapTermRel ft fr (fun x ↦ id) f₁✝).Realize v' xs ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, (mapTermRel ft fr (fun x ↦ id) f₂✝).Realize v' xs ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x ↦ id) (f₁✝ ⟹ f₂✝)).Realize v' xs ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
simp [mapTermRel, Realize, ih1, ih2]

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'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin (k + n✝) → M
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) (equal t₁✝ t₂✝)).Realize v' xs ↔ (equal t₁✝ t₂✝).Realize (v xs) (xs ∘ natAdd k)

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (xs : Fin (k + n✝) → M),
    (mapTermRel ft fr (fun x ↦ castLE ⋯) f₁✝).Realize v' xs ↔ f₁✝.Realize (v xs) (xs ∘ natAdd k)
ih2 :
  ∀ (xs : Fin (k + n✝) → M),
    (mapTermRel ft fr (fun x ↦ castLE ⋯) f₂✝).Realize v' xs ↔ f₂✝.Realize (v xs) (xs ∘ natAdd k)
xs : Fin (k + n✝) → M
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) (f₁✝ ⟹ f₂✝)).Realize v' xs ↔ (f₁✝ ⟹ f₂✝).Realize (v xs) (xs ∘ natAdd k)

Tactic:
simp [mapTermRel, Realize, ih1, ih2]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin (n✝ + n') → M
hmn : m ≤ n✝
⊢ (mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) (equal t₁✝ t₂✝)).Realize v xs ↔
    (equal t₁✝ t₂✝).Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
rw [Cardinal.le_def]

Goal state after:
case refine_2.refine_2
L : Language
α : Type u'
⊢ Nonempty (α ⊕ (i : ℕ) × L.Functions i ↪ (n : ℕ) × L.Term (α ⊕ Fin n))
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
| equal =>

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
⊢ (φ.onBoundedFormula (equal t₁✝ t₂✝)).Realize v xs ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ ⨆ i, S i = (closure L).toFun (⋃ i, ↑(S i))

Tactic:
closure_iUnion,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ ⨆ i, S i = ⨆ i, (closure L).toFun ↑(S i)
Module: Mathlib.ModelTheory.Encoding

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

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
⊢ φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs

Tactic:
by
  induction n with
  | zero => exact Unique.exists_iff.symm
  | succ n ih =>
    simp only [BoundedFormula.exs, ih, realize_ex]
    constructor
    · rintro ⟨xs, x, h⟩
      exact ⟨_, h⟩
    · rintro ⟨xs, h⟩
      rw [← Fin.snoc_init_self xs] at h
      exact ⟨_, _, h⟩

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.subtype.toHom.range = S

Tactic:
ext x
  simp only [Hom.mem_range, Embedding.coe_toHom, coe_subtype]
  refine ⟨?_, fun h => ⟨⟨x, h⟩, rfl⟩⟩
  rintro ⟨⟨y, hy⟩, rfl⟩
  exact hy

Goal state after:
Module: Mathlib.ModelTheory.Semantics

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

Tactic:
| equal =>

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ L[[α]].card ≤ ℵ₀

Tactic:
simp only [withConstants, card_sum, add_le_aleph0, lift_le_aleph0]

Goal state after:
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ L.card ≤ ℵ₀ ∧ (constantsOn α).card ≤ ℵ₀
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
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✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (BoundedFormula.equal t₁✝ t₂✝).Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (BoundedFormula.equal t₁✝ t₂✝).Realize v xs

Tactic:
| equal =>

Goal state after:
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:
by
  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.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : (α → M) → M
g : α → (β → M) → M
hf : A.TermDefinable L f
hg : ∀ (i : α), A.TermDefinable L (g i)
⊢ A.TermDefinable L fun b ↦ f fun x ↦ g x b

Tactic:
by
  obtain ⟨φ, rfl⟩ := hf
  choose ψ hψ using hg
  use φ.subst ψ
  simp [hψ]

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case neg
L : Language
T : L.Theory
h : ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
φ : L.Sentence
M : T.ModelType
hφ : ¬↑M ⊨ φ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ

Tactic:
right
      exact models_sentence_iff.2 fun N => (Sentence.realize_not N).2
        (mt (elementarilyEquivalent_iff.1 (h M N) φ).2 hφ)

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ Formula.Realize φ default ∨ (Formula.not φ).Realize default

Tactic:
Formula.realize_not,

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
φ : L.Sentence
⊢ Formula.Realize φ default ∨ ¬Formula.Realize φ default
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_3
E : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field E
inst✝⁶ : Field L
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra K L
inst✝³ : Algebra E L
inst✝² : IsScalarTower K E L
inst✝¹ : FinTrdeg K E
inst✝ : FinTrdeg E L
⊢ Algebra.trdeg K E < Cardinal.aleph0 ∧ Algebra.trdeg E L < Cardinal.aleph0

Tactic:
exact ⟨trdeg_lt_aleph0 K E, trdeg_lt_aleph0 E L⟩

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
⊢ x ∈ nilradical R ↔ ∃ n, x ^ p ^ n = 0

Tactic:
refine ⟨fun ⟨n, h⟩ ↦ ⟨n, ?_⟩, fun ⟨n, h⟩ ↦ ⟨p ^ n, h⟩⟩

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : 1 < p
x✝ : x ∈ nilradical R
n : ℕ
h : x ^ n ∈ 0
⊢ x ^ p ^ n = 0
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p (0, 0) * Quot.mk (R K p) (m, x) = mk K p (0, 0)

Tactic:
quot_mk_eq_mk,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p (0, 0) * mk K p (m, x) = mk K p (0, 0)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ Quot.mk (R K p) (m, x) * mk K p (0, 0) = mk K p (0, 0)

Tactic:
quot_mk_eq_mk,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p (m, x) * mk K p (0, 0) = mk K p (0, 0)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[n + z] x) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)

Tactic:
H

Goal state after:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ ∃ r, x = r ^ ↑n

Tactic:
simpa using exists_eq_pow_of_odd x (by simpa using hk)

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ mk K p (0, ↑x) = mk K p (0, ↑y)

Tactic:
H

Goal state after:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ mk K p (0, ↑y) = mk K p (0, ↑y)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬x = 0
⊢ (⇑(frobenius K p))^[m] (x * x⁻¹) = 1

Tactic:
rw [mul_inv_cancel₀ this, iterate_map_one]

Goal state after:
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: 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⟮α⟯ = ⊤
ω : Ω
hω : α ∈ ↑(M ω)
⊢ ⊤ ≤ comap ω K₀

Tactic:
rwa [← hα, adjoin_simple_le_iff]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x ↦ ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
x : G
hj' : ↑(g j) = ↑x
hi' : ↑(g i) = ↑x
hx : x ∈ c
⊢ x ∈ ⊥

Tactic:
rw [ne_eq, ← Subtype.mk.injEq (p := (· ∈ (s : Set ι))) i hi j hj] at h'

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x ↦ ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : ¬⟨i, hi⟩ = ⟨j, hj⟩
c : Set G
x : G
hj' : ↑(g j) = ↑x
hi' : ↑(g i) = ↑x
hx : x ∈ c
⊢ x ∈ ⊥
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: 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 : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : minpoly F x = minpoly F y
⊢ False

Tactic:
rw [minpoly.eq_zero hy] at hx

Goal state after:
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 : Set.range (minpoly F) = Set.range (minpoly F)
σ : E →ₐ[F] K
y : K
hy : ¬IsIntegral F y
x : E
hx : minpoly F x = 0
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: 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

Tactic:
exact not_irreducible_C _ hm

Goal state after:
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 := ⋯ }
hc : a * c = c * a
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 = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * (c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b) - c⁻¹ * a * ((⇑((ad (↥k) D) a))^[n - 1] b * a) =
    a * (c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b) - a * (c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a)

Tactic:
sub_right_inj,

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 := ⋯ }
hc : a * c = c * a
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 = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ c⁻¹ * a * ((⇑((ad (↥k) D) a))^[n - 1] b * a) = a * (c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a)
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ x.carrier = y.carrier → x = y

Tactic:
H

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
H : x.carrier = y.carrier
⊢ x = y
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
y : ConjRootClass K L
⊢ ∃ a, mk K a = -y ∧ ∃ b, mk K b = y ∧ a + b = 0

Tactic:
induction y with
    | h y => exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩

Goal state after: