mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
rcases finite_or_infinite X with _ | _

Goal state after:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Finite X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬(¬IsUnit a ∧ ∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b)

Tactic:
not_and_or

Goal state after:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬¬IsUnit a ∨ ¬∀ ⦃a_1 b : Cardinal.{u}⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
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 : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
this :
  ∀ {n : ℕ},
    (∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b) →
      ∀ (b c : Cardinal.{u_1}),
        ↑n ∣ b * c → ℵ₀ ≤ b * c → b ≠ 0 → c ≠ 0 → ℵ₀ ≤ b ∨ ℵ₀ ≤ c → ↑n ≠ 0 → ℵ₀ ≤ b → ↑n ∣ b ∨ ↑n ∣ c
hℵ₀b : ¬ℵ₀ ≤ b
⊢ ℵ₀ ≤ c * b

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

Tactic:
· rwa [mul_comm] at h'

Goal state after:
n✝ n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b c : Cardinal.{u_1}
hbc : ↑n ∣ b * c
h' : ℵ₀ ≤ b * c
hb : b ≠ 0
hc : c ≠ 0
hℵ₀ : ℵ₀ ≤ b ∨ ℵ₀ ≤ c
hn : ↑n ≠ 0
hℵ₀b : ℵ₀ ≤ b
⊢ ↑n ∣ b ∨ ↑n ∣ c
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
let p : ℕ := ringChar K

Goal state after:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c : Set K
S : Set (ι → K)
hS : c.Definable ring S
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S
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 L < Cardinal.aleph0

Tactic:
← Cardinal.lift_lt_aleph0,

Goal state after:
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
⊢ Cardinal.lift.{?u.43, u_5} (Algebra.trdeg K L) < Cardinal.aleph0
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
⊢ FinTrdeg K L

Tactic:
by
  rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0, ← lift_trdeg_add_eq K E L,
    Cardinal.add_lt_aleph0_iff, Cardinal.lift_lt_aleph0, Cardinal.lift_lt_aleph0]
  exact ⟨trdeg_lt_aleph0 K E, trdeg_lt_aleph0 E L⟩

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
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Cardinal.mk ι < Cardinal.aleph0

Tactic:
← Cardinal.lift_lt_aleph0,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
ι : Type u_3
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Cardinal.lift.{?u.24, u_3} (Cardinal.mk ι) < Cardinal.aleph0
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
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Algebra.trdeg K L < Cardinal.aleph0

Tactic:
← Cardinal.lift_lt_aleph0,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Cardinal.lift.{?u.25, u_2} (Algebra.trdeg K L) < Cardinal.aleph0
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this : NeZero f.natDegree
⊢ f ∣ X ^ Nat.card k ^ f.natDegree - X

Tactic:
have : Fact <| Irreducible f := ⟨hi⟩

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : Finite k
f : k[X]
hi : Irreducible f
n : ℕ
hdvd : f.natDegree ∣ n
a : AdjoinRoot f := AdjoinRoot.root f
this✝ : NeZero f.natDegree
this : Fact (Irreducible f)
⊢ f ∣ X ^ Nat.card k ^ f.natDegree - X
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

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this : Finite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case top
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
hi : IsSuccPrelimit ⊤
⊢ ⨆ j, filtration ↑j = filtration ⊤

Tactic:
iSup_range'

Goal state after:
case top
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
hi : IsSuccPrelimit ⊤
⊢ ⨆ i, filtration ↑i = filtration ⊤
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h : x = 0
⊢ x = 0

Tactic:
h

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp : ¬1 < p
h : x = 0
⊢ 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
m n : ℕ
x y : K
H : (⇑(frobenius K p))^[m] x = y
⊢ mk K p (n, x) = mk K p (m + n, y)

Tactic:
subst H

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m n : ℕ
x : K
⊢ mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
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 : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ ((x.2 ^ n) ^ p ^ x.1 * x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n * x.2) ^ p ^ (x.1 + x.1)

Tactic:
mul_pow,

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ ((x.2 ^ n) ^ p ^ x.1) ^ p ^ x.1 * (x.2 ^ p ^ x.1) ^ p ^ x.1 = (x.2 ^ n) ^ p ^ (x.1 + x.1) * x.2 ^ p ^ (x.1 + x.1)
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 : ℕ
⊢ ↑x = ↑0 ↔ ↑x = 0

Tactic:
Nat.cast_zero

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ
⊢ ↑x = 0 ↔ ↑x = 0
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
ω : ∃ ω, ⊤ ≤ M ω
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
exact ((botEquiv K K').toAlgHom.restrictScalars F).comp
    (ω.choose.codRestrict K₀.toSubalgebra fun x ↦ ω.choose_spec trivial)

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidableEq (Subgroup G)
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
have ⟨n, hn⟩ : ∃ n, n = (s.image H).card := exists_eq

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidableEq (Subgroup G)
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
n : ℕ
hn : n = (Finset.image H s).card
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y : G
⊢ y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)

Tactic:
z

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
⊢ z ∈ y • ↑(H j) → z ∈ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
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
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
i : F
hi : i ∈ s
⊢ m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)

Tactic:
b,

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)
i : F
hi : i ∈ s
⊢ m i • ((∏ j ∈ s, (x - (algebraMap F E) j)) * (x - (algebraMap F E) i)⁻¹) =
    m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
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
m : ℕ
hm2 : ∀ (n : ℕ), p ^ m ≤ n → (⇑((ad (↥k) D) a))^[n] = 0
h_exist : ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
⊢ ∃ n, 0 < n ∧ (⇑((ad (↥k) D) a))^[n] b ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0

Tactic:
refine ⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩
    set t := (Nat.find h_exist - 1 : ℕ) with ht
    by_cases! h_pos : 0 < t
    · convert! (ne_eq _ _) ▸ not_and.mp (Nat.find_min h_exist (m := t) (by lia)) h_pos
      lia
    · suffices h_find : Nat.find h_exist = 1 by
        rwa [h_find]
      rw [Nat.le_zero, ht, Nat.sub_eq_zero_iff_le] at h_pos
      linarith [(Nat.find_spec h_exist).1]

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)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ ((algebraMap K K[n√a]) ↑↑η * root (X ^ n - C a)) ^ n - (algebraMap K K[n√a]) a = 0

Tactic:
mul_pow,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ (algebraMap K K[n√a]) ↑↑η ^ n * root (X ^ n - C a) ^ n - (algebraMap K K[n√a]) a = 0
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)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
obtain ⟨σ, hσ⟩ := ‹IsCyclic Gal(L/K)›

Goal state after:
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)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ IsSplittingField K L (X ^ finrank K L - C a)

Tactic:
by
  constructor
  · rw [Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C,
      Polynomial.map_X]
    have ⟨_, hζ⟩ := hK
    rw [mem_primitiveRoots finrank_pos] at hζ
    exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha
  · rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα,
      IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite K α)]
    apply Algebra.adjoin_mono
    rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) ma' = m • (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) a'

Tactic:
smul_comm,

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) ma' = (↑(Module.finrank F ↥E))⁻¹ • m • (trace F ↥E) a'
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ 1⁻¹ • (trace F F) a = a

Tactic:
inv_one,

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
a : F
⊢ 1 • (trace F F) a = a
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ fa a = a ⊗ₜ[R] 1

Tactic:
by simp [fa]

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
⊢ (x' * y') • (a * b) = y' • (x' • a * b)

Tactic:
Algebra.smul_mul_assoc,

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
⊢ (x' * y') • (a * b) = y' • x' • (a * 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
⊢ (x' * y') • (a * b) = y' • (x' • a * b)

Tactic:
Algebra.smul_mul_assoc,

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
⊢ (x' * y') • (a * b) = y' • x' • (a * b)
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: case prime
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ elemExponent K a ≤ n

Tactic:
obtain ⟨y, hy⟩ := RingHom.mem_range.mp <| h

Goal state after:
case prime
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
⊢ elemExponent K a ≤ n
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
A B : IntermediateField F E
inst✝² : IsGalois F ↥A
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
⊢ A ⊓ B = ⊥

Tactic:
h

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
A B : IntermediateField F E
inst✝² : IsGalois F ↥A
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
⊢ ⊥ = ⊥
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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this : FiniteDimensional F ↥E'
v' : ↥s → ↥E' := fun i ↦ ⟨v ↑i, ⋯⟩
⊢ LinearIndependent F ((fun x ↦ v x ^ q ^ n) ∘ Subtype.val)

Tactic:
have h' : LinearIndependent F v' := (h s).of_comp E'.val.toLinearMap

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
this : FiniteDimensional F ↥E'
v' : ↥s → ↥E' := fun i ↦ ⟨v ↑i, ⋯⟩
h' : LinearIndependent F v'
⊢ LinearIndependent F ((fun x ↦ v x ^ q ^ n) ∘ Subtype.val)
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
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((algebraMap F E) z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ (frobenius E p) ((algebraMap F E) z) = (algebraMap F E) x

Tactic:
h

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this✝ : ExpChar E p
x z : F
h : (frobenius E p) ((algebraMap F E) z) = (algebraMap F E) x
this : (Algebra.ofId F E).toRingHom z ∈ perfectClosure F E
⊢ (algebraMap F E) x = (algebraMap F E) x
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
k : K
⊢ (C k).intDegree = 0

Tactic:
by
  rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]

Goal state after: