mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
⊢ m ∈ lieSpan R L s

Tactic:
mem_lieSpan

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
m : M
hm : m ∈ s
⊢ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : IsLieAbelian ↥(lieSpan R L s)
x : L
hx : x ∈ s
y : L
hy : y ∈ s
x' : ↥(lieSpan R L s) := ⟨x, ⋯⟩
y' : ↥(lieSpan R L s) := ⟨y, ⋯⟩
this : ⁅x', y'⁆ = 0
⊢ ⁅x, y⁆ = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : IsLieAbelian ↥(lieSpan R L s)
x : L
hx : x ∈ s
y : L
hy : y ∈ s
x' : ↥(lieSpan R L s) := ⟨x, ⋯⟩
y' : ↥(lieSpan R L s) := ⟨y, ⋯⟩
this : ⁅x', y'⁆ = 0
⊢ ⁅x, y⁆ = 0
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.mem.mem
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u : L
hu : u ∈ s
⊢ ⁅⟨w, ⋯⟩, ⟨u, ⋯⟩⁆ = 0

Tactic:
simpa using

Goal state after:
case refine_2.mem.mem
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y w : L
hw : w ∈ s
u : L
hu : u ∈ s
⊢ ⁅w, u⁆ = 0
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : m ∈ lieSpan R L s
⊢ m ∈ N

Tactic:
mem_lieSpan

Goal state after:
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
N : LieSubmodule R L M
hs : s ⊆ ↑N
m : M
hm : ∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
⊢ m ∈ N
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : I ≤ LieModule.ker R L ↥I
x✝¹ x✝ : ↥I
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ⁅⟨x, hx⟩, ⟨y, hy⟩⁆ = 0

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : I ≤ LieModule.ker R L ↥I
x✝¹ x✝ : ↥I
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ⁅x, ⟨y, hy⟩⁆ = 0
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
⊢ N ≤ maxTrivSubmodule R L M ↔ ⁅⊤, N⁆ = ⊥

Tactic:
refine ⟨fun h => ?_, fun h m hm => ?_⟩
  · rw [← le_bot_iff, ← ideal_oper_maxTrivSubmodule_eq_bot R L M ⊤]
    exact LieSubmodule.mono_lie_right ⊤ h
  · rw [mem_maxTrivSubmodule]
    rw [LieSubmodule.lie_eq_bot_iff] at h
    exact fun x => h x (LieSubmodule.mem_top x) m hm

Goal state after:
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m : M
hm : m ∈ ↑N
N' : Submodule R M
hN' : ∀ p ∈ {x | ∃ s, (∃ x ∈ N, lieSpan R L {x} = s) ∧ ↑s = x}, p ≤ N'
⊢ ∀ m ∈ N, ↑(lieSpan R L {m}) ≤ N'

Tactic:
simpa using

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m : M
hm : m ∈ ↑N
N' : Submodule R M
hN' : ∀ p ∈ {x | ∃ s, (∃ x ∈ N, lieSpan R L {x} = s) ∧ ↑s = x}, p ≤ N'
⊢ ∀ m ∈ N, ↑(lieSpan R L {m}) ≤ N'
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
hf : ⁅x, ↑f⁆ m = 0
⊢ (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆

Tactic:
LieHom.lie_apply,

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x : L
m : M
hf : ⁅x, ↑f m⁆ - ↑f ⁅x, m⁆ = 0
⊢ (↑f).toFun ⁅x, m⁆ = ⁅x, (↑f).toFun m⁆
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ 1 = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
h : minpoly A x = 1
⊢ False
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt✝ : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
lt : i < n
⊢ q.coeff i = coeff 0 i

Tactic:
simpa using

Goal state after:
case inl
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt✝ : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
lt : i < n
⊢ q.coeff i = 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt✝ : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
lt : i < n
⊢ ∑ i, q.coeff ↑i • x ^ ↑i = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
monic : p.Monic
hp0 : (Polynomial.aeval x) p = 0
n : ℕ
hpn : p.degree = ↑n
ind : LinearIndependent A fun i ↦ x ^ ↑i
q : A[X]
lt✝ : q.degree < p.degree
ne : ¬q = 0
hq : (Polynomial.aeval x) (∑ i ∈ Finset.range n, (monomial i) (q.coeff i)) = 0
i : ℕ
lt : i < n
⊢ ∑ x_1, (algebraMap A B) (q.coeff ↑x_1) * x ^ ↑x_1 = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case hp3
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
p : A[X]
hp1 : Irreducible p
hp2 : (Polynomial.aeval x) p = 0
this : p.leadingCoeff ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic

Tactic:
rwa [Polynomial.Monic, leadingCoeff_mul, leadingCoeff_C, mul_inv_cancel₀]

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

Goal state before:
pp: A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ (Polynomial.aeval x) (q.comp (X + C a)) = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
⊢ (Polynomial.aeval (x + (algebraMap A B) a)) q = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
h : IsIntegral A (x + (algebraMap A B) a)
⊢ IsIntegral A x

Tactic:
simpa using

Goal state after:
case neg
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : ¬IsIntegral A x
h : IsIntegral A (x + (algebraMap A B) a)
⊢ IsIntegral A x
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
⊢ minpoly A (x - (algebraMap A B) a) = (minpoly A x).comp (X + C a)

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
⊢ minpoly A (x + -(algebraMap A B) a) = (minpoly A x).comp (X + C a)
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
⊢ (Polynomial.aeval x) ((-1) ^ q.natDegree * q.comp (-X)) = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
q : A[X]
qmo : q.Monic
hq : (Polynomial.aeval (-x)) q = 0
⊢ (Polynomial.aeval (-x)) q = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁹ : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : Ring S
inst✝⁵ : Ring T
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
inst✝¹ : Algebra A T
inst✝ : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp : (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S)
x : S
⊢ (Polynomial.aeval (g x)) (map (↑f) (minpoly R x)) = 0

Tactic:
simpa using

Goal state after:
case refine_2
A : Type u_1
inst✝⁹ : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : Ring S
inst✝⁵ : Ring T
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
inst✝¹ : Algebra A T
inst✝ : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp : (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S)
x : S
⊢ (Polynomial.aeval (g x)) (map (↑f) (minpoly R x)) = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁹ : Field A
R : Type u_3
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : Ring S
inst✝⁵ : Ring T
inst✝⁴ : IsDomain S
inst✝³ : IsDomain T
inst✝² : Algebra R S
inst✝¹ : Algebra A T
inst✝ : Algebra.IsIntegral R S
f : R ≃+* A
g : S ≃+* T
hcomp : (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S)
x : S
⊢ (Polynomial.aeval (g x)) (map (↑f) (minpoly R x)) = 0

Tactic:
simpa using (map_aeval_eq_aeval_map hcomp (minpoly R x) x).symm

Goal state after:
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : ↑U ⊆ (y - x) +ᵥ ↑U
⊢ x - y ∈ U

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : ↑U ⊆ (y - x) +ᵥ ↑U
⊢ x - y ∈ U
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
z : M
hz : z ∈ ↑U
⊢ z ∈ (y - x) +ᵥ ↑U

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
z : M
hz : z ∈ ↑U
⊢ x - y + z ∈ U
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
h : x - y ∈ U
⊢ x +ᵥ ↑U ⊆ y +ᵥ ↑U

Tactic:
rw [Set.vadd_set_subset_iff_subset_neg_vadd_set, vadd_vadd, neg_add_eq_sub]
    intro z hz
    simpa [Set.mem_vadd_set_iff_neg_vadd_mem] using U.add_mem h hz

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
⊢ minpoly A 0 = X

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
⊢ minpoly A 0 = X
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
⊢ minpoly A 1 = X - 1

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
⊢ minpoly A 1 = X + -1
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
⊢ x = 0

Tactic:
simpa using

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
⊢ x = 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x, q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ q = 0

Tactic:
simpa using

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
hσ : IsOfFinOrder σ
q : K[X]
hq : q.Monic
H : q.natDegree < orderOf σ
hs : ∑ x, q.coeff ↑x • (σ ^ ↑x).toLinearMap = 0
⊢ q = 0
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y a✝ b✝ : ↥R[x]
ha✝ : a✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
hb✝ : b✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x) a = ↑a✝
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x) b = ↑b✝
i : ℕ
⊢ (a + b).coeff i ∈ I

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
I : Ideal R
y a✝ b✝ : ↥R[x]
ha✝ : a✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
hb✝ : b✝ ∈ Submodule.span (↥R[x]) (⇑(algebraMap R ↥R[x]) '' ↑I)
a : R[X]
ha : ∀ (i : ℕ), a.coeff i ∈ I
ha' : (aeval x) a = ↑a✝
b : R[X]
hb : ∀ (i : ℕ), b.coeff i ∈ I
hb' : (aeval x) b = ↑b✝
i : ℕ
⊢ a.coeff i + b.coeff i ∈ I
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
hw : z = ⟨x, ⋯⟩ * w
q : R[X]
hq : (aeval x) q = ↑w
⊢ (1 - p - X * q).coeff 0 - 1 ∈ I

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
I : Ideal R
hI : I ≠ ⊤
inst✝ : Invertible x
h : ∃ i ∈ Ideal.map (algebraMap R ↥R[x]) I, ∃ j ∈ Ideal.span {⟨x, ⋯⟩}, i + j = 1
y : ↥R[x]
hy : y ∈ Ideal.map (algebraMap R ↥R[x]) I
z : ↥R[x]
hz : z ∈ Ideal.span {⟨x, ⋯⟩}
eq : y + z = 1
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
hw : z = ⟨x, ⋯⟩ * w
q : R[X]
hq : (aeval x) q = ↑w
⊢ p.coeff 0 ∈ I
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.natDegree < d

Tactic:
simpa using

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.degree < ↑d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.natDegree < d
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.degree < ↑d

Tactic:
simpa using

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.natDegree < d
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
pb : PowerBasis R S
y : S
⊢ y ∈ Submodule.span R (Set.range fun i ↦ pb.gen ^ ↑i)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
pb : PowerBasis R S
y : S
⊢ y ∈ Submodule.span R (Set.range fun i ↦ pb.gen ^ ↑i)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (a.sum fun n a ↦ eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) = 0

Tactic:
refine Finset.sum_eq_zero fun n _ => ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (fun n a ↦ eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) n (a.coeff n) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : m = 0
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : m = 0
⊢ (Quotient.mk I) (a.coeff n) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ∑ x ∈ a.support, eval₂ (C.comp (Ideal.Quotient.mk I)) X ((monomial x) (coeff x a)) = 0

Tactic:
refine Finset.sum_eq_zero fun n _ => ?_

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
⊢ eval₂ (C.comp (Ideal.Quotient.mk I)) X ((monomial n) (coeff n a)) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
⊢ eval₂ (C.comp (Ideal.Quotient.mk I)) X ((monomial n) (coeff n a)) = 0

Tactic:
simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
⊢ (C ((Ideal.Quotient.mk I) (coeff n a)) * n.prod fun n e ↦ X n ^ e) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : coeff n a ∈ I
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0

Tactic:
← @Ideal.mk_ker R _ I,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ a.support
this : coeff n a ∈ RingHom.ker (Ideal.Quotient.mk I)
⊢ C ((Ideal.Quotient.mk I) (coeff n a)) = 0
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : 1 < n
a : K
⊢ X.natDegree < (X ^ n - C a).natDegree

Tactic:
by rwa [natDegree_X_pow_sub_C, natDegree_X]

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
e : n = 0
⊢ Irreducible (C (1 - a))

Tactic:
simpa using

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
e : n = 0
⊢ Irreducible (C (1 - a))
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ q.degree = 0

Tactic:
simpa using

Goal state after:
K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ q.degree = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ 0 = 0 ∧ ∀ (x : R), ¬Irreducible x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ ∀ (x : R), ¬Irreducible x
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), ¬Irreducible x
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ 0

Tactic:
simpa using

Goal state after:
case refine_2.inl
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), ¬Irreducible x
⊢ ∀ (x : R), ¬Irreducible x
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ ¬IsUnit a → emultiplicity a x ≤ 1

Tactic:
intro hu

Goal state after:
case mpr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
⊢ emultiplicity a x ≤ 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hq : ¬IsUnit q
hsep : p.Separable
⊢ emultiplicity q p ≤ 1

Tactic:
contrapose! hq
  apply isUnit_of_self_mul_dvd_separable hsep
  rw [← sq]
  apply pow_dvd_of_le_emultiplicity
  exact Order.add_one_le_of_lt hq

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R
⊢ (X - C x).Separable

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
x : R
⊢ (X + -C x).Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) (a ::ₘ a ::ₘ t)).prod.Separable
⊢ (X - C a) * (X - C a) ∣ (Multiset.map (fun a ↦ X - C a) (a ::ₘ a ::ₘ t)).prod

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) (a ::ₘ a ::ₘ t)).prod.Separable
⊢ (X - C a) * (X - C a) ∣ (X - C a) * ((X - C a) * (Multiset.map (fun a ↦ X - C a) t).prod)