mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
hm : (aeval i) p = (aeval i) 0
j : F
hj : j ∈ s.erase i
⊢ m j * ∏ x ∈ s.erase j, (i - x) = 0

Tactic:
by

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 := ⋯ }
this : ((ad (↥k) D) a) c = 0
⊢ (mulLeft (↥k) a) c - (mulRight (↥k) a) c = 0

Tactic:
by

Goal state after:
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 : Transcendental F x
⊢ LinearIndependent F fun a ↦ (x - (algebraMap F E) a)⁻¹

Tactic:
by

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 := ⋯ }
⊢ a * c = c * a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: σ : Type u
K : Type v
inst✝ : Field K
I : Ideal (MvPolynomial σ K)
hI : I ≠ ⊤
⊢ Function.Injective ⇑((Ideal.Quotient.mk I).comp C)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: σ : Type u
K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
⊢ Module.rank K (MvPolynomial σ K) = lift.{v, u} #(σ →₀ ℕ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
σ : Type v
⊢ Module.rank K (MvPolynomial σ K) = #(σ →₀ ℕ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: σ : Type u
K : Type v
inst✝¹ : CommRing K
inst✝ : IsEmpty σ
⊢ Module.rank K (MvPolynomial σ K) = 1

Tactic:
by

Goal state after:
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 ι
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 : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hcovers' : ¬⋃ i ∈ {x | K x = K k}, f i • ↑(K i) = Set.univ
⊢ (Finset.image K Finset.univ).card < (Finset.image H s).card

Tactic:
by

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

Goal state before:
pp: σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
⊢ Module.rank F (FractionRing (MvPolynomial σ F)) = max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : CommRing F
inst✝⁴ : Nontrivial F
inst✝³ : CommRing E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this : #E = #↥K
⊢ lift.{max u w, v} #E = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : CommRing F
inst✝⁴ : Nontrivial F
inst✝³ : CommRing E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
⊢ lift.{max u w, v} #E = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
by

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

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ lift.{max u w, v} (Module.rank (↥K) E) ≠ 0

Tactic:
by

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
⊢ c⁻¹ * a = a * c⁻¹

Tactic:
by

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
⊢ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
⊢ lift.{max u w, v} (Module.rank F E) = max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
⊢ Module.rank F E = #E

Tactic:
by

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
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) = Set.univ
i : ι
hi : i ∈ {x ∈ s | H x = H j}
⊢ g i • ↑(H i) = ?m.119 i hi

Tactic:
by

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
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
by

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✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
⊢ ∀ i ∈ {i ∈ s | (H i).FiniteIndex}, (H i).FiniteIndex

Tactic:
by

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⁻¹
⊢ a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this : Algebra.Transcendental F ↥(A ⊔ B)
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
have := Algebra.Transcendental.infinite F A

Goal state after:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝ : Algebra.Transcendental F ↥(A ⊔ B)
this : Infinite ↥A
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
⊢ (X ^ n - C a).Splits

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
by

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
⊢ c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ m ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

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
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ #↑↑A + #↑↑B = max #↥A #↥B

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (Polynomial.map (algebraMap K ↥K⟮x⟯) (X ^ n) - C (AdjoinSimple.gen K x))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ Irreducible (X ^ (n * m) - C a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

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
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} #↑(↑A ∪ ↑B))) ℵ₀ ≤
    max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} (max #↥A #↥B))) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

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
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ max (max (Cardinal.lift.{v, u} #F) (Cardinal.lift.{u, v} (max #↥A #↥B))) ℵ₀ = Cardinal.lift.{u, v} (max #↥A #↥B)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

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
⊢ Module.rank F ↥(A ⊔ B) ≤ Module.rank F ↥A * Module.rank F ↥B

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: 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
h : ¬IsIntegral K x
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : Odd n
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ n - C a)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ p ^ n - C a)

Tactic:
by

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 * d - d * a = a

Tactic:
by

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)
⊢ (X ^ n - C a).Separable

Tactic:
by

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✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
⊢ ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ

Tactic:
by

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)
⊢ eval₂ (↑(Algebra.ofId K K[n√a])) (↑↑η • root (X ^ n - C a)) (X ^ n - C a) = 0

Tactic:
by

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)
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑1 • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) =
    1 (root (X ^ n - C a))

Tactic:
by

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)
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑(ε * η) • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) =
    (liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑ε • root (X ^ n - C a)) ⋯ *
        liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑η • root (X ^ n - C a)) ⋯)
      (root (X ^ n - C a))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
η : ↥(rootsOfUnity n K)
⊢ ((autAdjoinRootXPowSubC n a) η) (root (X ^ n - C a)) = ↑↑η • root (X ^ n - C a)

Tactic:
by

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)
inst✝ : NeZero n
σ : Gal(K[n√a]/K)
this✝¹ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this✝ : IsDomain K[n√a] := inferInstance
this : DecidableEq K := Classical.decEq K
⊢ (if a = 0 then 1 else σ (root (X ^ n - C a)) / root (X ^ n - C a)) ^ n = 1

Tactic:
by

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✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
i : κ
hi : i ∈ {x | K x = K k}
⊢ f i • ↑(K k) = ?m.488 i hi

Tactic:
by

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)
inst✝ : NeZero n
⊢ Function.LeftInverse (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H) (↑(autAdjoinRootXPowSubC n a)).toFun

Tactic:
by

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 ≠ ⊤
⊢ ∃ x ∉ k, IsSeparable (↥k) x

Tactic:
by

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✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
⊢ ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
equiv : L ≃+* ↥k := ((botEquiv L D).symm.trans φ).toRingEquiv
x✝² : Algebra L ↥k := equiv.toRingHom.toAlgebra
x✝¹ : Algebra (↥k) L := equiv.symm.toRingHom.toAlgebra
x✝ : IsScalarTower L (↥k) D
x : ↥k
⊢ (algebraMap (↥k) D) x = (algebraMap L D) ((algebraMap (↥k) L) x)

Tactic:
by

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)
inst✝ : NeZero n
⊢ Function.RightInverse (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H) (↑(autAdjoinRootXPowSubC n a)).toFun

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
equiv : L ≃+* ↥k := ((botEquiv L D).symm.trans φ).toRingEquiv
x✝⁴ : Algebra L ↥k := equiv.toRingHom.toAlgebra
x✝³ : Algebra (↥k) L := equiv.symm.toRingHom.toAlgebra
x✝² : IsScalarTower L (↥k) D
x✝¹ : IsScalarTower (↥k) L D
x✝ : Algebra.IsAlgebraic (↥k) D
x : D
hxd : x ∉ k
hx : IsSeparable (↥k) x
⊢ x ∉ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
⊢ ∃ x ∉ ⊥, IsSeparable L x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Nontrivial

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
inst✝¹ : IsDomain A
inst✝ : IsDomain B
⊢ Nontrivial (A ⊗[R] B)

Tactic:
by

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)
inst✝ : NeZero n
σ : K[n√a] ≃ₐ[K] K[n√a]
⊢ ↑((autAdjoinRootXPowSubCEquiv hζ H).symm σ) • root (X ^ n - C a) = σ (root (X ^ n - C a))

Tactic:
by

Goal state after: