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

Goal state before:
pp: case all
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), f✝.Realize v ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')) ↔
    ∀ (x : M), f✝.Realize v (snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x)

Tactic:
refine forall_congr' fun x => iff_eq_eq.mpr (congr rfl (funext (Fin.lastCases ?_ fun i => ?_)))

Goal state after:
case all.refine_1
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
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') (last k) =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x (last k)

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
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
⊢ ∀ s_1 ∈ Set.range fun t ↦ ⋂ (_ : t ∈ s), ↑t, ClosedUnder f s_1

Tactic:
rintro _ ⟨t, rfl⟩

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
s : Set (L.Substructure M)
n : ℕ
f : L.Functions n
t : L.Substructure M
⊢ ClosedUnder f ((fun t ↦ ⋂ (_ : t ∈ s), ↑t) t)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
φ : L[[α]].BoundedFormula β n
v : β → M
xs : Fin n → M
⊢ (constantsVarsEquiv φ).Realize (Sum.elim (fun a ↦ ↑(L.con a)) v) xs ↔ φ.Realize v xs

Tactic:
refine realize_mapTermRel_id (fun n t xs => realize_constantsVarsEquivLeft) fun n R xs => ?_

Goal state after:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap (((fun x ↦ Equiv.sumEmpty (L.Relations x) ((constantsOn α).Relations x)) n) R) xs = RelMap R xs
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
S' : L.Substructure M
hS' : S' ∈ {S | s ⊆ ↑S}
⊢ S ≤ S'

Tactic:
rintro _ ⟨t, rfl⟩

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }
S' : L.Substructure M
hS' : S' ∈ {S | s ⊆ ↑S}
t : L.Term { x // x ∈ s }
⊢ Term.realize Subtype.val t ∈ S'
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Set M
m : M
⊢ m ∈ (closure L).toFun s ↔ m ∈ s

Tactic:
by
  rw [← SetLike.mem_coe, closure_eq_of_isRelational]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S✝ : L.Substructure M
s : Set M
φ : M →[L] N
S : L.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → N
hx : ∀ (i : Fin n), x i ∈ ⇑φ '' ↑S
⊢ φ (funMap f fun i ↦ Classical.choose ⋯) = funMap f x

Tactic:
simp only [Hom.map_fun, SetLike.mem_coe]

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S✝ : L.Substructure M
s : Set M
φ : M →[L] N
S : L.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → N
hx : ∀ (i : Fin n), x i ∈ ⇑φ '' ↑S
⊢ funMap f (⇑φ ∘ fun i ↦ Classical.choose ⋯) = funMap f x
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsComplete

Tactic:
apply Categorical.isComplete.{0, 0, 0} (Order.succ ℵ₀) _
    (ACF_categorical _ (Order.lt_succ _))
    (Order.le_succ ℵ₀)

Goal state after:
case h2
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ Cardinal.lift.{0, 0} Language.ring.card ≤ Cardinal.lift.{0, 0} (Order.succ ℵ₀)

case hS
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ ∀ (M : (Theory.ACF p).ModelType), Infinite ↑M
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S

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

Goal state after:
case intro
ι : Type u_1
K : Type u_2
R : Type u_3
inst✝⁴ : Field K
inst✝³ : Finite K
inst✝² : CommRing R
inst✝¹ : Finite ι
inst✝ : Algebra K R
alg : Algebra.IsAlgebraic K R
ps : ι → MvPolynomial ι R
S : Set (ι → R)
hm : Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S
hinj : Set.InjOn (fun v i ↦ (eval v) (ps i)) S
is_int : ∀ (x : R), IsIntegral K x
v : ι → R
hvS : v ∈ S
val✝ : Fintype ι
s : Finset R := (univ.biUnion fun i ↦ image (fun x ↦ coeff x (ps i)) (ps i).support) ∪ image v univ
hv : ∀ (i : ι), v i ∈ Algebra.adjoin K ↑s
hs₁ : ∀ (i : ι), ∀ k ∈ (ps i).support, coeff k (ps i) ∈ Algebra.adjoin K ↑s
⊢ v ∈ (fun v i ↦ (eval v) (ps i)) '' S
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ if c ≤ b then b else c
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
⊢ a ∣ b

Tactic:
if_pos h

Goal state after:
a✝ a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b
hz : b * c ≠ 0
h : c ≤ b
habc : a ≤ b * c
⊢ a ∣ b
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
hp : Nat.Prime p
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
by
  have : Fact p.Prime := ⟨hp⟩
  let := compatibleRingOfRing (AlgebraicClosure (ZMod p))
  rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _
    (AlgebraicClosure (ZMod p)), realize_genericPolyMapSurjOnOfInjOn]
  rintro v ⟨f, _⟩
  exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
p : ℕ
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
hp : Nat.Prime p
⊢ Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Goal state after:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
p : ℕ
hp : Nat.Prime p
⊢ ⟨p, hp⟩ ∈ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}

Tactic:
exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

Goal state after:
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ FinTrdeg K L ↔ Algebra.trdeg K L < Cardinal.aleph0

Tactic:
by
  constructor
  · intro ⟨E, fg, alg⟩
    rw [← trdeg_add_eq K E, trdeg_eq_zero_iff.2 alg, add_zero]
    rw [← essFiniteType_iff, Algebra.essFiniteType_iff_exists_subalgebra] at fg
    obtain ⟨S₀, M, fin, islocal⟩ := fg
    rw [← trdeg_add_eq K S₀, trdeg_eq_zero_iff.2 islocal.isAlgebraic, add_zero]
    exact trdeg_lt_aleph0_of_finiteType
  · intro h
    obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L
    have fin : s.Finite := Cardinal.lt_aleph0_iff_set_finite.1 (hs.cardinalMk_eq_trdeg.trans_lt h)
    constructor
    refine ⟨adjoin K s, fg_adjoin_of_finite fin, ?_⟩
    have alg := hs.isAlgebraic_field
    rwa [Subtype.range_coe] at alg

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

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Fintype σ
⊢ #↑{s | ∀ (n : σ), s n ≤ Fintype.card K - 1} = #↑{s | ∀ (n : σ), s n < Fintype.card K}

Tactic:
refine Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => ?_⟩
      refine forall_congr' fun n => le_tsub_iff_right ?_
      exact Fintype.card_pos_iff.2 ⟨0⟩

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

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

Tactic:
· exact exists_linearIndependent_algEquiv_apply_of_infinite K L

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
L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
f : L₁ ⟶ L₂
g : L₂ ⟶ L₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₁ with

Goal state after:
case op
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ
g : L₂ ⟶ L₃
L₁ : FiniteGaloisIntermediateField k K
f : op L₁ ⟶ L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: case op.op.op
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ L₂ : FiniteGaloisIntermediateField k K
f : op L₁ ⟶ op L₂
L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Tactic:
induction L₁ with

Goal state after:
case op.op.op.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₂ L₃ : FiniteGaloisIntermediateField k K
g : op L₂ ⟶ op L₃
L₁ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₁
isGalois✝ : IsGalois k ↥L₁
f : op { toIntermediateField := L₁, finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ } ⟶ op L₂
⊢ finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g
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) ((⇑(frobenius K p))^[y.1] x) * (frobenius K p) ((⇑(frobenius K p))^[n] y.2))

Tactic:
← map_mul,

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) ((⇑(frobenius K p))^[y.1] x * (⇑(frobenius K p))^[n] y.2))
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
⊢ toAlgEquivAux g (toAlgEquivAux g⁻¹ x) = x

Tactic:
let L := adjoin k {x, toAlgEquivAux g⁻¹ x}
    have hx : x ∈ L.1 := subset_adjoin _ _ (Set.mem_insert x {toAlgEquivAux g⁻¹ x})
    have hx' : toAlgEquivAux g⁻¹ x ∈ L.1 := subset_adjoin _ _ (Set.mem_insert_of_mem x rfl)
    simp only [toAlgEquivAux_eq_proj_of_mem _ _ L hx', mk_toAlgEquivAux g⁻¹ x L hx' hx, map_inv,
      AlgEquiv.aut_inv, AlgEquiv.apply_symm_apply]

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}
⊢ IsOpen (⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup)

Tactic:
suffices mulEquivToLimit k K '' L.1.fixingSubgroup = Set.preimage Subtype.val fix1 by
    rw [this]
    exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)

Goal state after:
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}
⊢ ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
hqn : q ∣ n
b : ↥K⟮x⟯
⊢ b ^ q ≠ AdjoinSimple.gen K x

Tactic:
hb

Goal state after:
case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
hqn : q ∣ n
b : ↥K⟮x⟯
hb : b ^ q = AdjoinSimple.gen K x
⊢ False
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
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm) K [α] =
    Subalgebra.map ↑(adjoinRootXPowSubCEquiv hζ H hα).symm ⊤

Tactic:
Algebra.map_top,

Goal state after:
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
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm) K [α] = (↑(adjoinRootXPowSubCEquiv hζ H hα).symm).range
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
have ⟨ζ, hζ⟩ := hK
  rw [mem_primitiveRoots finrank_pos] at hζ
  obtain ⟨σ, hσ⟩ := ‹IsCyclic Gal(L/K)›
  have hσ' := orderOf_eq_card_of_forall_mem_zpowers hσ
  -- Since the minimal polynomial of `σ` over `K` is `Xⁿ - 1`,
  -- `σ` has an eigenvector `v` with eigenvalue `ζ`.
  have : IsRoot (minpoly K σ.toLinearMap) ζ := by
    rw [IsGalois.card_aut_eq_finrank] at hσ'
    simpa [minpoly_algEquiv_toLinearMap σ (isOfFinOrder_of_finite σ), hσ',
      sub_eq_zero] using hζ.pow_eq_one
  obtain ⟨v, hv⟩ := (Module.End.hasEigenvalue_of_isRoot this).exists_hasEigenvector
  have hv' := hv.pow_apply
  simp_rw [← AlgEquiv.pow_toLinearMap, AlgEquiv.toLinearMap_apply] at hv'
  -- We claim that `v` is the desired root.
  refine ⟨v, ?_, ?_⟩
  · -- Since `v ^ n` is fixed by `σ` (`σ (v ^ n) = ζ ^ n • v ^ n = v ^ n`), it is in `K`.
    rw [← IntermediateField.mem_bot,
      ← OrderIso.map_bot IsGalois.intermediateFieldEquivSubgroup.symm]
    intro ⟨σ', hσ'⟩
    obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
    rw [smul_pow', Submonoid.smul_def, AlgEquiv.smul_def, hv', smul_pow, ← pow_mul,
      mul_comm, pow_mul, hζ.pow_eq_one, one_pow, one_smul]
  · -- Since `σ` does not fix `K⟮α⟯`, `K⟮α⟯` is `L`.
    apply IsGalois.intermediateFieldEquivSubgroup.injective
    rw [map_top, eq_top_iff]
    intro σ' hσ'
    obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
    have := hσ' ⟨v, IntermediateField.mem_adjoin_simple_self K v⟩
    simp only [AlgEquiv.smul_def, hv'] at this
    conv_rhs at this => rw [← one_smul K v]
    obtain ⟨k, rfl⟩ := hζ.dvd_of_pow_eq_one n (smul_left_injective K hv.2 this)
    rw [pow_mul, ← IsGalois.card_aut_eq_finrank, pow_card_eq_one', one_pow]
    exact one_mem _

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

Goal state before:
pp: case refine_1
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
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (toSubmodule A).lTensorOne (((algebraMap R ↥⊥) x' * (algebraMap R ↥⊥) y') ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) x' ⊗ₜ[R] a) *
      (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) y' ⊗ₜ[R] b)

Tactic:
← map_mul,

Goal state after:
case refine_1
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
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) (x' * y') ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) x' ⊗ₜ[R] a) *
      (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) y' ⊗ₜ[R] b)
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
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
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] ((algebraMap R ↥⊥) x' * (algebraMap R ↥⊥) y')) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] (algebraMap R ↥⊥) x') *
      (toSubmodule A).rTensorOne (b ⊗ₜ[R] (algebraMap R ↥⊥) y')

Tactic:
← map_mul,

Goal state after:
case refine_1
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
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (algebraMap R ↥⊥) (x' * y')) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] (algebraMap R ↥⊥) x') *
      (toSubmodule A).rTensorOne (b ⊗ₜ[R] (algebraMap R ↥⊥) y')
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
a : F
⊢ (algebraMap K L) ((iterateFrobeniusₛₗ F K L p hn) ((algebraMap F L) a)) =
    (algebraMap K L) ((algebraMap F K) a ^ p ^ n)

Tactic:
rw [← map_pow, ← IsScalarTower.algebraMap_apply, map_pow,
    algebraMap_iterateFrobeniusₛₗ F K L p hn]

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1

Tactic:
mem_perfectClosure_iff_natSepDegree_eq_one

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ (minpoly F x).natSepDegree = 1 ↔ (minpoly F x).natSepDegree = 1
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : fa.fieldRange.LinearDisjoint ↥fb.fieldRange
⊢ M = ⊥

Tactic:
simp_rw [linearDisjoint_iff', AlgHom.fieldRange_toSubalgebra,
    Subalgebra.linearDisjoint_iff_injective] at H

Goal state after:
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
⊢ M = ⊥
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this : ExpChar (↥M) q
⊢ (fun x ↦ x ^ q ^ n) '' S ⊆ ↑(adjoin F S)

Tactic:
· rintro _ ⟨y, hy, rfl⟩
    exact pow_mem (subset_adjoin F S hy) _

Goal state after: