mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case pos.refine_2
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).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ 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''
⊢ (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom ≫
      X.d (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯ =
    pageD X data r pq' pq'' ⋯ ≫
      (pageXIso X data r hr pq'' (data.i₀ r pq'' ⋯) i₀' i₀ i₁ ⋯ ⋯ ⋯ ⋯ n₁ n₂ (n₂ + 1) ⋯ ⋯ ⋯).hom

Tactic:
rw [pageD_eq X data r hr pq' pq'' h
        (homOfLE (data.le₀₁' r hr pq'' rfl (by simpa [← data.i₀_prev r r' _ _ h])))
        (homOfLE (data.i₀_le' hrr' hr pq' hi₀' hi₀)) (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
        (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃))
        rfl (by rw [hi₀', data.i₀_prev r r' _ _ h]) hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ (n₂ + 1) hn₁',
        Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ i, M✝ i)

Tactic:
← e.iSup_comp

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
ι : Type u_5
inst✝¹ : Finite ι
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
h : ∀ {M : α✝ → Submodule R P} [∀ (i : α✝), IsArtinian R ↥(M i)], IsArtinian R ↥(⨆ i, M i)
M✝ : β✝ → Submodule R P
inst✝ : ∀ (i : β✝), IsArtinian R ↥(M✝ i)
⊢ IsArtinian R ↥(⨆ x, M✝ (e x))
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'
⊢ n₀ = data.deg pq

Tactic:
have := data.hc r _ _ h

Goal state after:
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'
this : data.deg pq + 1 = data.deg pq'
⊢ n₀ = data.deg pq
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
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy✝ : y ∈ f.range
hy : ∃ y_1, f y_1 = y
⊢ ∃ a, f.rangeRestrict a = ⟨y, hy✝⟩

Tactic:
obtain ⟨x, rfl⟩ := hy

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : f x ∈ f.range
⊢ ∃ a, f.rangeRestrict a = ⟨f x, hy⟩
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'
x : L
⊢ f x ∈ f.idealRange

Tactic:
rw [idealRange_eq_map]

Goal state after:
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'
x : L
⊢ f x ∈ LieIdeal.map f ⊤
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
⊢ ↑(map N.incl (comap N.incl N')) = ↑(N ⊓ N')

Tactic:
exact (N : Submodule R M).map_comap_subtype N'

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'
h : f.range = ⊤
⊢ ↑(LieSubmodule.lieSpan R L' ↑⊤.toSubmodule) = ↑⊤

Tactic:
LieSubmodule.top_toSubmodule,

Goal state after:
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'
h : f.range = ⊤
⊢ ↑(LieSubmodule.lieSpan R L' ↑⊤.toSubmodule) = ⊤
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'
I : LieIdeal R L
x : L'
y : L
hy₂ : ↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ ↑f y ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Tactic:
rw [← hy]

Goal state after:
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'
I : LieIdeal R L
x : L'
y : L
hy₂ : ↑f y = x
z₁ : L
hz₁ : z₁ ∈ I
z₂ : L
hz₂ : z₂ ∈ f.ker
hy : z₁ + z₂ = y
⊢ ↑f (z₁ + z₂) ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: case a
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:
rw [le_inf_iff]

Goal state after:
case a
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 ∧ map f (comap f J) ≤ J
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 J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I ⊓ J

Tactic:
rw [le_inf_iff]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I ∧ ⁅I, J⁆ ≤ J
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 : LieIdeal R L
⊢ ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_eq_bot_iff]

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 : LieIdeal R L
⊢ (∀ m ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}, m = 0) ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
Module: Mathlib.Algebra.Lie.Ideal

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ toLieSubalgebra R L I = I.incl.range

Tactic:
exact (I : LieSubalgebra R L).incl_range.symm

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ Submodule.comap ↑I.incl ↑I₂ = ↑⊤ ↔ I ≤ I₂

Tactic:
LieSubmodule.top_toSubmodule,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ Submodule.comap ↑I.incl ↑I₂ = ⊤ ↔ I ≤ I₂
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: L : Type u_1
M : Type u_2
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : Subsingleton M
x : L
m : M
⊢ ⁅x, m⁆ = 0

Tactic:
simp_rw [Subsingleton.eq_zero m, lie_zero]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ IsFaithful R L M ↔ LieModule.ker R L M = ⊥

Tactic:
rw [isFaithful_iff', LieSubmodule.ext_iff]
  aesop

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N₂ : LieSubmodule R L M
⊢ Submodule.comap (↑N).subtype ↑N₂ = ↑⊤ ↔ N ≤ N₂

Tactic:
LieSubmodule.top_toSubmodule,

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
⊢ Submodule.comap (↑N).subtype ↑N₂ = ⊤ ↔ N ≤ 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 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]

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: 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
⊢ N ⊓ N' ≤ N'

Tactic:
exact inf_le_right

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

Tactic:
rw [le_inf_iff]

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.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✝ : Subsingleton B
a✝ : Nontrivial A
⊢ minpoly A x = 1

Tactic:
have := minpoly.min A x monic_one (Subsingleton.elim _ _)

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Subsingleton B
a✝ : Nontrivial A
this : (minpoly A x).degree ≤ degree 1
⊢ minpoly A x = 1
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: 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 ≤ J

Tactic:
exact inf_le_right

Goal state after:
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]
hl : q.natDegree = 0
h0 : ¬q = 0
⊢ (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0

Tactic:
eq_C_of_natDegree_eq_zero hl

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]
hl : q.natDegree = 0
h0 : ¬C (q.coeff 0) = 0
⊢ (Polynomial.aeval ((algebraMap A B) a)) (C (q.coeff 0)) ≠ 0
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ +
        (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ +
          ⁅L b, 2 • L (b * c)⁆) +
      (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ +
        ⁅L c, 2 • L (b * c)⁆) =
    ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) +
          (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) +
        (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) +
      (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆)

