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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I

Tactic:
rw [hI.mem_closure_iff]

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ M.Dep (insert e I) ∨ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X \ M.loops) = M.closure X

Tactic:
rw [← M.closure_union_loops_eq (X \ M.loops), sdiff_union_self, ← closure_empty,
    closure_union_closure_right_eq, union_empty]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.loops ∩ X ∪ X \ M.E = X ∧ (M ↾ X).E = X

Tactic:
inter_eq_self_of_subset_right hX,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ X ∪ X \ M.E = X ∧ (M ↾ X).E = X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
⊢ M.eRk (X ∩ M.E) = M.eRank

Tactic:
inter_eq_self_of_subset_right hX,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.E ⊆ X
⊢ M.eRk M.E = M.eRank
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankPos
B : Set α
hB : M.IsBase B
⊢ 1 ≤ M.eRank

Tactic:
rw [← hB.encard_eq_eRank, one_le_encard_iff_nonempty]

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankPos
B : Set α
hB : M.IsBase B
⊢ B.Nonempty
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
R X I : Set α
hI : M.IsBasis I (X ∩ R ∩ M.E) ∧ X ∩ R ⊆ R
⊢ I.encard = M.eRk (X ∩ R)

Tactic:
rw [← eRk_inter_ground, ← hI.1.eRk_eq_encard]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ M.closure {e} = M.closure {f}

Tactic:
by
  rw [← closure_closure _ {f}, ← insert_eq_of_mem hef, closure_insert_closure_eq_closure_insert,
    ← closure_closure _ {e}, ← insert_eq_of_mem (he.mem_closure_singleton hef),
    closure_insert_closure_eq_closure_insert, pair_comm]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M.eRk X = 0 ↔ X ⊆ M.loops

Tactic:
by
  rw [eRk_eq_zero_iff', inter_eq_self_of_subset_left hX]

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

Goal state before:
pp: α✝ α : 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
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})

Tactic:
rw [spanning_iff_compl_coindep sdiff_subset, ← dual_isLoop_iff_isColoop, ← singleton_dep,
      sdiff_sdiff_cancel_left (by simpa), ← not_indep_iff (by simpa)]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
hXY : M.closure X ⊂ M.closure Y
⊢ ∃ e ∈ Y, e ∉ M.closure X

Tactic:
by
  by_contra! hcon
  exact hXY.not_subset (M.closure_subset_closure_of_subset_closure hcon)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
⊢ M.closure J ∩ I = J

Tactic:
by
  have hJ := hI.subset hJI
  rw [subset_antisymm_iff, and_iff_left (subset_inter (M.subset_closure _) hJI)]
  rintro e ⟨heJ, heI⟩
  exact hJ.isBasis_closure.mem_of_insert_indep heJ (hI.subset (insert_subset heI hJI))

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

Goal state before:
pp: case mpr
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ M.Indep I

Tactic:
convert! hJ.indep

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e})
J : Set α
hJ : M.IsBasis J I
⊢ I = J
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : e ∉ M.closure I
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (X ∩ M.E))

Tactic:
hI.indep.notMem_closure_iff

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (X ∩ M.E))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ Minimal M.Spanning B

Tactic:
rw [minimal_subset_iff]

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Spanning B ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ B → B = t
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case mp
ι : Type u
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : range (w ∘ j) = range w
⊢ Surjective j

Tactic:
range_comp,

Goal state after:
case mp
ι : Type u
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
κ : Type w
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p✝ : IsTranscendenceBasis R (w ∘ j)
p : w '' range j = range w
⊢ Surjective j
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : 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)
⊢ adjoin R (range (Sum.elim y (⇑(algebraMap S A) ∘ x))) = Subalgebra.restrictScalars R Rxy

Tactic:
rw [← adjoin_algebraMap_image_union_eq_adjoin_adjoin, Sum.elim_range, union_comm, range_comp]

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

Goal state before:
pp: case refine_1
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ s

Tactic:
rw [← eq]; exact h.restrictScalars (adjoin R s)

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Subalgebra R A
S : Subalgebra (↥(adjoin R ↑s)) A := algebraicClosure (↥(adjoin R ↑s)) A
hs : ∀ (a : A), IsAlgebraic (↥s) a → a ∈ ↑s
⊢ ↑S = ↑s

Tactic:
refine Set.ext fun a ↦ ⟨(hs _ <| adjoin_eq s ▸ ·), fun h ↦ ?_⟩

Goal state after:
case refine_2
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Subalgebra R A
S : Subalgebra (↥(adjoin R ↑s)) A := algebraicClosure (↥(adjoin R ↑s)) A
hs : ∀ (a : A), IsAlgebraic (↥s) a → a ∈ ↑s
a : A
h : a ∈ ↑s
⊢ a ∈ ↑S
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsDomain A
inst✝ : FaithfulSMul R A
s : Set A
⊢ Algebra.IsAlgebraic (↥(adjoin R s)) A ↔ ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val

Tactic:
← matroid_spanning_iff,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsDomain A
inst✝ : FaithfulSMul R A
s : Set A
⊢ (matroid R A).Spanning s ↔ ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
⊢ trdeg R A ≤ #↑s

Tactic:
← matroid_spanning_iff,

Goal state after:
case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
alg : (matroid R A).Spanning s
⊢ trdeg R A ≤ #↑s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this✝ : Bijective (rangeFactorization x)
this : IsDomain A
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
← matroid_spanning_iff,

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this✝ : Bijective (rangeFactorization x)
this : IsDomain A
alg : (matroid R A).Spanning (range x)
⊢ IsTranscendenceBasis R Subtype.val
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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))

Tactic:
let f (n : ℕ) : Emb F K := IsFractionRing.liftAlgHom
    (g := i1.comp <| MvPolynomial.aeval fun i : ι ↦ MvPolynomial.X i ^ (n + 1)) <| hi1.comp <| by
      simpa [algebraicIndependent_iff_injective_aeval] using
        MvPolynomial.algebraicIndependent_polynomial_aeval_X _
          fun i : ι ↦ (Polynomial.transcendental_X F).pow n.succ_pos

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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree = 0
⊢ f.natSepDegree = 0

Tactic:
by
  linarith only [natSepDegree_le_natDegree f, h]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (0 * g).natSepDegree = natSepDegree 0 + g.natSepDegree ↔ 0 = 0 ∧ g = 0 ∨ IsCoprime 0 g

Tactic:
zero_mul,

Goal state after:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ natSepDegree 0 = natSepDegree 0 + g.natSepDegree ↔ 0 = 0 ∧ g = 0 ∨ IsCoprime 0 g
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
⊢ fixedField ⊥ = ⊤

Tactic:
ext
  simp

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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)

Tactic:
change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _
    exact algHomEquivSigma

Goal state after:
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
H : Subgroup Gal(L/K)
left✝ : H ∈ fixedByFinite K L
⊢ (fun g ↦ g.carrier) H ⊆ (fun x ↦ x⁻¹) ⁻¹' (fun g ↦ g.carrier) H

Tactic:
exact fun _ => H.inv_mem'

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

Goal state before:
pp: case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ a✝ * b✝ ∈ V ^ (k + 1 + l + 1)

Tactic:
rw [add_assoc, pow_add]

