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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ M.Indep {e} ∧ e ∈ R ↔ M.IsNonloop e ∧ e ∈ R

Tactic:
indep_singleton

Goal state after:
α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ M.IsNonloop e ∧ e ∈ R ↔ M.IsNonloop e ∧ e ∈ R
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
⊢ M.closure X = M.closure Y

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X
  obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)
  rw [hI.eRk_eq_encard, hJ.eRk_eq_encard] at hr
  rw [← closure_inter_ground, ← M.closure_inter_ground Y,
    ← hI.isBasis_inter_ground.closure_eq_closure,
    ← hJ.isBasis_inter_ground.closure_eq_closure, Finite.eq_of_subset_of_encard_le
      (hI.indep.finite_of_subset_isRkFinite hI.subset hX) hIJ hr]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
⊢ M.closure univ = M.E

Tactic:
rw [← closure_inter_ground, univ_inter, closure_ground]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.removeLoops = M
⊢ M.Loopless

Tactic:
rw [← h]

Goal state after:
α : Type u_1
M : Matroid α
h : M.removeLoops = M
⊢ M.removeLoops.Loopless
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

Tactic:
refine ⟨I₀, hI₀ss.trans inter_subset_right, ?_, hbij.injOn⟩

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ f '' I₀ = I
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
s : Set ι
i : ι
hs : AlgebraicIndepOn R x s
hi : Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ AlgebraicIndepOn R x (insert i s)

Tactic:
by
  nontriviality R
  have := hs.algebraMap_injective.nontrivial
  exact (insert_iff fun h ↦ hi <| isAlgebraic_algebraMap
    (⟨_, subset_adjoin ⟨i, h, rfl⟩⟩ : adjoin R (x '' s))).mpr ⟨hs, hi⟩

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
have : aeval (Sum.elim y x) = ((aeval y).restrictScalars R).comp e.toAlgHom := by
    ext (_ | _) <;> simp [e]

Goal state after:
case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (I ∪ J) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
union_comm I J,

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (J ∪ I) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : (MvPolynomial.map ↑f) p = 0
⊢ p = 0

Tactic:
exact map_injective (f : R →+* S) hf (by rwa [map_zero])

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

Goal state before:
pp: ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E

Tactic:
have := hx.isAlgebraic
  set S := range x
  let : Algebra (adjoin F S) (IntermediateField.adjoin F S) :=
    (Subalgebra.inclusion (IntermediateField.algebra_adjoin_le_adjoin F S)).toRingHom.toAlgebra
  have : IsScalarTower (adjoin F S) (IntermediateField.adjoin F S) E :=
    IsScalarTower.of_algebraMap_eq (congrFun rfl)
  exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ rootOfSplits ⋯ ⋯ ∈ f.aroots f.SplittingField

Tactic:
mem_aroots

Goal state after:
case h
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ f ≠ 0 ∧ (aeval (rootOfSplits ⋯ ⋯)) f = 0
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (∀ a ∈ f.aroots (AlgebraicClosure F), ∀ b ∈ g.aroots (AlgebraicClosure F), a ≠ b) ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
mem_aroots

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.FieldTheory.SeparableClosure

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

Tactic:
IntermediateField.rank_top'

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ Module.rank F E = Module.rank F E
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case inv
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : S ∈ 𝓝 1
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst✝³] U
onememU : 1 ∈ U
⊢ (U ∩ U⁻¹)⁻¹ = U ∩ U⁻¹

Tactic:
simp [inter_comm]

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
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
hsep : IsSeparable E x
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
⊢ IsSeparable F x

Tactic:
have hx : x ∈ E'⟮x⟯.restrictScalars F := mem_adjoin_simple_self _ x

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
hsep : IsSeparable E x
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⟯
⊢ 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
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 : w1 = f⁻¹ * g * w2
⊢ False

Tactic:
mul_inv_eq_iff_eq_mul.symm

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 : w1 * w2⁻¹ = f⁻¹ * g
⊢ False
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Submodule.span R (Set.range (minpolyDiv R x).coeff) ≤ Subalgebra.toSubmodule R[x]

pp: case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Subalgebra.toSubmodule R[x] ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)

Tactic:
· rw [Submodule.span_le]
    rintro _ ⟨i, rfl⟩
    apply coeff_minpolyDiv_mem_adjoin

Goal state after:
case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Subalgebra.toSubmodule R[x] ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)
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ᶜ
⊢ False

Tactic:
have fix : ∀ x ∈ IntermediateField.fixedField H.toSubgroup ⊓ ↑L', σ x = x :=
    fun x hx ↦ ((mem_fixingSubgroup_iff Gal(K/k)).mp hσ) x hx.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 ∈ fixedField ↑H ⊓ L'.toIntermediateField, σ x = x
⊢ False
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
x : S
hx : IsIntegral R x
⊢ Injective ⇑(Minpoly.toAdjoin R x)

Tactic:
refine (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => ?_

Goal state after:
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
x : S
hx : IsIntegral R x
P₁ : AdjoinRoot (minpoly R x)
hP₁ : (Minpoly.toAdjoin R x) P₁ = 0
⊢ P₁ = 0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑x.val * 2 ≤ ↑n
⊢ 0 ≤ ↑x.val * 2

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
⊢ x.valMinAbs = y → x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
by rintro rfl; exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩

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

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Tactic:
rw [← h]

Goal state after:
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ x.valMinAbs * 2 ≤ ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ (-a).valMinAbs = -a.valMinAbs

Tactic:
refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩

Goal state after:
case inr.refine_1
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a = ↑(-a.valMinAbs)

case inr.refine_2
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -↑n < -a.valMinAbs * 2

case inr.refine_3
n : ℕ
a : ZMod n
ha : 2 * a.val ≠ n
h : NeZero n
⊢ -a.valMinAbs * 2 ≤ ↑n
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
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))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ eval b (∑ x ∈ Finset.range k, (monomial x) (f.coeff (x + 1 + j)) * X) ∈ g • Q

Tactic:
← Finset.sum_mul,

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
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))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ eval b ((∑ i ∈ Finset.range k, (monomial i) (f.coeff (i + 1 + j))) * X) ∈ g • Q
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
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ 0 < p ^ (n + 1)

Tactic:
positivity

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

Goal state before:
pp: case neg.succ.hnc
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
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this✝ : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
this : g.natDegree ≠ 0
⊢ g.natDegree * p ^ (n + 1) ≠ 0

Tactic:
positivity

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

Goal state before:
pp: K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
this : ∏ x ∈ univ.erase (-1), x = 1
⊢ ∏ x, x = -1

Tactic:
rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (notMem_erase _ _), this, mul_one]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹² : Group G
inst✝¹¹ : Group G'
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : IsDomain B
inst✝⁷ : Algebra A B
inst✝⁶ : FaithfulSMul A B
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction G' B
inst✝³ : IsGaloisGroup G A B
inst✝² : IsGaloisGroup G' A B
inst✝¹ : Finite G
inst✝ : Finite G'
g : G'
x : B
⊢ (mulEquivCongr G G' A B) ((mulEquivCongr G G' A B).symm g) • x = g • x

Tactic:
MulEquiv.apply_symm_apply

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹² : Group G
inst✝¹¹ : Group G'
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : IsDomain B
inst✝⁷ : Algebra A B
inst✝⁶ : FaithfulSMul A B
inst✝⁵ : MulSemiringAction G B
inst✝⁴ : MulSemiringAction G' B
inst✝³ : IsGaloisGroup G A B
inst✝² : IsGaloisGroup G' A B
inst✝¹ : Finite G
inst✝ : Finite G'
g : G'
x : B
⊢ g • x = g • x
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: 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
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
⊢ FixedPoints.intermediateField ↥H = F

Tactic:
by
  refine IntermediateField.ext_iff.mpr fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
  · obtain ⟨a, rfl⟩ := hHFL.isInvariant.isInvariant x hx
    exact a.prop
  · have := congr_arg (restrictScalars K) <| IsGaloisGroup.fixedPoints_eq_bot H F L
    rw [restrictScalars_bot_eq_self] at this
    rwa [← this] at hx

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

Goal state before:
pp: K : Type u_1
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : DivisionRing K
inst✝ : CharP K p
⊢ (castHom ⋯ K).fieldRange = ⊥

Tactic:
rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
p : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (∏ p ∈ insert p f', p ^ i p)

Tactic:
Finset.prod_insert hpf'

Goal state after:
case insert
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
i : α → ℕ
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
p : α
f' : Finset α
hpf' : p ∉ f'
ih : (∀ p ∈ f', Prime p) → (∀ p ∈ f', ∀ q ∈ f', p ∣ q → p = q) → P (∏ p ∈ f', p ^ i p)
is_prime : ∀ p_1 ∈ insert p f', Prime p_1
is_coprime : ∀ p_1 ∈ insert p f', ∀ q ∈ insert p f', p_1 ∣ q → p_1 = q
⊢ P (p ^ i p * ∏ x ∈ f', x ^ i x)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
⊢ P a

Tactic:
let := Classical.decEq α
  have P_of_associated : ∀ {x y}, Associated x y → P x → P y := by
    rintro x y ⟨u, rfl⟩ hx
    exact hcp (fun p _ hpx => isUnit_of_dvd_unit hpx u.isUnit) hx (h1 u.isUnit)
  by_cases ha0 : a = 0
  · rwa [ha0]
  have : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
  let : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
  refine P_of_associated (prod_normalizedFactors ha0) ?_
  rw [← (normalizedFactors a).map_id, Finset.prod_multiset_map_count]
  refine induction_on_prime_power _ _ ?_ ?_ @h1 @hpr @hcp <;> simp only [Multiset.mem_toFinset]
  · apply prime_of_normalized_factor
  · apply normalizedFactors_eq_of_dvd

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
⊢ comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p

Tactic:
rw [← comap_coe e, comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]

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
I : Ideal S
⊢ absNorm I = 1 ↔ I = ⊤

Tactic:
by
  rw [absNorm_apply, cardQuot_eq_one_iff]

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

Goal state before:
pp: case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P)
this : P.IsMaximal
⊢ span {p} ≤ under ℤ P

Tactic:
obtain ⟨q, n, hn, hqP, hq, H⟩ := Ideal.exists_prime_and_absNorm_eq_pow P

Goal state after:
case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
hI : p ∣ ↑(absNorm P)
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
⊢ span {p} ≤ under ℤ P
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑(Subalgebra.toSubmodule (Algebra.adjoin R ↑s))

Tactic:
rw [Algebra.adjoin_eq_span, hs, span_invSubmonoid]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : Monoid.FG ↥M
s : Finset S
hs : Submonoid.closure ↑s = invSubmonoid M S
x : S
⊢ x ∈ ↑⊤