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

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

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ↑a = ∑ x, ↑(c₀ x) * logDeriv (u₀ x) + v₀′

Tactic:
rw [h₀]

Goal state after:
F : Type u_1
K : Type u_2
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Differential F
inst✝⁹ : Differential K
inst✝⁸ : Algebra F K
inst✝⁷ : DifferentialAlgebra F K
A : Type u_3
inst✝⁶ : Field A
inst✝⁵ : Algebra K A
inst✝⁴ : Algebra F A
inst✝³ : Differential A
inst✝² : IsScalarTower F K A
inst✝¹ : ContainConstants F K
inst1 : IsLiouville F K
inst2 : IsLiouville K A
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc✝ : ∀ (x : ι), (c x)′ = 0
u : ι → A
v : A
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
ι₀ : Type
w✝ : Fintype ι₀
c₀✝ : ι₀ → K
hc₀ : ∀ (x : ι₀), (c₀✝ x)′ = 0
u₀ : ι₀ → K
v₀ : K
h₀ : ↑a = ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′
c₀ : ι₀ → F
hc : ∀ (x : ι₀), (algebraMap F K) (c₀ x) = c₀✝ x
⊢ ∑ x, c₀✝ x * logDeriv (u₀ x) + v₀′ = ∑ x, ↑(c₀ x) * logDeriv (u₀ x) + v₀′
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: 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
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ False

Tactic:
simp_rw [eq_univ_iff_forall, mem_ofPred] at this

Goal state after:
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
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝¹⁰ : Field M
inst✝⁹ : Algebra K M
inst✝⁸ : Algebra L M
inst✝⁷ : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra S ↥F
inst✝³ : Algebra S M
inst✝² : IsScalarTower S (↥F) M
inst✝¹ : Algebra S K
inst✝ : IsScalarTower S K M
⊢ (F.extendRight M).algebra' = algebra F M

Tactic:
by
  with_reducible_and_instances rfl

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 ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0

Tactic:
rw [pNilradical_eq_nilradical hp]

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

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

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0

Tactic:
· rwa [hn, pow_zero, pow_one] at h

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
hn : ¬n = 0
⊢ x = 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Tactic:
obtain ⟨n, y, hy⟩ := pow_mem f p x
    obtain ⟨m, z, hz⟩ := pow_mem i p y
    exact ⟨n + m, z, by rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: X✝ Y✝ Z : Type u
inst✝¹⁴ : Group X✝
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : IsTopologicalGroup X✝
inst✝¹¹ : CompactSpace X✝
inst✝¹⁰ : TotallyDisconnectedSpace X✝
inst✝⁹ : Group Y✝
inst✝⁸ : TopologicalSpace Y✝
inst✝⁷ : IsTopologicalGroup Y✝
inst✝⁶ : CompactSpace Y✝
inst✝⁵ : TotallyDisconnectedSpace Y✝
inst✝⁴ : Group Z
inst✝³ : TopologicalSpace Z
inst✝² : IsTopologicalGroup Z
inst✝¹ : CompactSpace Z
inst✝ : TotallyDisconnectedSpace Z
X Y : ProfiniteGrp.{u_1}
f : X ⟶ Y
x✝ : IsIso ((forget₂ ProfiniteGrp.{u_1} Profinite).map f)
i : (forget₂ ProfiniteGrp.{u_1} Profinite).obj X ≅ (forget₂ ProfiniteGrp.{u_1} Profinite).obj Y :=
  asIso ((forget₂ ProfiniteGrp.{u_1} Profinite).map f)
e : ↑X.toProfinite.toTop ≃ₜ* ↑Y.toProfinite.toTop :=
  let __src := CompHausLike.homeoOfIso i;
  { toEquiv := __src.toEquiv, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso f

Tactic:
exact (ContinuousMulEquiv.toProfiniteGrpIso e).isIso_hom

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁶ : ExpChar M p
inst✝⁵ : ExpChar K p
inst✝⁴ : PerfectRing M p
inst✝³ : IsPRadical i p
inst✝² : ExpChar L p
inst✝¹ : IsPRadical j p
inst✝ : PerfectRing L p
x : L
⊢ (lift j i p) ((lift i j p) x) = x

Tactic:
rw [lift_comp_lift_apply, lift_self_apply]

Goal state after:
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 : ¬(⇑(frobenius K p))^[(0, 0).1] (m, x).2 = (⇑(frobenius K p))^[(m, x).1] (0, 0).2
⊢ mk K p (m, x) * (mk K p (m, x))⁻¹ = 1

Tactic:
rw [mk_inv, mk_mul_mk]

Goal state after:
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 : ¬(⇑(frobenius K p))^[(0, 0).1] (m, x).2 = (⇑(frobenius K p))^[(m, x).1] (0, 0).2
⊢ mk K p
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
        (⇑(frobenius K p))^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
          (⇑(frobenius K p))^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2) =
    1
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case inl
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 : ι
hcovers : (⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x) = Set.univ
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
y : G
hy✝ : y ∈ ⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • ↑(H k)
hk' : H k = H j
⊢ ∃ i, ∃ (_ : i ∈ Finset.univ), y ∈ f i • ↑(K i)

Tactic:
have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))

Goal state after:
case inl
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 : ι
hcovers : (⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x) = Set.univ
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
y : G
hy✝¹ : y ∈ ⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy✝ : y ∈ g k • ↑(H k)
hk' : H k = H j
i : ι
hi : i ∈ {x ∈ s | H x ≠ H j}
hy : y ∈ (g k * x⁻¹ * g i) • ↑(H i)
⊢ ∃ i, ∃ (_ : i ∈ Finset.univ), y ∈ f i • ↑(K i)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ (map (algebraMap K K[n√a]) X ^ n - map (algebraMap K K[n√a]) (C a)).Separable

Tactic:
map_C,

Goal state after:
case neg
K : Type u
inst✝ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a)) := { out := H }
this : Algebra K K[n√a] := inferInstance
hn : 0 < n
hn' : ¬n = 1
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ (map (algebraMap K K[n√a]) X ^ n - C ((algebraMap K K[n√a]) a)).Separable
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:
rwa [← Subalgebra.center_toSubring L, hcenter] at hxd

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
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F (↥E) ab' = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'

Tactic:
normalizedTraceAux_eq_of_finiteDimensional F a',

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
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F (↥E) ab' = (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) a' + normalizedTraceAux F (↥E) b'
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⟩
⊢ normalizedTraceAux F (↥E) ma' = m • normalizedTraceAux F (↥E) a'

Tactic:
normalizedTraceAux_eq_of_finiteDimensional F a',

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⟩
⊢ normalizedTraceAux F (↥E) ma' = m • (↑(Module.finrank F ↥E))⁻¹ • (trace F ↥E) a'
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : CommRing K
inst✝² : Ring L
inst✝¹ : Algebra K L
inst✝ : HasExponent K L
e : ℕ
h : e < exponent K L
⊢ ∃ a, a ^ ringExpChar K ^ e ∉ (algebraMap K L).range

Tactic:
by
  classical
  exact not_forall.mp <| Nat.find_min ‹HasExponent K L›.has_exponent h

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
this : a ^ ringExpChar K ^ elemExponent K a - (algebraMap K L) (elemReduct K a) = 0
⊢ (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a

Tactic:
sub_eq_zero,

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
this : a ^ ringExpChar K ^ elemExponent K a = (algebraMap K L) (elemReduct K a)
⊢ (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a

Tactic:
by
  have := minpoly_eq K a ▸ minpoly.aeval K a
  rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this

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

Goal state before:
pp: 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
f : K[X] := X ^ ringExpChar K ^ n - C y
⊢ a ^ ringExpChar K ^ n - (algebraMap K L) y = 0

Tactic:
sub_eq_zero,

Goal state after:
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
f : K[X] := X ^ ringExpChar K ^ n - C y
⊢ a ^ ringExpChar K ^ n = (algebraMap K L) y
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Module.Finite R ↥A
inst✝ : Module.Finite R ↥B
H : finrank R ↥(A ⊔ B) = finrank R ↥A * finrank R ↥B
⊢ A.LinearDisjoint B

Tactic:
by
  nontriviality R
  rw [← Module.finrank_tensorProduct] at H
  obtain ⟨j, hj⟩ := exists_linearIndependent_of_le_finrank H.ge
  rw [LinearIndependent] at hj
  let j' := Finsupp.linearCombination R j ∘ₗ
    (LinearEquiv.ofFinrankEq (A ⊗[R] B) _ (by simp)).toLinearMap
  replace hj : Function.Injective j' := by simpa [j']
  have hf : Function.Surjective (mulMap' A B).toLinearMap := mulMap'_surjective A B
  have := Subalgebra.finite_sup A B
  rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]
  exact Subtype.val_injective.comp (OrzechProperty.injective_of_surjective_of_injective j' _ hj hf)

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
q : ℕ
hF : ExpChar F q
S : Set E
⊢ IsPurelyInseparable F ↥(adjoin F S) ↔ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
    Set.subset_def, SetLike.mem_coe]

Goal state after:
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✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint ↥B
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.norm ↥A) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.norm F) x)

Tactic:
rw [linearDisjoint_iff'] at h₁
  refine h₁.norm_algebraMap ?_ x
  simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg toSubalgebra h₂

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) f.num -
      (algebraMap K[X] K⟮X⟯) f.num / (algebraMap K[X] K⟮X⟯) f.denom * (algebraMap K[X] K⟮X⟯) f.denom =
    0

Tactic:
div_mul_cancel₀ _ (algebraMap_ne_zero f.denom_ne_zero)

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) f.num - (algebraMap K[X] K⟮X⟯) f.num = 0
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
f_ne_zero : f ≠ 0
H : C f.num.leadingCoeff - f * C (f.denom.coeff f.num.natDegree) = 0
⊢ False

Tactic:
sub_eq_zero,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
f_ne_zero : f ≠ 0
H : C f.num.leadingCoeff = f * C (f.denom.coeff f.num.natDegree)
⊢ False
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this :
  (f.minpolyX ↥K⟮f⟯).natDegree ≤
    max f.num.natDegree
      (Polynomial.C ((algebraMap ↥K[f] ↥K⟮f⟯) ⟨f, ⋯⟩) * Polynomial.map (algebraMap K ↥K⟮f⟯) f.denom).natDegree
H : (algebraMap ↥K[f] ↥K⟮f⟯) ⟨f, ⋯⟩ = 0
⊢ f = C 0

Tactic:
simpa [map_zero] using congr($(H).val)

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

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ f * ↑this.unit = minpoly F x

Tactic:
by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ *
      (Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (Φ' E).content) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
map_C,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ *
      (Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content) * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
h : Function.Surjective ⇑f
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
by
  simpa using! congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h))

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x : F⟮X⟯
hx : x ≠ 0
⊢ (if x = 0 then 0 else exp x.intDegree) = exp x.intDegree

Tactic:
if_neg hx

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x : F⟮X⟯
hx : x ≠ 0
⊢ exp x.intDegree = exp x.intDegree
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
let : Algebra A B := (inclusion h1).toAlgebra

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this : Algebra ↥A ↥B := (inclusion h1).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : Function.Surjective ⇑f
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
by
  simpa using! congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h))

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.C ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩)) *
          Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
map_C,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.C
            (((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
              ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩)) *
          Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)