mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Semisimple

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝³ : Module.Finite K R
this✝² : Module.Finite R S
this✝¹ : Module.Finite K S
this✝ : IsArtinianRing R
this : IsReduced R
⊢ IsReduced S

Tactic:
S,

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
K : Type u_3
inst✝³ : Field K
inst✝² : Module K M
f g : End K M
inst✝¹ : FiniteDimensional K M
inst✝ : PerfectField K
comm : Commute f g
hf : f.IsSemisimple
hg : g.IsSemisimple
a : End K M
ha : a ∈ K[f, g]
R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}
S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))
this✝³ : Module.Finite K R
this✝² : Module.Finite R S
this✝¹ : Module.Finite K S
this✝ : IsArtinianRing R
this : IsReduced R
⊢ IsReduced (AdjoinRoot (map (algebraMap K R) (minpoly K g)))
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
i : ℕ × ℕ
hi : i ∈ {ij ∈ R2N ×ˢ R2N | ¬(ij.1 ≤ N ∧ ij.2 ≤ N)}
⊢ ((↑i.1!)⁻¹ * (↑i.2!)⁻¹) • (a ^ i.1 * b ^ i.2) = 0

Tactic:
simp only [not_and, not_le, mem_filter] at hi
    cases le_or_gt (N + 1) i.1 with
      | inl h => rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
      | inr h => rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]

Goal state after:
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
⊢ s = s₀

Tactic:
have hsf : Commute s (n₁ + s₁) := heq ▸ hc.symm.add_right (Commute.refl s)

Goal state after:
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₁)
⊢ s = s₀
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_3
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 : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ((bracket' R A L L) x) x = 0 → ((bracket' R A L L) y) y = 0 → ((bracket' R A L L) (x + y)) (x + y) = 0

Tactic:
intro z₁ z₂ h₁ h₂
    suffices bracket' R A L L z₁ z₂ + bracket' R A L L z₂ z₁ = 0 by
      rw [map_add, map_add, LinearMap.add_apply, LinearMap.add_apply, h₁, h₂,
        zero_add, add_zero, add_comm, this]
    refine z₁.induction_on ?_ ?_ ?_
    · simp only [map_zero, add_zero, LinearMap.zero_apply]
    · intro a₁ l₁; refine z₂.induction_on ?_ ?_ ?_
      · simp only [map_zero, add_zero, LinearMap.zero_apply]
      · intro a₂ l₂
        simp only [← lie_skew l₂ l₁, mul_comm a₁ a₂, TensorProduct.tmul_neg, bracket'_tmul,
          add_neg_cancel]
      · intro y₁ y₂ hy₁ hy₂
        simp only [hy₁, hy₂, add_add_add_comm, add_zero, LinearMap.add_apply, map_add]
    · intro y₁ y₂ hy₁ hy₂
      simp only [add_add_add_comm, hy₁, hy₂, add_zero, LinearMap.add_apply, map_add]

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

Goal state before:
pp: case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : (LieSubmodule.Quotient.mk' H.toLieSubmodule) ⁅⟨y, hy⟩, x⁆ = 0
⊢ ⁅y, x⁆ ∈ H

Tactic:
LieSubmodule.Quotient.mk_eq_zero

Goal state after:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : ⁅⟨y, hy⟩, x⁆ ∈ H.toLieSubmodule
⊢ ⁅y, x⁆ ∈ H
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
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False

Tactic:
LieIdeal.derivedSeries_eq_top n contra

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : ⊤ = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : derivedLengthOfIdeal R L I = k + 1
⊢ IsLieAbelian
    ↥(match k + 1 with
      | 0 => ⊥
      | k.succ => derivedSeriesOfIdeal R L k I)

Tactic:
· rw [derivedSeries_of_derivedLength_succ] at h; exact h.1

Goal state after:
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f✝ : S[X]
x : S
f g : S[X]
ihf : eval (m • x) (m • f) = m • eval x f
ihg : eval (m • x) (m • g) = m • eval x g
⊢ eval (m • x) (m • (f + g)) = m • eval x (f + g)

Tactic:
rw [smul_add, eval_add, ihf, ihg, eval_add, smul_add]

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

Goal state before:
pp: R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this✝ : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
⊢ LieModule.IsNilpotent L₂ M

Tactic:
have surj_id : Function.Surjective (LinearMap.id : M →ₗ[R] M) := Function.surjective_id

Goal state after:
R : Type u₁
L : Type u₂
L₂ : Type u₃
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
hf : Surjective ⇑f
h : LieAlgebra.IsEngelian R L
M : Type u₄
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L₂ M
_i4 : LieModule R L₂ M
h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)
this✝ : LieRingModule L M := LieRingModule.compLieHom M f
this : LieModule R L M := compLieHom M f
hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
surj_id : Surjective ⇑LinearMap.id
⊢ LieModule.IsNilpotent L₂ M
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 : L
m : M
⊢ ∃ k, ((toEnd R L M) x ^ k) m = 0

Tactic:
obtain ⟨k, hk⟩ := exists_forall_pow_toEnd_eq_zero 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
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
x : L
m : M
k : ℕ
hk : ∀ (x : L), (toEnd R L M) x ^ k = 0
⊢ ∃ k, ((toEnd R L M) x ^ k) m = 0
Module: Mathlib.FieldTheory.Finiteness

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀

Tactic:
by
  let b := Basis.ofVectorSpace K V
  rw [← b.mk_eq_rank'', lt_aleph0_iff_set_finite]
  constructor
  · intro
    exact (Basis.ofVectorSpaceIndex.linearIndependent K V).set_finite_of_isNoetherian
  · intro hbfinite
    refine
      @isNoetherian_of_linearEquiv K K (⊤ : Submodule K V) V _ _ _ _ _ _ (RingHom.id K) _ _ _
        (LinearEquiv.ofTop _ rfl) (id ?_)
    refine isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩
    rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]

Goal state after:
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
x : ↥(subfield M F)
⊢ m • Polynomial.C x = Polynomial.C x

Tactic:
Polynomial.smul_C,

Goal state after:
M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
x : ↥(subfield M F)
⊢ Polynomial.C (m • x) = Polynomial.C x
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
n : ℕ
x : ↥(subfield M F)
x✝ : m • (Polynomial.C x * Polynomial.X ^ n) = Polynomial.C x * Polynomial.X ^ n
⊢ m • Polynomial.C x * m • Polynomial.X ^ (n + 1) = Polynomial.C x * Polynomial.X ^ (n + 1)

Tactic:
Polynomial.smul_C,

Goal state after:
M : Type u
inst✝² : Monoid M
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
n : ℕ
x : ↥(subfield M F)
x✝ : m • (Polynomial.C x * Polynomial.X ^ n) = Polynomial.C x * Polynomial.X ^ n
⊢ Polynomial.C (m • x) * m • Polynomial.X ^ (n + 1) = Polynomial.C x * Polynomial.X ^ (n + 1)
Module: Mathlib.FieldTheory.IntermediateField.Algebraic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
⊢ l ∈ extendScalars ⋯

Tactic:
eq_of_le_of_finrank_le''
    ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
F E : IntermediateField K L
inst✝ : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
⊢ l ∈ extendScalars h_le
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
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³ * x✝², ⋯⟩

Tactic:
convert! congr_arg₂ (· * ·) h₁ h₂ <;> rw [← map_mul]

Goal state after:
case e'_2
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)

case e'_3
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Semiring K
inst✝ : Algebra F K
s : Set E
φ₁ φ₂ : ↥(adjoin F s) →ₐ[F] K
h : ∀ (x : E) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin F s)
x : E
hx : x ∈ adjoin F s
x✝³ x✝² : E
x✝¹ : x✝³ ∈ adjoin F s
x✝ : x✝² ∈ adjoin F s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit ((aeval a) p)

Tactic:
h_eval_p

Goal state after:
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : p.Monic
h_eval_p : (aeval a) p = 0
⊢ ¬IsUnit 0
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
σ : Lifts F E K
hσ✝ : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : ↑(insert ⊥ c) → IntermediateField F E := fun i ↦ (↑i).carrier
x : ↥σ.carrier
⊢ (Subalgebra.iSupLift (fun x ↦ (↑x).carrier.toSubalgebra) ⋯ (fun x ↦ (↑x).emb) ⋯ (⨆ x, (↑x).carrier.toSubalgebra) ⋯)
      (↑((⨆ i, (↑i).carrier).equivOfEq (⨆ i, (↑i).carrier.toSubalgebra) ⋯) ((inclusion ⋯) x)) =
    σ.emb x

Tactic:
exact Subalgebra.iSupLift_inclusion (K := (toSubalgebra <| t ·))
      (i := ⟨σ, hσ⟩) x (le_iSup (toSubalgebra <| t ·) ⟨σ, hσ⟩)

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

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
hm₂_aux : ∀ (i : K), m i ∈ (f.genEigenspace i) k
⊢ m μ ∈ p

Tactic:
simp_rw [Module.End.mem_genEigenspace] at hm₂_aux

Goal state after:
case pos
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
hm₂_aux : ∀ (i : K), ∃ l, ↑l ≤ k ∧ m i ∈ ((f - i • 1) ^ l).ker
⊢ m μ ∈ p
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : L
hx : IsIntegral K x
hy : IsIntegral K y
this✝ : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K ↥K⟮y⟯
⊢ FiniteDimensional K ↥(K⟮x⟯ ⊔ K⟮y⟯)

Tactic:
exact finiteDimensional_sup K⟮x⟯ K⟮y⟯

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

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
inst✝ : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ ⁅2 • e, m⁆ = 0

Tactic:
← t.lie_h_e_nsmul,

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
inst✝ : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ ⁅⁅h, e⁆, m⁆ = 0
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case refine_3
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1
t₁ t₂ : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
k₁ : ℕ
hk₁ :
  (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k₁) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) t₁)) = 0
k₂ : ℕ
hk₂ :
  (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k₂) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) t₂)) = 0
⊢ ∃ k,
    (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k)
        (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) (t₁ + t₂))) =
      0

Tactic:
use max k₁ k₂

Goal state after:
case h
R : Type u_2
L : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : LieRing L
inst✝¹² : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : LieRingModule L M₁
inst✝⁸ : LieModule R L M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : LieRingModule L M₂
inst✝⁴ : LieModule R L M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : LieRingModule L M₃
inst✝ : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ := ⋯
t₁ t₂ : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)
k₁ : ℕ
hk₁ :
  (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k₁) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) t₁)) = 0
k₂ : ℕ
hk₂ :
  (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ k₂) (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) t₂)) = 0
⊢ (((toEnd R L M₃) x - (χ₁ + χ₂) • 1) ^ max k₁ k₂)
      (g ((TensorProduct.map 𝕎(M₁, χ₁, x).subtype 𝕎(M₂, χ₂, x).subtype) (t₁ + t₂))) =
    0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : (↑(i + 1) = 0 ∨ n = i) ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False

Tactic:
Nat.cast_eq_zero

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
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
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : (i + 1 = 0 ∨ n = i) ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False
Module: Mathlib.Algebra.Lie.Semisimple.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
⊢ radical R L = ⊥

Tactic:
simpa only [radical_eq_top_of_isSolvable] using Subsingleton.elim ⊤ ⊥

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

Goal state before:
pp: case lie
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x y : L
hx : x ∈ H
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
hv' : ⁅x, v⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅x, ⁅u, v⁆⁆ ∈ lieSpan R L (range b.e)

Tactic:
rw [leibniz_lie, ← lie_skew _ v, neg_add_eq_sub]

Goal state after:
case lie
ι : Type u_1
R : Type u_2
L : Type u_3
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
b : Basis ι H
x y : L
hx : x ∈ H
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
hv' : ⁅x, v⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅u, ⁅x, v⁆⁆ - ⁅v, ⁅x, u⁆⁆ ∈ lieSpan R L (range b.e)
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: case mpr
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : BilinForm K V
W : Subspace K V
x : V
hx : x ∈ W ⊓ ker B
⊢ ∃ y, (domRestrict B W) y = 0 ∧ (Submodule.subtype W) y = x

Tactic:
exact ⟨⟨x, hx.1⟩, hx.right, rfl⟩

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

Goal state before:
pp: 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
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ ⁅↑j, z⁆ ∈ ⊥ ∧ ⁅↑j, y + z⁆ = 0

Tactic:
← LieSubmodule.mem_bot (R := R) (L := L)

Goal state after:
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
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := s.erase J
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := s'.sup id
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ ⁅↑j, z⁆ ∈ ⊥ ∧ ⁅↑j, y + z⁆ ∈ ⊥
Module: Mathlib.FieldTheory.SplittingField.Construction

Goal state before:
pp: K : Type v
inst✝ : Field K
f : K[X]
⊢ Irreducible (if H : ∃ g, Irreducible g ∧ g ∣ f then Classical.choose H else X)

Tactic:
split_ifs with H

Goal state after:
case pos
K : Type v
inst✝ : Field K
f : K[X]
H : ∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible (Classical.choose H)

case neg
K : Type v
inst✝ : Field K
f : K[X]
H : ¬∃ g, Irreducible g ∧ g ∣ f
⊢ Irreducible X
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
⊢ 1 ∉ spanCoeffs k

Tactic:
spanCoeffs,

Goal state after:
k : Type u
inst✝ : Field k
⊢ 1 ∉ Ideal.span (Set.range fun fn ↦ (subProdXSubC fn.1).coeff fn.2)
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
change algebraMap k _ _ = _; rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]

Goal state after:
Module: Mathlib.Algebra.Lie.Derivation.Killing

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule).Nondegenerate

Tactic:
by
  convert! LieAlgebra.IsKilling.killingForm_nondegenerate R 𝕀
  exact killingForm_restrict_range_ad R L

Goal state after: