mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        (fixedField L.fixingSubgroup) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup

Tactic:
fixedField_fixingSubgroup L

Goal state after:
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
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        L ↔
    L.fixingSubgroup ≤ K.fixingSubgroup
Module: Mathlib.FieldTheory.SeparableDegree

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✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : g.Separable
⊢ IsSeparable F x

Tactic:
replace hsep := hsep.of_dvd <| minpoly.dvd E' x hzero

Goal state after:
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✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ IntermediateField.restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
⊢ IsSeparable F x
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
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional K ↥E
g : Gal(L/K)
⊢ g ∈ MulAction.stabilizer Gal(L/K) x ↔ g ∈ E.fixingSubgroup

Tactic:
simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm

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

Goal state before:
pp: F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
⊢ (map (IsScalarTower.toAlgHom F E E') L).fixingSubgroup = Subgroup.comap (restrictNormalHom E) L.fixingSubgroup

Tactic:
by
  ext f
  simp only [Subgroup.mem_comap, mem_fixingSubgroup_iff]
  constructor
  · rintro h x hx
    change f.restrictNormal E x = x
    apply_fun _ using (algebraMap E E').injective
    rw [AlgEquiv.restrictNormal_commutes]
    exact h _ ⟨x, hx, rfl⟩
  · rintro h _ ⟨x, hx, rfl⟩
    replace h := congr(algebraMap E E' $(show f.restrictNormal E x = x from h x hx))
    rwa [AlgEquiv.restrictNormal_commutes] at h

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
⊢ IsCyclic Gal(K/F)

Tactic:
have := finrank_eq_two F K ▸ AlgEquiv.card_le

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : Fintype.card Gal(K/F) ≤ 2
⊢ IsCyclic Gal(K/F)
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
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : (aeval y) (minpoly R x) = 0
⊢ eval y (minpolyDiv R x) = 0

Tactic:
by
  rw [← eval_map_algebraMap, ← minpolyDiv_spec R x] at hy
  simp only [eval_mul, eval_sub, eval_X, eval_C, mul_eq_zero] at hy
  exact hy.resolve_right (by rwa [sub_eq_zero])

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
⊢ (minpoly R s).degree ≤ p.degree

Tactic:
by_cases! hs : ¬IsIntegral R s

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
hs : ¬IsIntegral R s
⊢ (minpoly R s).degree ≤ p.degree

case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
hs : IsIntegral R s
⊢ (minpoly R s).degree ≤ p.degree
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ (restrictNormalHom ↥L'.toIntermediateField) σ ∈ Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H

Tactic:
← IntermediateField.fixingSubgroup_fixedField (Subgroup.map (restrictNormalHom L') H.1)

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ (restrictNormalHom ↥L'.toIntermediateField) σ ∈
    (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)).fixingSubgroup
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K✝ : Type u_2
inst✝³ : Field k
inst✝² : Field K✝
inst✝¹ : Algebra k K✝
inst✝ : IsGalois k K✝
K L : IntermediateField k K✝
⊢ { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        (IntermediateField.fixedField L.fixingSubgroup) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup

Tactic:
fixedField_fixingSubgroup L

Goal state after:
k : Type u_1
K✝ : Type u_2
inst✝³ : Field k
inst✝² : Field K✝
inst✝¹ : Algebra k K✝
inst✝ : IsGalois k K✝
K L : IntermediateField k K✝
⊢ { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        L ↔
    L.fixingSubgroup ≤ K.fixingSubgroup
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝ : Field k
H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, eval x p = 0
p : k[X]
hp : Irreducible p
hs : p.Separable
⊢ IsUnit (C p.leadingCoeff⁻¹)

Tactic:
by aesop

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
this : (aeval x) (minpoly k x) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
eq_X_add_C_of_degree_eq_one h,

Goal state after:
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
this : (aeval x) (C (minpoly k x).leadingCoeff * X + C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).trace = ((leftMulMatrix b) s).trace

Tactic:
← toMatrix_lmul_eq

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).trace = ((toMatrix b b) (mulLeft R s)).trace
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
⊢ (trace R S) ((trace S T) x) = (trace R T) x

Tactic:
have := Classical.decEq ι
  have := Classical.decEq κ
  cases nonempty_fintype ι
  cases nonempty_fintype κ
  rw [trace_eq_matrix_trace (b.smulTower c), trace_eq_matrix_trace b, trace_eq_matrix_trace c,
    Matrix.trace, Matrix.trace, Matrix.trace, ← Finset.univ_product_univ, Finset.sum_product]
  refine Finset.sum_congr rfl fun i _ ↦ ?_
  simp only [map_sum, smulTower_leftMulMatrix, Finset.sum_apply, Matrix.diag,
    Finset.sum_apply i (Finset.univ : Finset κ) fun y => leftMulMatrix b (leftMulMatrix c x y y)]

Goal state after:
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
q : ℕ
hF : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n y, minpoly F x = X ^ q ^ n - C y

Tactic:
by
  simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one,
    minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : (algebraMap (𝓞 K) K) (Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P) = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0

Tactic:
coe_eq_zero_iff

Goal state after:
K : Type u_1
inst✝ : Field K
x : 𝓞 K
P : Polynomial ℤ
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
⊢ Polynomial.eval₂ (algebraMap ℤ (𝓞 K)) x P = 0
Module: Mathlib.RingTheory.IsGaloisGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
H : Subgroup G
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁷ : CommSemiring A
inst✝⁶ : Semiring C
inst✝⁵ : Algebra A C
inst✝⁴ : MulSemiringAction G C
N : Subgroup G
inst✝³ : CommSemiring B
inst✝² : Algebra B C
inst✝¹ : N.Normal
inst✝ : IsGaloisGroup (↥N) B C
this : (N : Subgroup G) →
  [inst : CommSemiring B] → [inst_1 : Algebra B C] → [N.Normal] → [IsGaloisGroup (↥N) B C] → SMul G B :=
  smulOfNormal G B C
g : G
b : B
c : C
⊢ g • b • c = (g • b) • g • c

Tactic:
by simp [Algebra.smul_def]

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

Goal state before:
pp: case right
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : eval₂ (algebraMap L (AlgebraicClosure F)) y (minpoly L x) = 0
⊢ eval₂ (algebraMap R (AlgebraicClosure F)) y (minpoly R x) = 0

Tactic:
← aeval_def

Goal state after:
case right
R : Type u_1
inst✝⁷ : CommRing R
L : Type u_5
inst✝⁶ : Field L
F : Type u_6
inst✝⁵ : Field F
inst✝⁴ : Algebra R L
inst✝³ : Algebra L F
inst✝² : Algebra R F
inst✝¹ : IsScalarTower R L F
inst✝ : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : (aeval y) (minpoly L x) = 0
⊢ (aeval y) (minpoly R x) = 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
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
⊢ (algebraMap K E) ((Algebra.trace K L) x) = ∑ σ, σ x

Tactic:
let pb := adjoin.powerBasis hx

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ (algebraMap K E) ((Algebra.trace K L) x) = ∑ σ, σ x
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : Infinite G
⊢ finrank K L = 0

Tactic:
contrapose! hG

Goal state after:
case inr
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
hG : finrank K L ≠ 0
⊢ Finite G
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
R : Type u_5
B : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Module.Finite R B
inst✝² : IsDomain B
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G R B
A : Subring B := (algebraMap R B).range
this✝³ : Algebra (FractionRing ↥A) (FractionRing B) := FractionRing.liftAlgebra (↥A) (FractionRing B)
this✝² : MulSemiringAction G (FractionRing B) := IsFractionRing.mulSemiringAction G B (FractionRing B)
this✝¹ : Algebra R ↥A := (algebraMap R B).rangeRestrict.toAlgebra
this✝ : IsScalarTower R (↥A) B
this : Module.Finite (↥A) B
⊢ Finite G

Tactic:
have := IsGaloisGroup.to_isFractionRing_of_isIntegral G A B (FractionRing A) (FractionRing B)

Goal state after:
G : Type u_1
inst✝⁷ : Group G
R : Type u_5
B : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Module.Finite R B
inst✝² : IsDomain B
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G R B
A : Subring B := (algebraMap R B).range
this✝⁴ : Algebra (FractionRing ↥A) (FractionRing B) := FractionRing.liftAlgebra (↥A) (FractionRing B)
this✝³ : MulSemiringAction G (FractionRing B) := IsFractionRing.mulSemiringAction G B (FractionRing B)
this✝² : Algebra R ↥A := (algebraMap R B).rangeRestrict.toAlgebra
this✝¹ : IsScalarTower R (↥A) B
this✝ : Module.Finite (↥A) B
this : IsGaloisGroup G (FractionRing ↥A) (FractionRing B)
⊢ Finite G
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ ∑ x, ↑↑x = if ⊥ = ⊥ then 1 else 0

Tactic:
simp only [univ_unique, sum_singleton, ↓reduceIte, Units.val_eq_one, OneMemClass.coe_eq_one]

Goal state after:
case pos
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Fintype ↥⊥
inst✝ : Decidable (⊥ = ⊥)
⊢ default = 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Fintype.card ↥G
⊢ ∑ x, ↑↑x ^ k = 0

Tactic:
rw [← Nat.card_eq_fintype_card] at k_lt_card_G

Goal state after:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : NoZeroDivisors K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card ↥G
⊢ ∑ x, ↑↑x ^ k = 0
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: a b : ℤ
⊢ a.gcd b = 1 ↔ a.natAbs.gcd b.natAbs = 1

Tactic:
gcd_eq_natAbs

Goal state after:
a b : ℤ
⊢ a.natAbs.gcd b.natAbs = 1 ↔ a.natAbs.gcd b.natAbs = 1
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : ¬φ = 1
⊢ ↑0 = 0

pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(Fintype.card Kˣ) = -1

Tactic:
· exact Nat.cast_zero

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun x ↦ ↑x ^ i, map_one' := ⋯, map_mul' := ⋯ }
this✝ : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h✝ : φ = 1
⊢ ↑(Fintype.card Kˣ) = -1
Module: Mathlib.RingTheory.Int.Basic

Goal state before:
pp: m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs

Tactic:
← hp.dvd_mul,

Goal state after:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ m * n
⊢ p ∣ m.natAbs * n.natAbs
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).prod = ∏ σ, σ pb.gen

Tactic:
@Fintype.prod_equiv (S →ₐ[R] F) _ _ (PowerBasis.AlgHom.fintype pb) _ _ pb.liftEquiv'
    (fun σ => σ pb.gen) (fun x => x) ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ((minpoly R pb.gen).aroots F).prod = ∏ x, ↑x

R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
F : Type u_6
inst✝¹ : Field F
inst✝ : Algebra R F
pb : PowerBasis R S
hE : (Polynomial.map (algebraMap R F) (minpoly R pb.gen)).Splits
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ ∀ (x : S →ₐ[R] F), x pb.gen = ↑(pb.liftEquiv' x)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)

Tactic:
have : a * d - a * d' ∈ P ^ (i + 1) := by
    simp only [← mul_sub]
    exact Ideal.mul_mem_mul a_mem h

Goal state after:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ IsOpen {x}

Tactic:
rw [this, isOpen_compl_iff]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ IsClosed (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ x ∈ f ⁻¹' closedPoints Y

Tactic:
apply isClosed_singleton_of_isLocallyClosed_singleton

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
inst✝ : JacobsonSpace Y
x : X
hx : x ∈ closedPoints X
⊢ IsLocallyClosed {f x}
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case pos
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∈ U j
⊢ IsClosed[instTopologicalSpaceSubtype] {⟨↑y, h⟩}

Tactic:
apply isClosed_singleton_of_isLocallyClosed_singleton

Goal state after:
case pos
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_1
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), JacobsonSpace ↥(U i)
Z : Set X
hZ' : IsLocallyClosed Z
i : ι
x : X
hx : x ∈ Z
hx' : x ∈ ↑(U i)
y : ↥(U i)
hy : y ∈ Subtype.val ⁻¹' Z
hy' : y ∈ closedPoints ↥(U i)
j : ι
h : ↑y ∈ U j
⊢ IsLocallyClosed {⟨↑y, h⟩}
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case h₁
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type w
inst✝³ : CommRing B✝
inst✝² : FormallyUnramified R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type w
inst✝¹ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝ : Algebra R B
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
exact FormallyUnramified.comp_injective I hI

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

Goal state before:
pp: case e_φ₁
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ ((Ideal.Quotient.mkₐ R I).comp f₂).comp ↑e = (Ideal.Quotient.mkₐ R I).comp (f₂.comp ↑e)

Tactic:
AlgHom.comp_assoc

Goal state after:
case e_φ₁
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
e : A ≃ₐ[R] B
C : Type u_3
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] C
e' : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
⊢ (Ideal.Quotient.mkₐ R I).comp (f₂.comp ↑e) = (Ideal.Quotient.mkₐ R I).comp (f₂.comp ↑e)