mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₂.IsPushout

Tactic:
refine CategoryTheory.IsPushout.of_iso h
    (evaluation₁.mapIso e) (evaluation₂.mapIso e)
    (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂

case refine_2
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃

case refine_3
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄

case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄
Module: Mathlib.Algebra.Lie.Basic

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
t : R
x y z : L
m n : M
⊢ ∀ (t : R) (x m : L), ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
by apply LieAlgebra.lie_smul

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃' = data.i₂ pq

Tactic:
by rw [hi₃', data.i₃_next r r' _ _ h]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₃' = data.i₂ pq

Tactic:
by rw [hi₃', data.i₃_next r r' _ _ h]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ Submodule.span R s ≤ (lieSpan R L s).toSubmodule

Tactic:
rw [Submodule.span_le, coe_toSubmodule]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ s ⊆ ↑(lieSpan R L s)
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ (lieSpan R L ↑{ toSubmodule := p, lie_mem' := h }).toSubmodule = { toSubmodule := p, lie_mem' := h }.toSubmodule

Tactic:
toSubmodule_inj,

Goal state after:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ lieSpan R L ↑{ toSubmodule := p, lie_mem' := h } = { toSubmodule := p, lie_mem' := h }
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K

Tactic:
rintro h' ⟨x, hx⟩ ⟨y, hy⟩ hy'; exact h' x y hx hy'

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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ ∃ (x_1 : x ∈ ⨆ i, N i), motive x x_1

Tactic:
refine iSup_induction N (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, N i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_

Goal state after:
case refine_1
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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx✝ : x✝ ∈ ⨆ i, N i
i : ι
x : M
hx : x ∈ N i
⊢ ∃ (hx : x ∈ ⨆ i, N i), motive x hx

case refine_2
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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : x ∈ ⨆ i, N i
⊢ ∃ (hx : 0 ∈ ⨆ i, N i), motive 0 hx

case refine_3
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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → x ∈ ⨆ i, N i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, N i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, N i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, N i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, N i), motive (x + y) hx
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
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ ↑(lieSpan R L ↑{ toSubmodule := p, lie_mem := h }) = ↑{ toSubmodule := p, lie_mem := h }

Tactic:
toSubmodule_inj,

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
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
⊢ lieSpan R L ↑{ toSubmodule := p, lie_mem := h } = { toSubmodule := p, lie_mem := h }
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
hnz : ¬minpoly A x - p = 0
⊢ (minpoly A x - p).degree < (minpoly A x).degree

Tactic:
apply degree_sub_lt_left _ (minpoly.ne_zero hx)

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
hnz : ¬minpoly A x - p = 0
⊢ (minpoly A x).leadingCoeff = p.leadingCoeff

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
hnz : ¬minpoly A x - p = 0
⊢ (minpoly A x).degree = p.degree
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case hp2
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
⊢ (Polynomial.aeval x) (p * C p.leadingCoeff⁻¹) = 0

Tactic:
aeval_mul,

Goal state after:
case hp2
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
⊢ (Polynomial.aeval x) p * (Polynomial.aeval x) (C p.leadingCoeff⁻¹) = 0
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
⊢ ∀ (q : A[X]), q.degree < (X - C a).degree → ¬q = 0 → (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0

Tactic:
intro q

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
a : A
hf : Injective ⇑(algebraMap A B)
a✝ : Nontrivial A
q : A[X]
⊢ q.degree < (X - C a).degree → ¬q = 0 → (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
p q : A[X]
hi : Irreducible p
b : B
hfa : (Polynomial.aeval b) p = 0
hga : (Polynomial.aeval b) q = 0
⊢ p ∣ minpoly A b

Tactic:
rw [← minpoly.eq_of_irreducible hi hfa]

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
p q : A[X]
hi : Irreducible p
b : B
hfa : (Polynomial.aeval b) p = 0
hga : (Polynomial.aeval b) q = 0
⊢ p ∣ p * C p.leadingCoeff⁻¹
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✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : (Polynomial.aeval x) (f * g) = 0
⊢ False

Tactic:
aeval_mul,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : (Polynomial.aeval x) f * (Polynomial.aeval x) g = 0
⊢ False
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case J
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
← I.incl_idealRange

Goal state after:
case J
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆
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]), q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree

Tactic:
intro q

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]
⊢ q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree
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]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C p * C (X - C a) + q * (X - C b) = P

Tactic:
by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ pb.minpolyGen.degree = ↑pb.dim

Tactic:
by
  unfold minpolyGen
  rw [degree_sub_eq_left_of_degree_lt] <;> rw [degree_X_pow]
  apply degree_sum_fin_lt

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : ∑ x_1, (aeval x) ((monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0

Tactic:
← map_sum

Goal state after:
case pos
S : Type u_2
inst✝² : Ring S
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra K S
x : S
h : IsIntegral K x
g : Fin (minpoly K x).natDegree → K
i : Fin (minpoly K x).natDegree
hg : (aeval x) (∑ x_1, (monomial ↑x_1) (g x_1)) = 0
⊢ g i = 0
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬Squarefree 0

Tactic:
rw [Squarefree, not_forall]
  exact ⟨0, by simp⟩

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : (∏ i ∈ s, (X - C (f i))).Separable
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Tactic:
← insert_erase hx,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x : ι
hfs : (∏ i ∈ insert x (s.erase x), (X - C (f i))).Separable
y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ ((toMatrix b b) f).det = LinearMap.det f

Tactic:
rw [det_eq_det_toMatrix_of_finset b.reindexFinsetRange,
    det_toMatrix_eq_det_toMatrix b b.reindexFinsetRange]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ (n₁ + k))) g₂ = (expand F (p ^ n₁)) g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂

Tactic:
pow_add,

Goal state after:
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
hp : 0 < p
n₁ : ℕ
g₁ : F[X]
hg₁ : g₁.Separable
hgf₁ : (expand F (p ^ n₁)) g₁ = f
g₂ : F[X]
hg₂ : g₂.Separable
k : ℕ
hgf₂ : (expand F (p ^ n₁ * p ^ k)) g₂ = (expand F (p ^ n₁)) g₁
⊢ n₁ = n₁ + k ∧ g₁ = g₂
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ annIdealGenerator 𝕜 a = 0 ↔ annIdeal 𝕜 a = ⊥

Tactic:
by
  simp only [annIdealGenerator, mul_eq_zero, IsPrincipal.eq_bot_iff_generator_eq_zero,
    Polynomial.C_eq_zero, inv_eq_zero, Polynomial.leadingCoeff_eq_zero, or_self_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b b' : Basis ι A M
⊢ ↑⋯.unit⁻¹ = b'.det ⇑b

Tactic:
by
  rw [← Units.mul_eq_one_iff_inv_eq, IsUnit.unit_spec, ← det_basis, ← det_basis]
  exact LinearEquiv.det_mul_det_symm _

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
⊢ ∀ (q : K[X]), q.Monic → (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree

Tactic:
intro q

Goal state after:
case refine_2
K : Type u_5
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (f * C f.leadingCoeff⁻¹).Monic
q : K[X]
⊢ q.Monic → (aeval (root f)) q = 0 → (f * C f.leadingCoeff⁻¹).degree ≤ q.degree
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
g✝ : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := ⋯
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ Quot.mk (⇑(Submodule.quotientRel (span {f}))) g = (aeval (root f)) g

Tactic:
aeval_eq

Goal state after:
case h
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
g✝ : R[X]
inst✝ : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := f * C f.leadingCoeff⁻¹
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ Quot.mk (⇑(Submodule.quotientRel (span {f}))) g = (mk f) g
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ (a : Submodule R M) (b : a ∈ ((Algebra.lsmul R R M) f).invtSubmodule),
      a ≤ p → ∃ a_2 ≤ p, (∃ (x : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), ⟨a ⊓ a_2, ⋯⟩ = ⊥) ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p

Tactic:
invtSubmodule.mk_eq_bot_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
e : Submodule R[X] (AEval' (LinearMap.restrict f hp)) ≃o ↑(Iic ((AEval.mapSubmodule R M f) ⟨p, hp⟩)) :=
  (Submodule.orderIsoMapComap (AEval.restrict_equiv_mapSubmodule f p hp)).trans
    ((AEval.mapSubmodule R M f) ⟨p, hp⟩).mapIic
⊢ (∀ a ∈ ((Algebra.lsmul R R M) f).invtSubmodule,
      a ≤ p → ∃ a_2 ≤ p, (∃ (_ : a_2 ∈ ((Algebra.lsmul R R M) f).invtSubmodule), a ⊓ a_2 = ⊥) ∧ a ⊔ a_2 = p) ↔
    ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ q ⊓ r = ⊥ ∧ q ⊔ r = p
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
x✝ : AdjoinRoot g
x : R[X]
⊢ (aeval (root g)) x = (mk g) x

Tactic:
aeval_eq

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : (aeval (root g)) (minpoly R pb.gen) = 0
h₂ : (aeval pb.gen) g = 0
x✝ : AdjoinRoot g
x : R[X]
⊢ (mk g) x = (mk g) x
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotQuotEquivComm I f)
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (span {(Ideal.Quotient.mk (Ideal.map C I)) f})) ((Ideal.Quotient.mk (Ideal.map C I)) p)

Tactic:
by
  simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk,
    polynomialQuotientEquivQuotientPolynomial_map_mk]

Goal state after:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
⊢ IsFinitelySemisimple (LinearMap.restrict f hp)

Tactic:
intro q

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
hf : f.IsFinitelySemisimple
q : Submodule R ↥p
⊢ ∀ (hp_1 : q ∈ invtSubmodule (LinearMap.restrict f hp)),
    Module.Finite R ↥q → IsSemisimple ((LinearMap.restrict f hp).restrict hp_1)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f) ((algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x) =
    (algebraMap R ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})) x

Tactic:
rw [this, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, map_C, Quotient.alg_map_eq]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝ : CommRing R
I✝ : Ideal R
f✝ f : R[X]
I : Ideal R
x : R
this : (algebraMap R (AdjoinRoot f ⧸ Ideal.map (of f) I)) x = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) (C x))
⊢ (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (C ((Ideal.Quotient.mk I) x)) =
    ((algebraMap (R ⧸ I)[X] ((R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) f})).comp
        (algebraMap R (R ⧸ I)[X]))
      x
Module: Mathlib.Algebra.Lie.AdjointAction.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
this : (ad K (Module.End K V)) n = (ad K (Module.End K V)) (n + s) - (ad K (Module.End K V)) s
⊢ (ad K (Module.End K V)) n ∈ K[(ad K (Module.End K V)) (n + s)]

Tactic:
rw [this]

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n s : Module.End K V
hc : Commute n s
hn : IsNilpotent n
hs : s.IsSemisimple
this : (ad K (Module.End K V)) n = (ad K (Module.End K V)) (n + s) - (ad K (Module.End K V)) s
⊢ (ad K (Module.End K V)) (n + s) - (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hy : y ∈ H
⊢ -⁅x, y⁆ ∈ H ↔ ⁅x, y⁆ ∈ H

Tactic:
neg_mem_iff (G := L)

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ -⁅y, x⁆ ∈ H

Tactic:
neg_mem_iff (G := L)

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case refine_1
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
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lowerCentralSeries R L (↥N) k = ⊥
⊢ lcs k N = ⊥

Tactic:
rw [← N.lowerCentralSeries_map_eq_lcs, ← LieModuleHom.le_ker_iff_map]
    simpa

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

Goal state before:
pp: R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsNoetherian R L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range
h : ∀ (y : ↥L'), IsNilpotent ↑y
s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}
hs : s.Nonempty
this : ∀ K ∈ s, K ≠ ⊤ → ∃ K' ∈ s, K < K'
_i5 : IsNoetherian R ↥L'
hK₁ : ⊤ ∈ s
hK₂ : ∀ x ∈ s, ¬⊤ < x
⊢ ⊤ ∈ s

Tactic:
exact hK₁

Goal state after: