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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
x : (X.H n₁).obj (mk₁ f) ⟶ A
hx : X.δ f g n₀ n₁ hn₁ ≫ x = 0
⊢ X.δ f g (n₁ - 1) n₁ ⋯ ≫ x = 0

Tactic:
by
    obtain rfl : n₀ = n₁ -1 := by lia
    exact hx

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

Goal state before:
pp: C : Type u_1
ι' : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι'
X' : SpectralObject C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ =
    X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂

Tactic:
rw [← map_comp .., ← map_comp ..]
  rfl

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
hg : IsIso g
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
simpa only [Preadditive.IsIso.comp_right_eq_zero] using X.zero₁ f g _ rfl n₀ n₁

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

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
l : ℕ
⊢ ∀ (r r' : ℤ) (pq : ℤ × Fin l),
    autoParam (2 ≤ r) SpectralSequenceDataCore._auto_32 →
      autoParam (r ≤ r') SpectralSequenceDataCore._auto_34 →
        Fin.clamp (↑↑pq.2 + (r - 1)).toNat l ≤ Fin.clamp (↑↑pq.2 + (r' - 1)).toNat l

Tactic:
by
    rintro r r' ⟨a, ⟨a', _⟩⟩ hr hrr'
    rw [Fin.mk_le_mk]
    exact Fin.clamp_monotone (by lia)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
p : ↑{I | I.IsMaximal}
q : { I // I.IsMaximal }
hq1 : q ∈ s
hq2 : ↑q ≤ ↑p
⊢ p ∈ s

Tactic:
← Subtype.ext <| q.2.eq_of_le p.2.ne_top hq2

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsArtinianRing R
s : Finset { I // I.IsMaximal }
H : ∀ (a : { I // I.IsMaximal }), s.inf Subtype.val ≤ ↑a
p : ↑{I | I.IsMaximal}
q : { I // I.IsMaximal }
hq1 : q ∈ s
hq2 : ↑q ≤ ↑p
⊢ q ∈ s
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: case succ
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
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
⊢ ∑ x_1 ∈ antidiagonal n, n.choose x_1.1 • ⁅((ad R L) x ^ x_1.1) y, (φ x) ((φ x ^ x_1.2) z)⁆ +
      ∑ x_1 ∈ antidiagonal n, n.choose x_1.1 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆ =
    ∑ x_1 ∈ antidiagonal n, n.choose x_1.1 • ⁅((ad R L) x ^ x_1.1) y, (φ x) ((φ x ^ x_1.2) z)⁆ +
      ∑ x_1 ∈ antidiagonal n, n.choose x_1.2 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆

Tactic:
add_left_cancel_iff,

Goal state after:
case succ
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
x y : L
z : M
n : ℕ
ih : (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆
⊢ ∑ x_1 ∈ antidiagonal n, n.choose x_1.1 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆ =
    ∑ x_1 ∈ antidiagonal n, n.choose x_1.2 • ⁅((ad R L) x) (((ad R L) x ^ x_1.1) y), (φ x ^ x_1.2) z⁆
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
m : L
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)

Tactic:
rw [SetLike.mem_coe, mem_lieSpan]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
⊢ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
⊢ e.toLinearEquiv.conj ((ad R L) x) = (ad R L') (e x)

Tactic:
ext y'
  rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]

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

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'
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier

Tactic:
suffices ⁅f x, f y⁆ ∈ J by
        simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          Submodule.mem_toAddSubmonoid, Submodule.mem_comap, LieHom.coe_toLinearMap, LieHom.map_lie,
          LieSubalgebra.mem_toSubmodule]
        exact this
      apply J.lie_mem h

Goal state after:
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'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ ⇑f '' ↑I ⊆ ↑(map f I)

Tactic:
exact LieSubmodule.subset_lieSpan

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'
I : LieIdeal R L
⊢ LieIdeal.map f I ≤ f.idealRange

Tactic:
rw [f.idealRange_eq_map]
  exact LieIdeal.map_mono le_top

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'
I : LieIdeal R L
h₁ : Function.Injective ⇑f
h₂ : map f I = ⊥
⊢ I = ⊥

Tactic:
by
  rw [← f.ker_eq_bot, LieHom.ker] at h₁
  rw [eq_bot_iff, map_le_iff_le_comap, h₁] at h₂
  rw [eq_bot_iff]; exact h₂

Goal state after:
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 : toLieSubalgebra R L' f.idealRange = f.range
y : L'
x : L
h₂ : ↑f x ∈ ↑J
h₁ : ↑f x = y
⊢ ↑f x ∈ ↑(map f (comap f J))

Tactic:
exact mem_map h₂

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
s : Set M
m : M
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)

Tactic:
rw [SetLike.mem_coe, mem_lieSpan]

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
s : Set M
m : M
hm : m ∈ s
⊢ ∀ (N : LieSubmodule R L M), s ⊆ ↑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
c : R
x : M
hx : x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
y : L
⊢ ⁅y, c • x⁆ = 0

Tactic:
lie_smul,

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
c : R
x : M
hx : x ∈ {m | ∀ (x : L), ⁅x, m⁆ = 0}
y : L
⊢ c • ⁅y, x⁆ = 0
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
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ↑k + 1 = pb.dim
⊢ pb.gen ^ pb.dim + ∑ x, pb.minpolyGen.coeff ↑x • pb.gen ^ ↑x = (aeval pb.gen) pb.minpolyGen

Tactic:
rw [add_comm, aeval_eq_sum_range, Finset.sum_range_succ, ← leadingCoeff,
      pb.minpolyGen_monic.leadingCoeff, one_smul, natDegree_minpolyGen, Finset.sum_range]

Goal state after:
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: case inr
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
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)

Tactic:
by_cases hf : f %ₘ minpoly A pb.gen = 0

Goal state after:
case pos
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
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)

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
⊢ ((pb.basis.constr A) fun i ↦ y ^ ↑i) ((aeval pb.gen) (f %ₘ minpoly A pb.gen)) = (aeval y) (f %ₘ minpoly A pb.gen)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ d ∣ y

Tactic:
exact dvd_trans ⟨c, by rw [hc, ← eq, mul_comm]⟩ hb

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ f.Separable

Tactic:
have := h.of_mul_left_left; rw [derivative_mul] at this
  exact IsCoprime.of_mul_right_left (IsCoprime.of_add_mul_left_right this)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime (q * q * p) (q * derivative q * p + q * derivative q * p + q * q * derivative p)

Tactic:
dsimp only [Separable] at hp

Goal state after:
R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) (derivative (q * q * p))
⊢ IsCoprime (q * q * p) (q * derivative q * p + q * derivative q * p + q * q * derivative p)
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
H : derivative f = 0
HF : CharP F 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ g, Irreducible g ∧ (expand F 0) g = f

Tactic:
have := CharP.charP_to_charZero F
      have := derivative_eq_zero.1 H
      have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
      contradiction

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ (p • f.roots).toFinset = f.roots.toFinset

Tactic:
(roots f).toFinset_nsmul _ (expChar_pos R p).ne'

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ f.roots.toFinset = f.roots.toFinset
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n✝ : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : DecidableEq R
inst✝ : PerfectRing R p
n : ℕ
⊢ ⇑(iterateFrobeniusEquiv R p n).toEquiv '' ↑((expand R (p ^ n)) f).roots.toFinset = ↑f.roots.toFinset

Tactic:
by
    rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n)]
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ (b'.toMatrix (⇑f ∘ ⇑b)).det =
    ((LinearMap.toMatrix b b') f * (LinearMap.toMatrix b' b) ↑(b'.equiv b (Equiv.refl ι))).det

Tactic:
Matrix.det_mul,

Goal state after:
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ (b'.toMatrix (⇑f ∘ ⇑b)).det =
    ((LinearMap.toMatrix b b') f).det * ((LinearMap.toMatrix b' b) ↑(b'.equiv b (Equiv.refl ι))).det
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
g : R[X]
hg : g.Monic
i : Fin g.natDegree
⊢ (mk g) ((monomial ↑i) (Pi.single i 1 i)) = root g ^ ↑i

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]
hg : g.Monic
i : Fin g.natDegree
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial ↑b) (Pi.single i 1 b) = 0

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]
hg : g.Monic
i : Fin g.natDegree
⊢ i ∉ Finset.univ → (monomial ↑i) (Pi.single i 1 i) = 0

Tactic:
· rw [Pi.single_eq_same, monomial_one_right_eq_X_pow, (mk g).map_pow, mk_X]

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]
hg : g.Monic
i : Fin g.natDegree
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial ↑b) (Pi.single i 1 b) = 0

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]
hg : g.Monic
i : Fin g.natDegree
⊢ i ∉ Finset.univ → (monomial ↑i) (Pi.single i 1 i) = 0
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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : (aeval f) (X ^ n) = 0
⊢ (aeval f) X = 0

Tactic:
rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M)] at h0 ⊢

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
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ annihilator R[X] (AEval R M f)
⊢ X ∈ annihilator R[X] (AEval R M f)
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ exp a • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
exp,