Tactic:
(commute_lmul_lmul_sq b).lie_eq,

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 0 + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ +
        (⁅L b, L (a * a)⁆ + 0 + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) +
      (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ +
        ⁅L c, 2 • L (b * c)⁆) =
    ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) +
          (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) +
        (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) +
      (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆)
Module: Mathlib.LinearAlgebra.SModEq.Basic

Goal state before:
pp: R : Type u_6
inst✝ : CommRing R
I : Ideal R
x y : R
h : x ≡ y [SMOD I]
f : R[X]
⊢ Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]

Tactic:
Polynomial.eval_eq_sum,

Goal state after:
R : Type u_6
inst✝ : CommRing R
I : Ideal R
x y : R
h : x ≡ y [SMOD I]
f : R[X]
⊢ (f.sum fun e a ↦ a * x ^ e) ≡ f.sum fun e a ↦ a * y ^ e [SMOD I]
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
p q d : A[X]
h : p * q = minpoly A x * d
⊢ (Polynomial.aeval x) (p * q) = 0

Tactic:
simp [h, aeval A x]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case neg.hc
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ↑⟨↑k + 1, ⋯⟩ = ↑k + 1

pp: case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim), x ≠ ⟨↑k + 1, ⋯⟩ → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0

Tactic:
· rfl

Goal state after:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim), x ≠ ⟨↑k + 1, ⋯⟩ → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ f.coeff n ∈ comap C I

Tactic:
mem_comap,

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : ↥((Quotient.mk I).comp C).range
hx : C x ∈ map (mapRingHom ((Quotient.mk I).comp C).rangeRestrict) I
i : R →+* ↥((Quotient.mk I).comp C).range := ((Quotient.mk I).comp C).rangeRestrict
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ C (f.coeff n) ∈ I
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
⊢ (map f p).Separable ↔ p.Separable

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
  obtain ⟨m, hm⟩ := Ideal.exists_maximal S
  have := Separable.map H (f := Ideal.Quotient.mk m)
  rwa [map_map, separable_def, derivative_map, isCoprime_map] at this

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f

Tactic:
have : Module.Finite A M := by
      rcases H with ⟨s, ⟨hs⟩⟩
      exact Module.Finite.of_basis hs

Goal state after:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Free A M
c : A
f : M →ₗ[A] M
a✝ : Nontrivial A
H : ∃ s, Nonempty (Basis (↥s) A M)
this : Module.Finite A M
⊢ LinearMap.det (c • f) = c ^ finrank A M * LinearMap.det f
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
⊢ ⇑(iterateFrobeniusEquiv R p n) = (⇑((RingAut.toPerm R) (frobeniusEquiv R p)))^[n]

Tactic:
exact (pow_iterate p n).symm

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case succ
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
n : ℕ
ih : ∀ (x : R), (⇑(frobeniusEquiv R p).symm)^[n] x ^ p ^ n = x
x : R
⊢ (⇑(frobeniusEquiv R p).symm)^[n + 1] x ^ p ^ (n + 1) = x

Tactic:
simp [pow_succ, pow_mul, ih]

Goal state after:
Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p

Tactic:
rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inr
F : Type u_1
K : Type u_3
inst✝² : CommRing F
inst✝¹ : Ring K
inst✝ : Algebra F K
x : K
h : IsSeparable F x
h✝ : Nontrivial F
⊢ IsIntegral F x

Tactic:
exact of_not_not (h.ne_zero <| minpoly.eq_zero ·)

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)

Tactic:
exact (LinearMap.commute_mulLeft_right a a).isNilpotent_sub hl hr

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i) x p = 0
r : R
⊢ (liftAlgHom p i x h) ((of p) r) = i r

Tactic:
by
  simp [liftAlgHom]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i) x p = 0
⊢ (liftAlgHom p i x h) (root p) = x

Tactic:
by
  simp [liftAlgHom]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Lemmas

Goal state before:
pp: R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (-(x - y)) ^ n = 0

Tactic:
neg_pow,

Goal state after:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (-1) ^ n * (x - y) ^ n = 0
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
c : R
x : L
t : M ⊗[R] N
⊢ ⁅c • x, t⁆ = c • ⁅x, t⁆

Tactic:
change hasBracketAux (c • x) _ = c • hasBracketAux _ _

Goal state after:
R : Type u
inst✝¹⁸ : CommRing R
L : Type v
M : Type w
N : Type w₁
P : Type w₂
Q : Type w₃
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
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L P
inst✝⁴ : LieModule R L P
inst✝³ : AddCommGroup Q
inst✝² : Module R Q
inst✝¹ : LieRingModule L Q
inst✝ : LieModule R L Q
c : R
x : L
t : M ⊗[R] N
⊢ (hasBracketAux (c • x)) t = c • (hasBracketAux x) t
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
z : L
⊢ z ∈ (LieIdeal.toLieSubalgebra R L (derivedSeries R L 1)).toSubmodule ↔
    z ∈ Submodule.span R {x | ∃ x_1 y, ⁅x_1, y⁆ = x}

Tactic:
simp only [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
    LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span']

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
z : L
⊢ z ∈ Submodule.span R {x | ∃ x_1 ∈ ⊤, ∃ n ∈ ⊤, ⁅x_1, n⁆ = x} ↔ z ∈ Submodule.span R {x | ∃ x_1 y, ⁅x_1, y⁆ = x}
Module: Mathlib.Algebra.Lie.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} =
    Submodule.map (↑(toModuleHom R L M)) (↑(TensorProduct.LieModule.map (incl I) N.incl)).range

Tactic:
toLinearMap_map,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} =
    Submodule.map (↑(toModuleHom R L M)) (TensorProduct.map ↑(incl I) ↑N.incl).range
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
⊢ derivedSeries R L 0 = ⊤

pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
n✝ : ℕ
⊢ derivedSeries R L (n✝ + 1) = ⊤

Tactic:
· rfl

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
n✝ : ℕ
⊢ derivedSeries R L (n✝ + 1) = ⊤