mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝² : Nontrivial S
this✝¹ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝ : Algebra.IsAlgebraic (↥Sy) A
x✝ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥Rxy) (↥Sy) A
⊢ Algebra.IsAlgebraic (↥Rxy) A

Tactic:
have : IsScalarTower Rx Rxy Sy := .of_algebraMap_eq fun ⟨a, _⟩ ↦ Subtype.ext rfl

Goal state after:
case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝³ : Nontrivial S
this✝² : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝¹ : Algebra.IsAlgebraic (↥Sy) A
x✝ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower ↥Rx ↥Rxy ↥Sy
⊢ Algebra.IsAlgebraic (↥Rxy) A
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
q : ℕ
hF : ExpChar F q
n : ℕ
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
obtain - | hprime := hF

Goal state after:
case zero
F : Type u
inst✝¹ : Field F
f : F[X]
n : ℕ
inst✝ : CharZero F
⊢ ((expand F (1 ^ n)) f).natSepDegree = f.natSepDegree

case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup Gal(E/F)
K : IntermediateField F E
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
⊢ ϕ • (↑x * ↑y) = ↑x * ↑y

Tactic:
rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]

Goal state after:
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : OpenNormalSubgroup G
h : (fun H ↦ ↑H.toOpenSubgroup) A = (fun H ↦ ↑H.toOpenSubgroup) B
x✝ : G
⊢ x✝ ∈ (↑A.toOpenSubgroup).carrier ↔ x✝ ∈ (↑B.toOpenSubgroup).carrier

Tactic:
dsimp at h

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : OpenNormalSubgroup G
h : ↑A.toOpenSubgroup = ↑B.toOpenSubgroup
x✝ : G
⊢ x✝ ∈ (↑A.toOpenSubgroup).carrier ↔ x✝ ∈ (↑B.toOpenSubgroup).carrier
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : (fun x ↦ f • x) w1 = (fun x ↦ g • x) w2
⊢ False

Tactic:
dsimp at h

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : f * w1 = g * w2
⊢ False
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁶ : CommRing R
inst✝⁵ : Field S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
y : M
x✝ : y ∈ N
⊢ 0 ∈ 1

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
| (integralClosure R K).toSubring.subtype x

Tactic:
← algeq.symm_apply_apply x

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f
algeq : ↥(integralClosure R K) ≃ₐ[R] R := ((integralClosure R K).equivOfEq ⊥ ⋯).trans (Algebra.botEquivOfInjective ⋯)
x : ↥(integralClosure R K)
| (integralClosure R K).toSubring.subtype (algeq.symm (algeq x))
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ R[x]
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ R[x]
⊢ 0 ∈ R[x]

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree

Tactic:
rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']

Goal state after:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpolyDiv R x).natDegree + (X - C x).natDegree

R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ p = a' * b'

pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ ¬IsUnit a'

Tactic:
· exact Polynomial.map_injective _ (IsFractionRing.injective R K) H

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ ¬IsUnit a'
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ IsUnit (map (algebraMap R K) (C (integerNormalization R⁰ p).content * C ↑u))

Tactic:
← map_mul,

Goal state after:
case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ IsUnit (map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u)))
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E

Tactic:
by
  refine ⟨⟨fun x ↦ (isIntegral' F (algebraMap E K x)).tower_bot_of_field⟩, fun x h ↦ ?_⟩
  rw [IsSeparable, ← minpoly.algebraMap_eq (algebraMap E K).injective] at h
  obtain ⟨y, h⟩ := inseparable F _ h
  exact ⟨y, (algebraMap E K).injective (h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm)⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b

Tactic:
← map_mul,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
h1 : C (c * d) * p = integerNormalization R⁰ a * integerNormalization R⁰ b
this : NormalizedGCDMonoid R
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
h1 :
  C (integerNormalization R⁰ a).content * C (integerNormalization R⁰ b).content * (integerNormalization R⁰ b).primPart *
      (integerNormalization R⁰ a).primPart =
    C (c * d) * p
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b

Tactic:
← map_mul,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
h1 :
  C ((integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content) * (integerNormalization R⁰ b).primPart *
      (integerNormalization R⁰ a).primPart =
    C (c * d) * p
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ (x + y) ^ p ^ (n + m) ∈ (algebraMap R A).rangeS

Tactic:
add_pow_expChar_pow,

Goal state after:
case h
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
p : ℕ
inst✝ : ExpChar A p
x y : A
n : ℕ
hx : x ^ p ^ n ∈ (algebraMap R A).rangeS
m : ℕ
hy : y ^ p ^ m ∈ (algebraMap R A).rangeS
⊢ x ^ p ^ (n + m) + y ^ p ^ (n + m) ∈ (algebraMap R A).rangeS
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : Algebra.IsSeparable K L
ι : Type u_5
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (b i)
inst✝ : IsIntegrallyClosed A
⊢ (↑A (Algebra.linearMap C L)).range ≤ Submodule.span A (Set.range ⇑((traceForm K L).dualBasis ⋯ b))

Tactic:
by
  rw [← LinearMap.BilinForm.dualSubmodule_span_of_basis,
    ← LinearMap.BilinForm.le_flip_dualSubmodule, Submodule.span_le]
  rintro _ ⟨i, rfl⟩ _ ⟨y, rfl⟩
  simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.BilinForm.flip_apply,
    traceForm_apply]
  refine Submodule.mem_one.mpr <| IsIntegrallyClosed.isIntegral_iff.mp ?_
  exact isIntegral_trace ((IsIntegralClosure.isIntegral A L y).algebraMap.mul (hb_int i))

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral A (b x)
b' : Basis (↥s) K L := (traceForm K L).dualBasis ⋯ b
this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')
f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict
⊢ Submodule.comap (↑A (Algebra.linearMap C L)).rangeRestrict (Submodule.inclusion ⋯).ker = ⊥

Tactic:
Submodule.ker_inclusion,

Goal state after:
A : Type u_1
K : Type u_2
inst✝¹⁷ : CommRing A
inst✝¹⁶ : Field K
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
L : Type u_3
inst✝¹³ : Field L
C : Type u_4
inst✝¹² : CommRing C
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra C L
inst✝⁷ : IsIntegralClosure C A L
inst✝⁶ : Algebra A C
inst✝⁵ : IsScalarTower A C L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral A (b x)
b' : Basis (↥s) K L := (traceForm K L).dualBasis ⋯ b
this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')
f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict
⊢ Submodule.comap (↑A (Algebra.linearMap C L)).rangeRestrict ⊥ = ⊥
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
⊢ b ∈ ↑Q → b ∈ ⋃ i ∈ ↑⊤, ↑(i • P)

Tactic:
hb

Goal state after:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
⊢ b ∈ ⋃ i ∈ ↑⊤, ↑(i • P)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hf : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)
hx : IsIntegral K x
⊢ (Polynomial.map (algebraMap K F) (minpoly K x)).Splits

Tactic:
exact hf

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ ¬a.valMinAbs * 2 = ↑(n + 1)

pp: n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2

Tactic:
· intro he
    rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
    exacts [h (Nat.cast_nonneg _), zero_lt_two]

Goal state after:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
⊢ valMinAbs 0 = 0

Tactic:
by simp only [valMinAbs_def_pos, if_true, Int.ofNat_zero, zero_le, val_zero]

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Tactic:
have : (a.val : ℤ) - n ≤ 0 := by
    rw [sub_nonpos, Int.ofNat_le]
    exact a.val_le
  rw [valMinAbs_def_pos]
  split_ifs
  · rw [Int.natAbs_natCast, natCast_zmod_val]
  · rw [← Int.cast_natCast, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
      Int.cast_natCast, Int.cast_natCast, natCast_self, sub_zero, natCast_zmod_val]

Goal state after:
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : ¬n ≤ k
⊢ q.coeff n = 0

Tactic:
Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_not_ge hn)

Goal state after:
case neg
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
hn : ¬n ≤ k
⊢ 0 = 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) = ∑ x, ?f x

Tactic:
← trace_eq_sum_embeddings (AlgebraicClosure L) (x := x)

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
x : L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((Algebra.trace K L) x)) =
    (algebraMap K (AlgebraicClosure L)) ((Algebra.trace K L) x)
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
⊢ (trace K L) x = 0 x

Tactic:
rw [trace_eq_zero_of_not_exists_basis]

Goal state after:
case neg.h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : ¬FiniteDimensional K L
⊢ ¬∃ s, Nonempty (Basis (↥s) K L)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
g : G
⊢ (algebraMap B (B ⧸ Q)) (g • b) * (algebraMap B (B ⧸ Q)) (g • b₀) =
    (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)

Tactic:
hb

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
b₀ : B
hx : ∀ (g : G), g • Q = Q → (algebraMap B (B ⧸ Q)) (g • b₀) = (algebraMap B (B ⧸ Q)) b₀
a b : B
ha1 : ∀ (g : G), g • a = a
ha2 : a ∉ Q
hb : ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0)
g : G
⊢ (algebraMap B (B ⧸ Q)) (if g • Q = Q then a else 0) * (algebraMap B (B ⧸ Q)) (g • b₀) =
    (algebraMap B (B ⧸ Q)) (if g • Q = Q then a * b₀ else 0)