mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
h : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
X : Set α
heX : e ∈ M.closure X
heX' : e ∉ X
C : Set α
hC : M.IsCircuit C
heC : e ∈ C
⊢ False

Tactic:
exact h.1 hC heC

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : M.Dep X
⊢ M.eRk X < X.encard

Tactic:
by
  refine (M.eRk_le_encard X).lt_of_ne ?_
  rw [ne_eq, ← indep_iff_eRk_eq_encard]
  exact hX.not_indep

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ M.closure (insert e (M.closure X)) = M.closure X

Tactic:
insert_eq_of_mem he,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ M.closure X
⊢ M.closure (M.closure X) = M.closure X
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R f

Tactic:
← transcendental_polynomial_aeval_X_iff R i

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R ((Polynomial.aeval (X i)) f)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsBasis ∅ X ↔ X ⊆ M.closure ∅

Tactic:
by
  rw [isBasis_iff_indep_closure, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case neg.inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf : f ∉ M.E
heB : e ∈ B
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
cases hB.indep.notMem_closure_sdiff_of_mem heB (M.closure_subset_closure (by intro; aesop) he)

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
s : Set ι
i : ι
hi : i ∉ s
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 ↦ x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
algebraicIndependent_singleton_iff ⟨i, rfl⟩

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
s : Set ι
i : ι
hi : i ∉ s
⊢ Transcendental (↥(adjoin R (x '' s))) (x ↑⟨i, ⋯⟩) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_1
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i_1 ↦ x ↑i_1) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
algebraicIndependent_singleton_iff ⟨i, rfl⟩

Goal state after:
case e'_1
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s : Set ι
i : ι
⊢ Transcendental (↥(adjoin R (x '' s))) (x ↑⟨i, ⋯⟩) ↔ Transcendental (↥(adjoin R (x '' s))) (x i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.Spanning B

Tactic:
by rwa [h.spanning_iff_spanning]

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ Polynomial.map (↑hx.aevalEquiv) ((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) (X none)) =
    Polynomial.X

Tactic:
aeval_X,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ Polynomial.map (↑hx.aevalEquiv) (none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) = Polynomial.X
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
⊢ Polynomial.map (↑hx.aevalEquiv) ((aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) (X (some i))) =
    Polynomial.C (hx.aevalEquiv (X i))

Tactic:
aeval_X,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
i : ι
⊢ Polynomial.map (↑hx.aevalEquiv) ((some i).elim Polynomial.X fun s ↦ Polynomial.C (X s)) =
    Polynomial.C (hx.aevalEquiv (X i))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2.none
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (Polynomial.aeval a) Polynomial.X = (aeval fun o ↦ o.elim a x) (X none)

Tactic:
aeval_X,

Goal state after:
case refine_2.none
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (Polynomial.aeval a) Polynomial.X = none.elim a x
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (aeval x) (X i) = (aeval fun o ↦ o.elim a x) (X (some i))

Tactic:
aeval_X,

Goal state after:
case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ x i = (aeval fun o ↦ o.elim a x) (X (some i))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ x i = (aeval fun o ↦ o.elim a x) (X (some i))

Tactic:
aeval_X,

Goal state after:
case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ x i = (some i).elim a x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: 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✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{max w v, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s } =
    lift.{w, max v w} (lift.{v, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s })

Tactic:
lift_add,

Goal state after:
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✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{max w v, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s } =
    lift.{w, max v w} (lift.{v, w} #{ x // x ∈ t }) + lift.{w, max v w} (lift.{w, v} #{ x // x ∈ s })
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ (𝓝 1).HasBasis (fun V ↦ V ∈ B) id

Tactic:
B.nhds_one_eq

Goal state after:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.filter.HasBasis (fun V ↦ V ∈ B) id
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case e'_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (∃ n x_1, (algebraMap F E) x_1 = x ^ q ^ n) ↔ ∃ n y, (Polynomial.aeval x) X ^ q ^ n - (algebraMap F E) y = 0

Tactic:
aeval_X,

Goal state after:
case e'_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
⊢ (∃ n x_1, (algebraMap F E) x_1 = x ^ q ^ n) ↔ ∃ n y, x ^ q ^ n - (algebraMap F E) y = 0
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case right
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
x : R
⊢ (fun x1 x2 ↦ x1 • x2) x 0 ∈ {0}

Tactic:
simp only [smul_zero, mem_singleton_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : DiscreteTopology R
⊢ ∀ (x₀ : R) {U : Set M},
    U ∈
        (have this := default;
          this).sets →
      ∃
        V ∈
          (have this := default;
            this).sets,
        V ⊆ (fun x ↦ x₀ • x) ⁻¹' U

Tactic:
rintro x₀ U (h : U ∈ {{(0 : M)}})
        rw [mem_singleton_iff] at h
        use {0}, rfl
        simp [h]

Goal state after:
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✝
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : IntermediateField K L
inst✝¹ : IsGalois K L
inst✝ : IsGalois K ↥E
σ : Gal(L/K)
⊢ MulAut.conj σ • E.fixingSubgroup = E.fixingSubgroup

Tactic:
← map_fixingSubgroup,

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✝
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : IntermediateField K L
inst✝¹ : IsGalois K L
inst✝ : IsGalois K ↥E
σ : Gal(L/K)
⊢ (map (↑σ) E).fixingSubgroup = E.fixingSubgroup
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (Polynomial.aeval x) X ^ q ^ n - (Polynomial.aeval x) (C y) = 0
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
aeval_X,

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : x ^ q ^ n - (Polynomial.aeval x) (C y) = 0
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ (algebraMap F E) (-(minpoly F x).coeff 0) = x ^ q ^ n

Tactic:
by rw [map_neg, h, neg_mul, one_mul, neg_neg]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F E < finrank F ↥F⟮x⟯ * finrank (↥F⟮x⟯) E
⊢ False

Tactic:
Module.finrank_mul_finrank F F⟮x⟯ E

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
heq : finSepDegree F E = finrank F E
x : E
halg : IsAlgebraic F x
h : finSepDegree F ↥F⟮x⟯ < finrank F ↥F⟮x⟯
this : finSepDegree F E < finrank F E
⊢ False
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_2
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).Monic

pp: case refine_3
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

pp: case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

Tactic:
· simpa [monic_scaleRoots_iff] using minpoly.monic
      (hs.map (IsScalarTower.toAlgHom R S L)).tower_top

Goal state after:
case refine_3
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)
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
x : k
hx : eval x (p * C p.leadingCoeff⁻¹) = 0
⊢ eval x p = 0

Tactic:
by simpa [hp.ne_zero] using hx

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) X + (aeval x) (C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
aeval_X,

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 : x + (aeval x) (C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
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✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ g₁ • (algebraMap B C) x = g₂ • (algebraMap B C) x

Tactic:
smul_eq_iff_eq_inv_smul,

Goal state after:
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✝² : FaithfulSMul B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
q : G ⧸ N
x : B
g₁ g₂ : G
h : (QuotientGroup.leftRel N) g₁ g₂
⊢ (algebraMap B C) x = g₁⁻¹ • g₂ • (algebraMap B C) x
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ e ((trace A C) x) = (trace B C) x

Tactic:
rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]

Goal state after:
case pos
A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ e ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x).trace = ((leftMulMatrix b) x).trace
Module: Mathlib.Data.ZMod.ValMinAbs

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

Tactic:
split_ifs <;> simp [add_zero, sub_add_cancel]

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

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : (frobenius K p ^ n) x = x ^ p ^ n
⊢ (frobenius K p * frobenius K p ^ n) x = (x ^ p ^ n) ^ p

Tactic:
RingHom.mul_def,

Goal state after:
case succ
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
hn : (frobenius K p ^ n) x = x ^ p ^ n
⊢ ((frobenius K p).comp (frobenius K p ^ n)) x = (x ^ p ^ n) ^ p
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Group G
inst✝¹⁵ : Finite G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹² : Q.IsPrime
inst✝¹¹ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra (A ⧸ P) K
inst✝⁷ : Algebra (B ⧸ Q) L
inst✝⁶ : Algebra (A ⧸ P) L
inst✝⁵ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower (A ⧸ P) K L
inst✝² : Algebra.IsInvariant A B G
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
f : Gal(L/K)
x : L
hx : ∀ (g : ↥(MulAction.stabilizer G Q)), ((IsFractionRing.stabilizerHom G P Q K L) g) x = x
⊢ f x = x

Tactic:
obtain ⟨_⟩ := nonempty_fintype G
  have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A Q
  have : Algebra.IsIntegral A B := Algebra.IsInvariant.isIntegral A B G
  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (B ⧸ Q) x
  obtain ⟨b, a, ha, h⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A ⧸ P) y).exists_smul_eq_mul x hy
  replace ha : algebraMap (A ⧸ P) L a ≠ 0 := by
    rwa [Ne, algebraMap_apply (A ⧸ P) K L, algebraMap_eq_zero_iff, algebraMap_eq_zero_iff]
  replace hy : algebraMap (B ⧸ Q) L y ≠ 0 :=
    mt (algebraMap_eq_zero_iff (B ⧸ Q) L).mp (nonZeroDivisors.ne_zero hy)
  replace h : algebraMap (B ⧸ Q) L x / algebraMap (B ⧸ Q) L y =
      algebraMap (B ⧸ Q) L b / algebraMap (A ⧸ P) L a := by
    rw [mul_comm, Algebra.smul_def, mul_comm] at h
    rw [div_eq_div_iff hy ha, ← map_mul, ← h, map_mul, ← algebraMap_apply]
  simp only [h, map_div₀, algebraMap_apply (A ⧸ P) K L, AlgEquiv.commutes] at hx ⊢
  simp only [← algebraMap_apply, div_left_inj' ha] at hx ⊢
  exact fixed_of_fixed1 G P Q K L f b (fun g ↦ IsFractionRing.injective (B ⧸ Q) L
    ((IsFractionRing.fieldEquivOfAlgEquiv_algebraMap K L L
      (Ideal.Quotient.stabilizerHom Q P G g) b).symm.trans (hx g)))

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

Goal state before:
pp: case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
this : NeZero n
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
obtain ⟨a, rfl⟩ := ZMod.natCast_zmod_surjective a

Goal state after:
case inr.inr
n p k : ℕ
inst✝ : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf ↑a).Coprime n
ha0 : ↑a ≠ 0
⊢ ↑a = 1 ∨ IsUnit (↑a - 1)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
k : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u_4
inst✝¹⁰ : Finite G
inst✝⁹ : Group G
inst✝⁸ : MulSemiringAction G B
inst✝⁷ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝⁶ : Q.LiesOver P
inst✝⁵ : CommRing k
inst✝⁴ : Algebra (A ⧸ P) k
inst✝³ : Algebra (B ⧸ Q) k
inst✝² : IsScalarTower (A ⧸ P) (B ⧸ Q) k
inst✝¹ : IsDomain k
inst✝ : FaithfulSMul (B ⧸ Q) k
σ : k ≃ₐ[A ⧸ P] k
f : B ⧸ Q →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom (A ⧸ P) (B ⧸ Q) k
hf : Function.Injective ⇑f
τ₁ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₁ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₁ x) = σ ((algebraMap (B ⧸ Q) k) x)
τ₂ : B ⧸ Q →ₐ[A ⧸ P] B ⧸ Q
h₂ : ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ₂ x) = σ.symm ((algebraMap (B ⧸ Q) k) x)
x y : B
e : (mk Q) y = τ₁ ((mk Q) x)
⊢ (algebraMap (B ⧸ Q) k) (τ₂ (τ₁ ((mk Q) x))) = σ.symm (σ ((algebraMap (B ⧸ Q) k) ((mk Q) x)))

Tactic:
rw [← h₁, ← e, h₂]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ ↑(absNorm I) ∣ (Algebra.norm ℤ) x

Tactic:
rw [← Int.dvd_natAbs, ← absNorm_span_singleton x, Int.natCast_dvd_natCast]
  exact absNorm_dvd_absNorm_of_le ((span_singleton_le_iff_mem _).mpr h)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n

Tactic:
have : IsAddTorsionFree S := .of_isTorsionFree ℤ _

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this : IsAddTorsionFree S
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n