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

Tactic:
intro j _ hj
      rw [← monomial_zero_right _, Pi.single_eq_of_ne hj]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: case inl
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₀ : nilpotencyClass a ≤ k
⊢ (∑ i ∈ range k, (↑i !)⁻¹ • a ^ i) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
sum_smul,

Goal state after:
case inl
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₀ : nilpotencyClass a ≤ k
⊢ ∑ i ∈ range k, ((↑i !)⁻¹ • a ^ i) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m
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
⊢ (∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i) • m = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i • m

Tactic:
sum_smul,

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.Derivation.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
D : LieDerivation R L L
n : ℕ
a b : L
⊢ ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅(⇑D)^[ij.1] a, (⇑D)^[ij.2] b⁆ =
    ∑ i ∈ range (n + 1), n.choose i • ⁅(⇑D)^[i] a, (⇑D)^[n - i] b⁆

Tactic:
exact sum_antidiagonal_eq_sum_range_succ (fun i j ↦ n.choose i • ⁅D^[i] a, D^[j] b⁆) n

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: case refine_3
R✝ : Type u_1
S✝ : Type u_2
T✝ : Type u_3
U✝ : Type u_4
K : Type u_5
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ (liftAlgHom q (Algebra.TensorProduct.map (AlgHom.id T T) (AlgHom.restrictScalars R (ofId S (AdjoinRoot p))))
          (1 ⊗ₜ[R] root p) ⋯).comp
      (Algebra.TensorProduct.lift (algHom T T (AdjoinRoot q)) (mapAlgHom includeRight p q ⋯) ⋯) =
    AlgHom.id T (T ⊗[R] AdjoinRoot p)

Tactic:
· ext : 3 <;> simp

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
⊢ q.natDegree < p.natDegree

Tactic:
← hp.natDegree_map (algebraMap R (AdjoinRoot p)),

Goal state after:
n : ℕ
IH :
  ∀ m < n,
    ∀ {R : Type u} [inst : CommRing R] [Nontrivial R] {p : R[X]},
      p.Monic →
        p.natDegree = m →
          ∃ S x x_1,
            ∃ (_ : Module.Finite R S) (_ : Free R S) (_ : Nontrivial S), (Polynomial.map (algebraMap R S) p).Splits
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
hn : p.natDegree = n
hpu : ¬IsUnit p
q : (AdjoinRoot p)[X]
hq : Polynomial.map (algebraMap R (AdjoinRoot p)) p = (X - C (AdjoinRoot.root p)) * q
hqm : q.Monic
this✝¹ : Free R (AdjoinRoot p)
this✝ : Module.Finite R (AdjoinRoot p)
this : Nontrivial (AdjoinRoot p)
⊢ q.natDegree < (Polynomial.map (algebraMap R (AdjoinRoot p)) p).natDegree
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Module ℚ A
B : Type u_2
F : Type u_3
inst✝³ : Ring B
inst✝² : FunLike F A B
inst✝¹ : RingHomClass F A B
inst✝ : Module ℚ B
a : A
f : F
k : ℕ
hk : a ^ k = 0
⊢ f (exp a) = exp (f a)

Tactic:
have hk' : (f a) ^ k = 0 := by simp [← map_pow, hk]

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Module ℚ A
B : Type u_2
F : Type u_3
inst✝³ : Ring B
inst✝² : FunLike F A B
inst✝¹ : RingHomClass F A B
inst✝ : Module ℚ B
a : A
f : F
k : ℕ
hk : a ^ k = 0
hk' : f a ^ k = 0
⊢ f (exp a) = exp (f a)
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
inst✝ : LieModule R L M
⊢ lowerCentralSeries R L (↥N) k = ⊥ ↔ lcs k N = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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

case refine_2
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 : lcs k N = ⊥
⊢ lowerCentralSeries R L (↥N) k = ⊥
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
| (∑ x ∈ s, (g • l x - l x) • (toFun G F) x) g'

Tactic:
rw [Finset.sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: case f
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
x : F
| g • l x * (toFun G F) x g'

Tactic:
rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]