Goal state after:
case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a✝ b✝ : G
ha : a✝ ∈ ⋃ n, V ^ (n + 1)
hb : b✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : a✝ ∈ V ^ (k + 1)
l : ℕ
hl : b✝ ∈ V ^ (l + 1)
⊢ a✝ * b✝ ∈ V ^ (k + 1) * V ^ (l + 1)
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K L : IntermediateField F E
inst✝³ : Normal F ↥K
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
x : E
hx₁ : x ∈ K
hx₂ : ⟨x, hx₁⟩ ∈ fixedField (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range
φ : Gal(E/↥L)
⊢ φ x = x

Tactic:
← restrictRestrictAlgEquivMapHom_apply K L φ ⟨x, hx₁⟩

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K L : IntermediateField F E
inst✝³ : Normal F ↥K
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
x : E
hx₁ : x ∈ K
hx₂ : ⟨x, hx₁⟩ ∈ fixedField (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range
φ : Gal(E/↥L)
⊢ ↑(((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ) ⟨x, hx₁⟩) = 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]
⊢ (minpolyDiv R x).natDegree < i + ((minpolyDiv R x).natDegree + 1)

Tactic:
lia

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
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * C r.leadingCoeff = r
⊢ q ∣ p

Tactic:
Monic.leadingCoeff,

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
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * C 1 = r
⊢ q ∣ p

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 q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' * C r.leadingCoeff = r
⊢ r.Monic
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ minpoly R s ≠ 0

Tactic:
· convert! right_ne_zero_of_mul <| hMul ▸ h₀
    refine IsIntegrallyClosed.minpoly.unique ?_ ?_ ?_ |>.symm
    · have := hMul ▸ leadingCoeff_mul .. |>.symm
      simp only [leadingCoeff_C, ne_eq, leadingCoeff_eq_zero, h₀, not_false_eq_true, mul_eq_left₀]
        at this
      exact this
    · have := congrArg (Polynomial.aeval s) hMul
      simp only [hp, h₀, map_mul, aeval_C, zero_eq_mul, FaithfulSMul.algebraMap_eq_zero_iff,
        leadingCoeff_eq_zero, false_or] at this
      exact this
    · exact (hMul ▸ degree_C_mul <| by simp [h₀]) ▸ pmin

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
hdeg : f.degree ≠ 0
hsep : f.Separable
x : k
hx : f.IsRoot x
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
exact ⟨x, by simpa [f] using hx⟩

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
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : (g' * f).content = (b • k).content
h : Associated (g' * f).content (b • k).content
⊢ g ∈ lifts (algebraMap R K)

Tactic:
← C_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
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : (g' * f).content = (b • k).content
h : Associated (g' * f).content (C b * k).content
⊢ g ∈ lifts (algebraMap R K)
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, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

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

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
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
⊢ ∀ {a b : A},
    a ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} →
      b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS} → a + b ∈ {x | ∃ n, x ^ p ^ n ∈ (algebraMap R A).rangeS}

Tactic:
rintro x y ⟨n, hx⟩ ⟨m, hy⟩
    use n + m
    rw [add_pow_expChar_pow, pow_add, pow_mul, mul_comm (_ ^ n), pow_mul]
    exact add_mem (pow_mem hx _) (pow_mem hy _)

Goal state after:
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✝² : MulSemiringAction G B
inst✝¹ : SMulCommClass G A B
H : Subgroup G
inst✝ : H.Normal
g : G
x : ↥(FixedPoints.subring B ↥H)
h : ↥H
⊢ h • g • ↑x = g • ↑x

Tactic:
by
    simpa [mul_smul] using! congr(g • $(x.2 ⟨_, ‹H.Normal›.conj_mem' _ h.2 g⟩))

Goal state after:
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✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
H : Subgroup G
inst✝¹ : H.Normal
inst✝ : Algebra.IsInvariant A B G
x : ↥(FixedPoints.subalgebra A B ↥H)
hx : ∀ (g : G ⧸ H), g • x = x
⊢ ∃ a, (algebraMap A ↥(FixedPoints.subalgebra A B ↥H)) a = x

Tactic:
by
    obtain ⟨y, hy⟩ := Algebra.IsInvariant.isInvariant (A := A) (G := G) x.1
      (fun g ↦ congr_arg Subtype.val (hx g))
    exact ⟨y, Subtype.ext hy⟩

Goal state after:
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
val✝ : Fintype G
b : B
p : A[X]
hp1 : map (algebraMap A B) p = charpoly G b
hp2 : p.Monic
⊢ eval₂ (algebraMap A B) b p = 0

Tactic:
← eval_map,

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
val✝ : Fintype G
b : B
p : A[X]
hp1 : map (algebraMap A B) p = charpoly G b
hp2 : p.Monic
⊢ eval b (map (algebraMap A B) p) = 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
hx : IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x) = -(minpoly K x).nextCoeff

Tactic:
by
  simpa [minpoly_gen K x] using PowerBasis.trace_gen_eq_nextCoeff_minpoly <| adjoin.powerBasis hx

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

Goal state before:
pp: 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
⊢ IsIntegral R (finrank (↥L⟮x⟯) F • ((minpoly L x).aroots (AlgebraicClosure F)).sum)

pp: 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
⊢ (Polynomial.map (algebraMap L (AlgebraicClosure F)) (minpoly L x)).Splits

Tactic:
· refine (IsIntegral.multiset_sum ?_).nsmul _
    intro y hy
    rw [mem_roots_map (minpoly.ne_zero hx')] at hy
    use minpoly R x, minpoly.monic hx
    rw [← aeval_def] at hy ⊢
    exact minpoly.aeval_of_isScalarTower R x y hy

Goal state after:
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
⊢ (Polynomial.map (algebraMap L (AlgebraicClosure F)) (minpoly L x)).Splits