Goal state after:
case inr
A : Type u_1
inst✝⁴ : Ring A
inst✝³ : Module ℚ A
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module ℚ M
a : A
m : M
k : ℕ
h : a ^ k • m = 0
hn : IsNilpotent a
h₀ : k < nilpotencyClass a
⊢ (∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m
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
n' : Module.End K (Module.End K V)
hn'_adj : n' ∈ K[(ad K (Module.End K V)) (n + s)]
s' : Module.End K (Module.End K V)
hs'_adj : s' ∈ K[(ad K (Module.End K V)) (n + s)]
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V)) (n + s) = n' + s'
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]

Tactic:
have hc' : Commute n' s' :=
    Algebra.commute_of_mem_adjoin_singleton_of_commute hs'_adj
      (Algebra.commute_of_mem_adjoin_self hn'_adj).symm

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
n' : Module.End K (Module.End K V)
hn'_adj : n' ∈ K[(ad K (Module.End K V)) (n + s)]
s' : Module.End K (Module.End K V)
hs'_adj : s' ∈ K[(ad K (Module.End K V)) (n + s)]
hn'_nil : IsNilpotent n'
hs'_ss : s'.IsSemisimple
h_jc : (ad K (Module.End K V)) (n + s) = n' + s'
hc' : Commute n' s'
⊢ (ad K (Module.End K V)) s ∈ K[(ad K (Module.End K V)) (n + s)]
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
ha : IsNilpotent a
a✝ : Nontrivial A
⊢ IsNilpotent (exp a - 1)

Tactic:
exp,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
ha : IsNilpotent a
a✝ : Nontrivial A
⊢ IsNilpotent (∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i - 1)
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 : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ R ∙ x
s : R
hu₂ : s • x ∈ R ∙ x
⊢ ⁅t • x + v, s • x + w⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
apply Submodule.mem_sup_right

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 : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : t • x ∈ R ∙ x
s : R
hu₂ : s • x ∈ R ∙ x
⊢ ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule
Module: Mathlib.Algebra.Lie.Nilpotent

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
k✝ : ℕ
N : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
k : ℕ
hk : lowerCentralSeries R L (↥M₁) k = ⊥
⊢ IsNilpotent L ↥(M₁ ⊔ M₂)

Tactic:
obtain ⟨l, hl⟩ := IsNilpotent.nilpotent R L M₂

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
k✝ : ℕ
N : LieSubmodule R L M
M₂✝ : Type w₁
inst✝⁶ : AddCommGroup M₂✝
inst✝⁵ : Module R M₂✝
inst✝⁴ : LieRingModule L M₂✝
inst✝³ : LieModule R L M₂✝
inst✝² : LieModule R L M
M₁ M₂ : LieSubmodule R L M
inst✝¹ : IsNilpotent L ↥M₁
inst✝ : IsNilpotent L ↥M₂
k : ℕ
hk : lowerCentralSeries R L (↥M₁) k = ⊥
l : ℕ
hl : lowerCentralSeries R L (↥M₂) l = ⊥
⊢ IsNilpotent L ↥(M₁ ⊔ M₂)
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ LieModule.IsNilpotent L M

Tactic:
by
    rw [isNilpotent_iff R]
    use k * n
    simpa [hk'] using this k

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

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
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * k) = ⊥

Tactic:
rw [eq_bot_iff, ← hM]

Goal state after:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * k) ≤ lowerCentralSeries R L M k
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : nilpotencyLength L M = 0
⊢ IsTrivial L M

Tactic:
rw [nilpotencyLength_eq_zero_iff] at h

Goal state after:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ f * g

Tactic:
exact dvd_mul_left _ _

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
let _ : MulSemiringAction Q F := MulSemiringAction.compHom _ (QuotientGroup.kerLift f)

Goal state after:
G : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* Gal(F/↥(subfield G F)) := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_2 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)
Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f

Tactic:
exact spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

Tactic:
by
  have := E1.toSubalgebra.rank_sup_le_of_free E2.toSubalgebra
  rwa [← sup_toSubalgebra_of_isAlgebraic E1 E2 halg] at this

Goal state after: