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

Goal state before:
pp: case refine_1.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
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅⁅y, ↑x⁆, ↑n⁆ ∈ Submodule.span R s

Tactic:
apply Submodule.subset_span

Goal state after:
case refine_1.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
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := ⋯
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅⁅y, ↑x⁆, ↑n⁆ ∈ s
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case refine_1.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
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅↑x, ⁅y, ↑n⁆⁆ ∈ Submodule.span R s

Tactic:
apply Submodule.subset_span

Goal state after:
case refine_1.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
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := ⋯
y : L
m' : M
hm' : m' ∈ Submodule.span R s
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅↑x, ↑n⁆ = m''
⊢ ⁅↑x, ⁅y, ↑n⁆⁆ ∈ s
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case insert
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
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih : ∀ {m : M}, ↑t ⊆ {x | ∃ p ∈ S, ↑p = x} → m ∈ ⨆ i ∈ t, i → ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
m : M
hs : ↑(insert q t) ⊆ {x | ∃ p ∈ S, ↑p = x}
hsm : m ∈ ⨆ i ∈ insert q t, i
⊢ ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}

Tactic:
| insert q t hqt ih =>

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
p : ι → LieSubmodule R L M
x✝ : M
⊢ x✝ ∈ sSup {x | ∃ s ∈ range fun i ↦ p i, ↑s = x} ↔ x✝ ∈ ⨆ i, ↑(p i)

Tactic:
simp [Submodule.mem_sSup, Submodule.mem_iSup]

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J : LieIdeal R L'
h : f.IsIdealMorphism
⊢ map f (comap f J) = f.idealRange ⊓ J

Tactic:
apply le_antisymm
  · rw [le_inf_iff]; exact ⟨f.map_le_idealRange _, map_comap_le⟩
  · rw [f.isIdealMorphism_def] at h
    rw [← SetLike.coe_subset_coe, LieSubmodule.coe_inf, ← coe_toLieSubalgebra, h]
    rintro y ⟨⟨x, h₁⟩, h₂⟩; rw [← h₁] at h₂ ⊢; exact mem_map h₂

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

Goal state before:
pp: R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ e.range = ⊤

Tactic:
rw [LieModuleHom.range_eq_top]

Goal state after:
R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ Function.Surjective ⇑e.toLieModuleHom
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]
x✝ : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
⊢ (Polynomial.aeval x) p = 0

Tactic:
by rw [hq, map_mul, aeval, zero_mul]

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

Goal state before:
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:
simp [← h, ← hx']

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

Tactic:
rw [le_inf_iff]; constructor <;>
  apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]

Goal state after:
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:
h₁,

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₂⁆ = comap I.incl ⁅I₁, 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]
hq : q.Monic
hs : (Polynomial.aeval σ.toLinearMap) q = 0
H : q.natDegree < orderOf σ
⊢ False

Tactic:
rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs

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
hs : ∑ i, q.coeff ↑i • σ.toLinearMap ^ ↑i = 0
H : q.natDegree < orderOf σ
⊢ False
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Subsingleton B
⊢ b ≡ (algebraMap A B) 0 [SMOD Ideal.span {pb.gen}]

Tactic:
SModEq,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Subsingleton B
⊢ Submodule.Quotient.mk b = Submodule.Quotient.mk ((algebraMap A B) 0)
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
⊢ b ≡ (algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩) [SMOD Ideal.span {pb.gen}]

Tactic:
SModEq,

Goal state after:
case inr
A : Type u_4
B : Type u_5
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
pb : PowerBasis A B
b : B
h✝ : Nontrivial B
H : (pb.basis.repr b) ⟨0, ⋯⟩ • pb.basis ⟨0, ⋯⟩ + ∑ x ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr b) x • pb.basis x = b
⊢ Submodule.Quotient.mk b = Submodule.Quotient.mk ((algebraMap A B) ((pb.basis.repr b) ⟨0, ⋯⟩))
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).coeff 0 - 1 ∈ I ∧ (aeval ⅟x) (1 - p - X * q).reverse = 0

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).coeff 0 ≠ 0

Tactic:
· exact ⟨this, (eval₂_reverse_eq_zero_iff ..).mpr <| by simp [← aeval_def, hp.2, hq, ← eq, hw]⟩

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 ≠ 0
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i ∈ Finset.range pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) =
    (f %ₘ minpoly A pb.gen).coeff i • y ^ i

Tactic:
rw [Finset.mem_range] at hi

Goal state after:
case neg
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f : A[X]
h✝ : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) =
    (f %ₘ minpoly A pb.gen).coeff i • y ^ i
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
x : S
hx : B.gen ∈ R[x]
⊢ R[B.gen] ≤ R[x]

Tactic:
refine adjoin_le ?_

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
x : S
hx : B.gen ∈ R[x]
⊢ {B.gen} ⊆ ↑R[x]
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : ¬IsUnit x
⊢ n = 0 ∨ n = 1

Tactic:
contrapose! h'

Goal state after:
R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ IsUnit x
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 2 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Tactic:
rw [← one_add_one_eq_two]

Goal state after:
R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ 1 + 1 ≤ emultiplicity a r ↔ 1 < emultiplicity a r
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ LinearMap.det f = 1

Tactic:
refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl
    intro s b
    have : IsEmpty s := by
      rw [← Fintype.card_eq_zero_iff]
      exact (Module.finrank_eq_card_basis b).symm.trans h
    exact Matrix.det_isEmpty

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p q : ℕ
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : PerfectRing M q
⊢ Bijective fun x ↦ x ^ 1

Tactic:
simpa using! bijective_id

Goal state after:
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✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = (of f) ↑q.num / (of f) ↑q.den

Tactic:
← map_div₀,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = (of f) (↑q.num / ↑q.den)
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✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = (of f) (↑q.num / ↑q.den)

Tactic:
← NNRat.cast_def

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = (of f) ↑q
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✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ
⊢ ↑q = (of f) ↑q.num / (of f) ↑q.den

Tactic:
← map_div₀,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ
⊢ ↑q = (of f) (↑q.num / ↑q.den)
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
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
i : ℕ
hi : i ≤ k
⊢ (f ^ i) x ∈ ↑(Submodule.comap f (Submodule.span R {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}))

Tactic:
apply Submodule.subset_span

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
hs : f.IsFinitelySemisimple
this : ∀ (p : Submodule R M) (hp₁ : p ∈ f.invtSubmodule), Module.Finite R ↥p → LinearMap.restrict f hp₁ = 0
x : M
k : ℕ
hk : f ^ k = 0
p : Submodule R M := ⋯
i : ℕ
hi : i ≤ k
⊢ f ((f ^ i) x) ∈ {x_1 | ∃ i, ∃ (_ : i ≤ k), (f ^ i) x = x_1}
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i

Tactic:
h₁,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : FiniteDimensional K V
inst✝ : PerfectField K
n₁ s₁ n₂ s₂ : End K V
hn₁ : IsNilpotent n₁
hs₁ : s₁.IsSemisimple
hn₂ : IsNilpotent n₂
hs₂ : s₂.IsSemisimple
hc₁ : Commute n₁ s₁
hc₂ : Commute n₂ s₂
h : n₁ + s₁ = n₂ + s₂
n₀ : End K V
hn₀ : n₀ ∈ K[n₁ + s₁]
s₀ : End K V
hs₀ : s₀ ∈ K[n₁ + s₁]
hn₀_nil : IsNilpotent n₀
hs₀_ss : s₀.IsSemisimple
h₀ : n₁ + s₁ = n₀ + s₀
n s : End K V
hn : IsNilpotent n
hs : s.IsSemisimple
hc : Commute n s
heq : n₁ + s₁ = n + s
hsf : Commute s (n₁ + s₁)
hnf : Commute n (n₁ + s₁)
⊢ IsNilpotent (n₀ - n)

Tactic:
exact (commute_of_mem_adjoin_singleton_of_commute hn₀ hnf).symm.isNilpotent_sub hn₀_nil hn

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeries R (↥I) k = comap I.incl (derivedSeriesOfIdeal R L k I)

Tactic:
by
  induction k with
  | zero => simp only [derivedSeries_def, comap_incl_self, derivedSeriesOfIdeal_zero]
  | succ k ih =>
    simp only [derivedSeries_def, derivedSeriesOfIdeal_succ] at ih ⊢; rw [ih]
    exact comap_bracket_incl_of_le I (derivedSeriesOfIdeal_le_self I k)
      (derivedSeriesOfIdeal_le_self I k)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
this : ((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₁ = 0
⊢ ((bracket' R A L L) z₁) z₁ + ((bracket' R A L L) z₂) z₁ + (((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₂) =
    0

Tactic:
h₁,

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((bracket' R A L L) z₁) z₁ = 0
h₂ : ((bracket' R A L L) z₂) z₂ = 0
this : ((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₁ = 0
⊢ 0 + ((bracket' R A L L) z₂) z₁ + (((bracket' R A L L) z₁) z₂ + ((bracket' R A L L) z₂) z₂) = 0
Module: Mathlib.Algebra.Lie.Quotient

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ ⁅mk x + mk y, mk z⁆ = mk ⁅x, z⁆ + mk ⁅y, z⁆

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ ⁅Submodule.Quotient.mk (x + y), mk z⁆ = mk ⁅x, z⁆ + mk ⁅y, z⁆
Module: Mathlib.Algebra.Lie.Quotient

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x + y, z⁆ = mk ⁅x, z⁆ + mk ⁅y, z⁆

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x + y, z⁆ = Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆)
Module: Mathlib.Algebra.Lie.Quotient

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x + y, z⁆ = Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x + y, z⁆ = Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆)
Module: Mathlib.Algebra.Lie.Quotient

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ ⁅mk x, mk y + mk z⁆ = mk ⁅x, y⁆ + mk ⁅x, z⁆

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ ⁅mk x, Submodule.Quotient.mk (y + z)⁆ = mk ⁅x, y⁆ + mk ⁅x, z⁆
Module: Mathlib.Algebra.Lie.Quotient

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, y + z⁆ = mk ⁅x, y⁆ + mk ⁅x, z⁆

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, y + z⁆ = Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆)
Module: Mathlib.Algebra.Lie.Quotient

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, y + z⁆ = Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, y + z⁆ = Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆)
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
t : A
x : A ⊗[R] L
m : A ⊗[R] M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
simp only [bracket_def, map_smul, LinearMap.smul_apply]

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

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = mk ⁅⁅x, y⁆, z⁆ + mk ⁅y, ⁅x, z⁆⁆

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆)
Module: Mathlib.Algebra.Lie.Quotient

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

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 N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆)