mathlib-initiative/mathlib-tactics huggingface dataset:
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 : M →ₗ⁅R,L⁆ N
x : L
⊢ ⁅x, ↑F⁆ = 0

Tactic:
ext

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 : M →ₗ⁅R,L⁆ N
x : L
x✝ : M
⊢ ⁅x, ↑F⁆ x✝ = 0 x✝
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
⊢ map LieModuleHom.id N = N

Tactic:
ext

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
⊢ m✝ ∈ map LieModuleHom.id N ↔ 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))
⊢ ⇑(maxTrivLinearMapEquivLieModuleHom f) = ⇑↑f

Tactic:
ext

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✝ : M
⊢ (maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑f x✝
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))
⊢ ↑(maxTrivLinearMapEquivLieModuleHom f) = ↑f

Tactic:
ext

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✝ : M
⊢ ↑(maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑f x✝
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, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆

Tactic:
constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_right]

Goal state after:
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:
ext

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'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M
⊢ comap e.toLieModuleHom (map e.toLieModuleHom N) = N

Tactic:
ext

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'
⊢ map e.toLieModuleHom (comap e.toLieModuleHom N) = N

Tactic:
ext

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
⊢ LieSubmodule.map f ⊤ = f.range

Tactic:
ext

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:
ext

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.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
⊢ map (N.incl.restrictLie H) ⊤ = N.restr H

Tactic:
ext

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.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:
constructor

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:
constructor

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:
constructor

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

case 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 N' : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅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:
constructor

Goal state after:
case 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
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆

case 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
⊢ ⁅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).degree ≤ (q.comp (X + C a)).degree
⊢ ((minpoly A x).comp (X - C a)).degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree qmo.ne_zero,
        degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
        natDegree_X_sub_C, mul_one]

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).degree ≤ (q.comp (X + C a)).degree
⊢ ↑(minpoly A x).natDegree ≤ ↑q.natDegree
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case cons
R : Type u_1
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
ι : Type u_6
x y : ι → M
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD U]) → ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD U]
⊢ ∑ i ∈ Finset.cons i s h✝, x i ≡ ∑ i ∈ Finset.cons i s h✝, y i [SMOD U]

Tactic:
| cons i s _ ih =>

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

Goal state before:
pp: case e_p
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ (fun x ↦ ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x) = fun x ↦ ∃ a ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, ↑f a = x

Tactic:
ext

Goal state after:
case e_p
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
x✝ : L'
⊢ (∃ x n, ⁅↑x, ↑n⁆ = x✝) ↔ ∃ a ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, ↑f a = x✝
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: case cons
A : Type u_3
inst✝ : CommRing A
I : Ideal A
ι : Type u_6
x y : ι → A
i : ι
s : Finset ι
h✝ : i ∉ s
ih : (∀ i ∈ s, x i ≡ y i [SMOD I]) → ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]
hxy : ∀ i_1 ∈ Finset.cons i s h✝, x i_1 ≡ y i_1 [SMOD I]
⊢ ∏ i ∈ Finset.cons i s h✝, x i ≡ ∏ i ∈ Finset.cons i s h✝, y i [SMOD I]

Tactic:
| cons i s _ ih =>

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

Goal state before:
pp: case refine_3
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
⊢ (map (↑f) (minpoly R x)).Monic

Tactic:
exact (monic (Algebra.IsIntegral.isIntegral x)).map _

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✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (minpoly A x).coeff 0 = 0 ↔ x = 0

Tactic:
constructor

Goal state after:
case mp
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
⊢ (minpoly A x).coeff 0 = 0 → x = 0

case mpr
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
⊢ x = 0 → (minpoly A x).coeff 0 = 0
Module: Mathlib.RingTheory.Polynomial.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ (∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P) ↔ eval a (eval b P) = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ (∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P) → eval a (eval b P) = 0

case mpr
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ eval a (eval b P) = 0 → ∃ a_2 b_1, a_2 * C (X - C a) + b_1 * (X - C b) = P
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]
⊢ y ∈ Ideal.map (algebraMap R ↥R[x]) I ↔ ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

Tactic:
constructor

Goal state after:
case mp
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]
⊢ y ∈ Ideal.map (algebraMap R ↥R[x]) I → ∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y

case mpr
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]
⊢ (∃ p, (∀ (i : ℕ), p.coeff i ∈ I) ∧ (aeval x) p = ↑y) → y ∈ Ideal.map (algebraMap R ↥R[x]) 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 σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ σ.toLinearMap = ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap

Tactic:
ext

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 σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
x✝ : L
⊢ σ.toLinearMap x✝ = ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap x✝
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
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, f.degree < ↑d ∧ y = (aeval x) f) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f

Tactic:
constructor

Goal state after:
case mp
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, f.degree < ↑d ∧ y = (aeval x) f) → ∃ f, f.natDegree < d ∧ y = (aeval x) f

case mpr
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, f.natDegree < d ∧ y = (aeval x) f) → ∃ f, f.degree < ↑d ∧ y = (aeval x) f
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v w : n → R
⊢ { toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } + { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v w : n → R
i✝ : n
⊢ ({ toFun := dotProduct (v + w), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 =
    (({ toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := dotProduct w, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
        LinearMap.single R (fun i ↦ R) i✝)
      1
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
t : R
v : n → R
⊢ { toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) t • { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
t : R
v : n → R
i✝ : n
⊢ ({ toFun := dotProduct (t • v), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 =
    (((RingHom.id R) t • { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ LinearMap.single R (fun i ↦ R) i✝)
      1
Module: Mathlib.LinearAlgebra.Matrix.Dual

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Dual R (n → R)
⊢ (fun v ↦ { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ })
      ((fun f i ↦ f ((LinearMap.single R (fun a ↦ R) i) 1)) f) =
    f

Tactic:
ext

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : Dual R (n → R)
i✝ : n
⊢ ((fun v ↦ { toFun := dotProduct v, map_add' := ⋯, map_smul' := ⋯ })
          ((fun f i ↦ f ((LinearMap.single R (fun a ↦ R) i) 1)) f) ∘ₗ
        LinearMap.single R (fun i ↦ R) i✝)
      1 =
    (f ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f) = Polynomial.map (Quotient.mk I) f

Tactic:
by
  simp only [polynomialQuotientEquivQuotientPolynomial, coe_eval₂RingHom, RingEquiv.symm_mk,
    RingEquiv.coe_mk, Equiv.coe_fn_symm_mk, Quotient.lift_mk]
  rw [eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]

Goal state after:
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
B : PowerBasis R S
⊢ ⊤ ≤ Subalgebra.toSubmodule R[B.gen]

Tactic:
← B.basis.span_eq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
⊢ Submodule.span R (Set.range ⇑B.basis) ≤ Subalgebra.toSubmodule R[B.gen]
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ norm R = MonoidHom.id R

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
x✝ : R
⊢ (norm R) x✝ = (MonoidHom.id R) x✝
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι

Tactic:
by
  have := Classical.decEq ι
  rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]
  simp

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: case inl
K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
⊢ root (X ^ Nat.succ 0 - C a) ≠ 0

Tactic:
rw [pow_one]

Goal state after:
case inl
K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
⊢ root (X - C a) ≠ 0