Goal state after:
case f
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a
i : F
his : i ∈ s
g g' : G
x : F
| g • (l x * (toFun G F) x (g⁻¹ * g'))
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
⊢ restrictNormalHom K = MonoidHom.id Gal(K/F)

Tactic:
ext f x

Goal state after:
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : Gal(K/F)
x : K
⊢ ((restrictNormalHom K) f) x = ((MonoidHom.id Gal(K/F)) f) x
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
⊢ AlgEquiv.restrictNormalHom K₁ = (AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)

Tactic:
ext f x

Goal state after:
F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
inst✝⁸ : Algebra K₁ K₂
inst✝⁷ : Algebra K₁ K₃
inst✝⁶ : Algebra K₂ K₃
inst✝⁵ : IsScalarTower F K₁ K₃
inst✝⁴ : IsScalarTower F K₁ K₂
inst✝³ : IsScalarTower F K₂ K₃
inst✝² : IsScalarTower K₁ K₂ K₃
inst✝¹ : Normal F K₁
inst✝ : Normal F K₂
f : Gal(K₃/F)
x : K₁
⊢ ((AlgEquiv.restrictNormalHom K₁) f) x = (((AlgEquiv.restrictNormalHom K₁).comp (AlgEquiv.restrictNormalHom K₂)) f) x
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

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
inst✝ : Algebra.IsAlgebraic K ↥E2
this : (adjoin K (↑E1 ∪ ↑E2)).toSubalgebra = Algebra.adjoin K (↑E1.toSubalgebra ∪ ↑E2)
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
exact this

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯)
K : IntermediateField F E
hK : K.FG
⊢ P K

Tactic:
by
  obtain ⟨S, rfl⟩ := hK
  exact induction_on_adjoin_finset S P base fun K x _ hK => ih K x hK

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Basic

Goal state before:
pp: k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ ∀ (p : k'[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0

Tactic:
intro p

Goal state after:
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
p : k'[X]
⊢ p.Monic → Irreducible p → ∃ x, eval x p = 0
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
i : ι → E
x : E
⊢ x ∈ adjoin F (Set.range i) ↔ ∃ r s, x = (MvPolynomial.aeval i) r / (MvPolynomial.aeval i) s

Tactic:
by
  simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Pi

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → End R M
μ : ι → R
p : Submodule R M
hfp : ∀ (i : ι), MapsTo ⇑(f i) ↑p ↑p
h✝ : Nonempty ι
⊢ ⨅ x, Submodule.map p.subtype ((genEigenspace (LinearMap.restrict (f x) ⋯) (μ x)) ⊤) =
    Submodule.map p.subtype (⨅ i, maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Tactic:
Submodule.map_iInf _ p.injective_subtype

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥

Tactic:
rw [finrank_adjoin_eq_one_iff]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ {α} ⊆ ↑⊥ ↔ α ∈ ⊥
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤

Tactic:
iff_true_right IntermediateField.mem_top

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤

Tactic:
iff_true_right IntermediateField.mem_top

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ weightSpace M χ ≤ genWeightSpaceOf M (χ x) x

Tactic:
rw [← (LieSubmodule.toSubmodule_orderEmbedding R L M).le_iff_le]

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
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✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ (LieSubmodule.toSubmodule_orderEmbedding R L M) (weightSpace M χ) ≤
    (LieSubmodule.toSubmodule_orderEmbedding R L M) (genWeightSpaceOf M (χ x) x)
Module: Mathlib.Algebra.Lie.Weights.Cartan

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
inst✝ : LieRing.IsNilpotent ↥H
x : L
⊢ x ∈ zeroRootSubalgebra R L H ↔ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
change x ∈ rootSpace H 0 ↔ _
  simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero]

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

Goal state before:
pp: case h.mk
R : Type u_2
L : Type u_3
M : Type u_4
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✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
x : L
k : ℕ
hk : ∀ (b : ℕ), k ≤ b → ⨅ m, ((toEnd R L M) x ^ m).range = ((toEnd R L M) x ^ b).range
m : M
F : LieSubmodule R L M := posFittingComp R L M
x✝ : M ⧸ F
⊢ ((toEnd R L (M ⧸ F)) x ^ k) (Quot.mk (⇑(↑F).quotientRel) m) = 0 (Quot.mk (⇑(↑F).quotientRel) m)

Tactic:
replace hk : (toEnd R L M x ^ k) m ∈ F := by
    apply posFittingCompOf_le_posFittingComp R L M x
    simp_rw [← LieSubmodule.mem_toSubmodule, posFittingCompOf, hk k (le_refl k)]
    apply LinearMap.mem_range_self

Goal state after:
case h.mk
R : Type u_2
L : Type u_3
M : Type u_4
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✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
x : L
k : ℕ
m : M
F : LieSubmodule R L M := posFittingComp R L M
x✝ : M ⧸ F
hk : ((toEnd R L M) x ^ k) m ∈ F
⊢ ((toEnd R L (M ⧸ F)) x ^ k) (Quot.mk (⇑(↑F).quotientRel) m) = 0 (Quot.mk (⇑(↑F).quotientRel) m)
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (B x) y = ((B (x + y)) (x + y) - (B x) x - (B y) y) / 2

Tactic:
simp only [map_add, LinearMap.add_apply]

Goal state after:
M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (B x) y = ((B x) x + (B y) x + ((B x) y + (B y) y) - (B x) x - (B y) y) / 2
Module: Mathlib.LinearAlgebra.BilinearForm.Properties

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B C : BilinForm R M
hB : B.IsSymm
hC : C.IsSymm
h : ∀ (x : M), (B x) x = (C x) x
x y : M
⊢ (B x) y = (C x) y

Tactic:
hB.polarization,

Goal state after:
M : Type u_2
inst✝³ : AddCommMonoid M
R : Type u_8
inst✝² : Field R
inst✝¹ : NeZero 2
inst✝ : Module R M
B C : BilinForm R M
hB : B.IsSymm
hC : C.IsSymm
h : ∀ (x : M), (B x) x = (C x) x
x y : M
⊢ ((B (x + y)) (x + y) - (B x) x - (B y) y) / 2 = (C x) y
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
this : ⨆ x, genWeightSpace M ↑((Weight.equivSetOfPred K L M) x) = ⊤
⊢ ⨆ χ, genWeightSpace M ⇑χ = ⊤

Tactic:
exact this

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
⊢ (B.restrict p) ⟨z, hz⟩ = 0 ↔ B z = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : (B.restrict p) ⟨z, hz⟩ = 0
⊢ B z = 0

case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0
z : M
hz : z ∈ p
h : B z = 0
⊢ (B.restrict p) ⟨z, hz⟩ = 0
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsAtom I
J : LieIdeal R ↥I
y : ↥I
hy : y ∈ ↑↑J
a : L
ha : a ∈ I
b : L
hb : b ∈ sSup ({I' | IsAtom I'} \ {I})
this : ⁅b, ↑y⁆ = 0
⊢ ⁅b, ↑I.incl y⁆ ∈ Submodule.map ↑I.incl ↑J

Tactic:
erw [this]; simp only [zero_mem]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.Linear

Goal state before:
pp: k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) (x + y) =
    (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x +
      (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) y

Tactic:
map_add

Goal state after:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
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✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : CharZero R
χ : L → R
hχ : genWeightSpace M χ ≠ ⊥
x y : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x +
      (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) y =
    (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x +
      (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) y
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
obtain rfl | hI := hI.eq_or_lt

Goal state after:
case inl
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : s.sup id ≤ s.sup id
⊢ ∃ t ⊆ s, s.sup id = t.sup id

case inr
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
s : Finset (LieIdeal R L)
hs : ↑s ⊆ {I | IsAtom I}
I : LieIdeal R L
hI✝ : I ≤ s.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
⊢ ∃ t ⊆ s, I = t.sup id
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
⊢ m₁.toEnumFinset ⊆ m₂.toEnumFinset

Tactic:
intro p

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ m₁.toEnumFinset → p ∈ m₂.toEnumFinset
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁ ≤ m₂
⊢ m₁.toEnumFinset ⊆ m₂.toEnumFinset

Tactic:
by
  intro p
  simp only [Multiset.mem_toEnumFinset]
  exact lt_of_le_of_lt' (Multiset.le_iff_count.mp h p.1)

Goal state after:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ consEquiv x = some ⟨x.fst, Fin.cast ⋯ x.snd⟩

Tactic:
by
  simp [consEquiv, hx]
  rfl

Goal state after:
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
hf : f.natDegree ≠ 0
g : K[X]
hg : f = f.factor * g
⊢ (map (AdjoinRoot.of f.factor) f).IsRoot (AdjoinRoot.root f.factor)

Tactic:
rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
J : LieIdeal R L
hJ : IsAtom J
hJ' : J ≤ I
x y : ↥J
this : ↑⁅⟨↑x, ⋯⟩, ⟨↑y, ⋯⟩⁆ = ↑0
⊢ ⁅↑x, ↑y⁆ = 0

Tactic:
exact this

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ IsSemisimple R L

Tactic:
by
  constructor
  · simp
  · simpa using sSupIndep_singleton _
  · intro I hI₁ hI₂
    apply IsSimple.non_abelian (R := R) (L := L)
    rw [IsSimple.isAtom_iff_eq_top] at hI₁
    rwa [hI₁, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI₂

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
ι : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
⊢ IsNilpotent A ↔ ∀ (i : ι), ∃ n, (A ^ n).row i = 0

Tactic:
rw [← isNilpotent_transpose_iff, isNilpotent_iff]
  refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩
  · obtain ⟨n, hn⟩ := h (Pi.single i 1)
    exact ⟨n, by simpa [← transpose_pow] using hn⟩
  · choose n hn using h
    suffices ∀ i, (A ^ ⨆ j, n j) i = 0 from ⟨⨆ j, n j, by simp [mulVec_eq_sum, this]⟩
    exact fun i ↦ pow_row_eq_zero_of_le (hn i) (Finite.le_ciSup n i)

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
this : LinearMap.ker f = ⊤
⊢ f = 0

Tactic:
LinearMap.ker_eq_top

Goal state after:
K : Type u_3
V : Type u_4
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
this : f = 0
⊢ f = 0