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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective ⇑f
x : L
m : M
hm : m ∈ N
⊢ (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⁅x, ⟨m, hm⟩⁆ =
    ⁅x, (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⟨m, hm⟩⁆

Tactic:
;

Goal state after:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective ⇑f
x : L
m : M
hm : m ∈ N
⊢ (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⁅x, ⟨m, hm⟩⁆ =
    ⁅x, (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⟨m, hm⟩⁆
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective ⇑f
x : L
m : M
hm : m ∈ N
⊢ ↑((↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⁅x, ⟨m, hm⟩⁆) =
    ↑⁅x, (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⟨m, hm⟩⁆

Tactic:
;

Goal state after:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective ⇑f
x : L
m : M
hm : m ∈ N
⊢ ↑((↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⁅x, ⟨m, hm⟩⁆) =
    ↑⁅x, (↑(Submodule.equivMapOfInjective (↑f) hf ↑N)).toFun ⟨m, hm⟩⁆
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
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥

Tactic:
;

Goal state after:
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
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥
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
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : 0 = m
⊢ m ∈ ↑⊥

Tactic:
;

Goal state after:
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
N : LieSubmodule R L M
I : LieIdeal R L
inst✝ : LieModule.IsTrivial L M
m : M
x : ↥I
n : ↥N
h : 0 = m
⊢ m ∈ ↑⊥
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N✝ N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ comap e.toLieModuleHom (map e.toLieModuleHom N) ↔ m✝ ∈ N

Tactic:
;

Goal state after:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N✝ N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ comap e.toLieModuleHom (map e.toLieModuleHom N) ↔ m✝ ∈ N
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N✝ N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M'
m✝ : M'
⊢ m✝ ∈ map e.toLieModuleHom (comap e.toLieModuleHom N) ↔ m✝ ∈ N

Tactic:
;

Goal state after:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N✝ N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M'
m✝ : M'
⊢ m✝ ∈ map e.toLieModuleHom (comap e.toLieModuleHom N) ↔ m✝ ∈ N
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
hm : m ∈ f.ker
⊢ (f.comp f.ker.incl) ⟨m, hm⟩ = 0 ⟨m, hm⟩

Tactic:
;

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
hm : m ∈ f.ker
⊢ (f.comp f.ker.incl) ⟨m, hm⟩ = 0 ⟨m, hm⟩
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m✝ : N
⊢ m✝ ∈ LieSubmodule.map f ⊤ ↔ m✝ ∈ f.range

Tactic:
;

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m✝ : N
⊢ m✝ ∈ LieSubmodule.map f ⊤ ↔ m✝ ∈ f.range
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f✝ : M →ₗ⁅R,L⁆ N
P : LieSubmodule R L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), f m ∈ P
x : L
m : M
⊢ ↑((LinearMap.codRestrict (↑P) (↑f) h) ⁅x, m⁆) = ↑⁅x, (LinearMap.codRestrict (↑P) (↑f) h) m⁆

Tactic:
;

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f✝ : M →ₗ⁅R,L⁆ N
P : LieSubmodule R L N
f : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), f m ∈ P
x : L
m : M
⊢ ↑((LinearMap.codRestrict (↑P) (↑f) h) ⁅x, m⁆) = ↑⁅x, (LinearMap.codRestrict (↑P) (↑f) h) m⁆
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆ ∧ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m

Tactic:
;

Goal state after:
case h
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆ ∧ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m
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
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
m✝ : M
⊢ m✝ ∈ map (N.incl.restrictLie H) ⊤ ↔ m✝ ∈ N.restr H

Tactic:
;

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
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
m✝ : M
⊢ m✝ ∈ map (N.incl.restrictLie H) ⊤ ↔ m✝ ∈ N.restr H
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]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).degree ≤
    p.degree

Tactic:
;

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]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 ↦ x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).degree ≤
    p.degree
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
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
⊢ minpoly A x = p

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
pmin : ∀ (q : A[X]), q.Monic → (Polynomial.aeval x) q = 0 → p.degree ≤ q.degree
hx : IsIntegral A x
⊢ minpoly A x = p
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆

pp: case h.right
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m

Tactic:
;

Goal state after:
case h.left
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ ∈ ⁅I, N⁆

case h.right
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ∃ z ∈ ⁅J, N⁆, ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + z = m
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₂, hx₂⟩, ↑n⁆ ∈ ⁅J, N⁆ ∧ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + ⁅↑⟨x₂, hx₂⟩, ↑n⁆ = m

Tactic:
;

Goal state after:
case h
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₂, hx₂⟩, ↑n⁆ ∈ ⁅J, N⁆ ∧ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + ⁅↑⟨x₂, hx₂⟩, ↑n⁆ = m
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
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) (p ^ n) = 0
⊢ (Polynomial.aeval x) p = 0

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) (p ^ n) = 0
⊢ (Polynomial.aeval x) p = 0
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
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) p ^ n = 0
⊢ (Polynomial.aeval x) p = 0

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) p ^ n = 0
⊢ (Polynomial.aeval x) p = 0
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case h.left
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₂, hx₂⟩, ↑n⁆ ∈ ⁅J, N⁆

pp: case h.right
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + ⁅↑⟨x₂, hx₂⟩, ↑n⁆ = m

Tactic:
;

Goal state after:
case h.left
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₂, hx₂⟩, ↑n⁆ ∈ ⁅J, N⁆

case h.right
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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
h✝ : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
m : M
x : L
hx : x ∈ I ⊔ J
n : ↥N
h : ⁅↑⟨x, hx⟩, ↑n⁆ = m
x₁ : L
hx₁ : x₁ ∈ I
x₂ : L
hx₂ : x₂ ∈ J
hx' : x₁ + x₂ = x
⊢ ⁅↑⟨x₁, hx₁⟩, ↑n⁆ + ⁅↑⟨x₂, hx₂⟩, ↑n⁆ = m
Module: Mathlib.Algebra.Lie.IdealOperations

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 N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆

Tactic:
;

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 N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
Module: Mathlib.Algebra.Lie.IdealOperations

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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆

Tactic:
;

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
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos.refine_2
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
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : ↑(minpoly A x).natDegree ≤ (q.comp (X + C a)).degree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree

Tactic:
degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero,

Goal state after:
case pos.refine_2
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
this : (Polynomial.aeval x) (q.comp (X + C a)) = 0
H : ↑(minpoly A x).natDegree ≤ ↑(q.comp (X + C a)).natDegree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
;

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
;

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: 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 σ
⊢ orderOf σ = orderOf hσ.unit

pp: case hf
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 σ
⊢ Injective ⇑↑(AlgEquiv.algHomUnitsEquiv K L)

Tactic:
← orderOf_units,

Goal state after:
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 σ
⊢ orderOf σ = orderOf ↑hσ.unit

case hf
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 σ
⊢ Injective ⇑↑(AlgEquiv.algHomUnitsEquiv K L)
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
⊢ RingHom.ker (evalRingHom x) = Ideal.span {X - C x}

Tactic:
ext y
  simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]

Goal state after:
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 : ↥R[x]
a : R
ha : a ∈ ↑I
i : ℕ
⊢ (if i = 0 then a else 0) ∈ I

Tactic:
;

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 : ↥R[x]
a : R
ha : a ∈ ↑I
i : ℕ
⊢ (if i = 0 then a else 0) ∈ I
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: case h
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, ⋯⟩}
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
q : R[X]
hq : (aeval x) q = ↑w
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : ↑y + ↑z = 1
hw : ↑z = ↑(⟨x, ⋯⟩ * w)
⊢ (1 - p - X * q).trailingCoeff - 1 ∈ I ∧ (aeval ⅟x) (1 - p - X * q).reverse = 0

Tactic:
trailingCoeff_eq_coeff_zero

Goal state after:
case h
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, ⋯⟩}
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
q : R[X]
hq : (aeval x) q = ↑w
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : ↑y + ↑z = 1
hw : ↑z = ↑(⟨x, ⋯⟩ * w)
⊢ (1 - p - X * q).coeff 0 - 1 ∈ I ∧ (aeval ⅟x) (1 - p - X * q).reverse = 0

case h
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, ⋯⟩}
p : R[X]
hp : (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y
w : ↥R[x]
q : R[X]
hq : (aeval x) q = ↑w
this : (1 - p - X * q).coeff 0 - 1 ∈ I
eq : ↑y + ↑z = 1
hw : ↑z = ↑(⟨x, ⋯⟩ * w)
⊢ (1 - p - X * q).coeff 0 ≠ 0
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
pb : PowerBasis R S
y : S
⊢ ∃ f, y = (aeval pb.gen) f

Tactic:
nontriviality S
  obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y
  exact ⟨f, hf⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {↑(quotientSpanXSubCAlgEquiv y) ((Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (C x))} = Ideal.span {x}

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {↑(quotientSpanXSubCAlgEquiv y) ((Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (C x))} = Ideal.span {x}
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
⊢ ↑(quotientSpanXSubCAlgEquiv y) ((Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (C x)) = x

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ ↑(quotientSpanXSubCAlgEquiv y) ((Ideal.Quotient.mkₐ R (Ideal.span {X - C y})) (C x)) = x