mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = C f.leadingCoeff * 0
hi : minpoly K x = 0
⊢ f = 0

Tactic:
mul_zero

Goal state after:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : K[X]
hs : (Polynomial.map (algebraMap K L) f).Splits
this : (Polynomial.map (algebraMap K L) f).degree ≠ 0
x : L
hx : (aeval x) f = 0
key : f = 0
hi : minpoly K x = 0
⊢ f = 0
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ -⁅h, f⁆ = 2 • f

Tactic:
neg_eq_iff_eq_neg,

Goal state after:
L : Type u_2
inst✝ : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ ⁅h, f⁆ = -(2 • f)
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case h
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✝ : LieRing.IsNilpotent L
x : L
φ : Module.End R M := ⋯
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := ⋯
f₂ : Module.End R (L ⊗[R] M) := ⋯
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
h₂ : φ ∘ₗ ↑(toModuleHom R L M) = ↑(toModuleHom R L M) ∘ₗ (f₁ + f₂)
q : Module.End R (L ⊗[R] M)
hq : f₂ ^ (N + k) = (f₁ + f₂) ^ k * q
⊢ (φ ^ k) ((toModuleHom R L M) (q (y ⊗ₜ[R] m))) = ⁅y, (φ ^ (N + k)) m⁆

Tactic:
change (φ ^ k).comp ((toModuleHom R L M : L ⊗[R] M →ₗ[R] M)) _ = _

Goal state after:
case h
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✝ : LieRing.IsNilpotent L
x : L
φ : Module.End R M := (toEnd R L M) x
y : L
k N : ℕ
m : M
hm : ∀ (i : ℕ), ∃ y, (φ ^ i) y = (φ ^ (N + k)) m
f₁ : Module.End R (L ⊗[R] M) := LinearMap.rTensor M ((LieAlgebra.ad R L) x)
f₂ : Module.End R (L ⊗[R] M) := LinearMap.lTensor L φ
hN : f₁ ^ N = 0
h₁ : Commute f₁ f₂
h₂ : φ ∘ₗ ↑(toModuleHom R L M) = ↑(toModuleHom R L M) ∘ₗ (f₁ + f₂)
q : Module.End R (L ⊗[R] M)
hq : f₂ ^ (N + k) = (f₁ + f₂) ^ k * q
⊢ ((φ ^ k) ∘ₗ ↑(toModuleHom R L M)) (q (y ⊗ₜ[R] m)) = ⁅y, (φ ^ (N + k)) m⁆
Module: Mathlib.Algebra.Lie.Weights.Basic

Goal state before:
pp: case succ
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
x : L
k : ℕ
m : M
l : ℕ
ih : ((toEnd R L M) x ^ l) m ∈ lowerCentralSeries R L M l
⊢ ((toEnd R L M) x ^ (l + 1)) m ∈ lowerCentralSeries R L M (l + 1)

Tactic:
| succ l ih =>

Goal state after:
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
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
χ : L → R
x : L
this : (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id) = 0
⊢ (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = finrank R ↥(genWeightSpace M χ) • χ x

Tactic:
map_sub,

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
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
χ : L → R
x : L
this :
  (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) -
      (trace R ↥(genWeightSpace M χ)) (χ x • LinearMap.id) =
    0
⊢ (trace R ↥(genWeightSpace M χ)) ((toEnd R L ↥(genWeightSpace M χ)) x) = finrank R ↥(genWeightSpace M χ) • χ x
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
j : n
a✝ : j ∈ s
hij : j ≠ i
⊢ w j * 0 = 0

Tactic:
mul_zero

Goal state after:
V : Type u_5
K : Type u_6
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : Type w
B : BilinForm K V
v : n → V
hv₁ : B.iIsOrtho v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
j : n
a✝ : j ∈ s
hij : j ≠ i
⊢ 0 = 0
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case h.right.a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
⊢ ∀ b ∈ C, b ≤ sSup (sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

Tactic:
intro c

Goal state after:
case h.right.a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
⊢ c ∈ C → c ≤ sSup (sSup {x | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: 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
⊢ x ∈ (domRestrict B W).range.dualCoannihilator ↔ x ∈ B.orthogonal W

Tactic:
constructor <;> rw [mem_orthogonal_iff]

Goal state after:
case mp
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
⊢ x ∈ (domRestrict B W).range.dualCoannihilator → ∀ n ∈ W, (B n) x = 0

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
⊢ (∀ n ∈ W, (B n) x = 0) → x ∈ (domRestrict B W).range.dualCoannihilator
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
W : Submodule K V
⊢ finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W

Tactic:
have := finrank_add_finrank_orthogonal' (B := B) W
  rw [hB.ker_eq_bot, inf_bot_eq, finrank_bot, add_zero] at this
  lia

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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
h : ∀ (x y : L), Commute ((toEnd R L M) x) ((toEnd R L M) y)
χ : L → R
x y : L
hχ : ¬↑(⨅ x, genWeightSpaceOf M (χ x) x) = ↑⊥
⊢ χ (x + y) = χ x + χ y

Tactic:
genWeightSpaceOf,

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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
h : ∀ (x y : L), Commute ((toEnd R L M) x) ((toEnd R L M) y)
χ : L → R
x y : L
hχ : ¬↑(⨅ x, { toSubmodule := ((toEnd R L M) x).maxGenEigenspace (χ x), lie_mem := ⋯ }) = ↑⊥
⊢ χ (x + y) = χ x + χ y
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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
t : R
x : L
hχ : ¬↑(⨅ x, genWeightSpaceOf M (χ x) x) = ↑⊥
⊢ χ (t • x) = t • χ x

Tactic:
genWeightSpaceOf,

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✝² : IsLieAbelian L
inst✝¹ : IsDomain R
inst✝ : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), genWeightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
t : R
x : L
hχ : ¬↑(⨅ x, { toSubmodule := ((toEnd R L M) x).maxGenEigenspace (χ x), lie_mem := ⋯ }) = ↑⊥
⊢ χ (t • x) = t • χ x
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: ι : 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
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
⊢ ⁅y, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
have (i : ι) (x : L) (hx : x ∈ lieSpan R L (range b.f)) :
      ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower := by
    induction hx using LieSubalgebra.lieSpan_induction with
    | mem u hu =>
      obtain ⟨j, rfl⟩ := hu
      rcases eq_or_ne i j with rfl | hij
      · rw [(b.sl2 i).lie_e_f]
        apply LieSubmodule.mem_sup_left
        nth_rw 1 [mem_toLieSubmodule, b.cartan_eq_lieSpan]
        exact LieSubalgebra.subset_lieSpan <| mem_range_self i
      · simp [b.lie_e_f_ne _ _ hij]
    | zero => simp
    | add u v _ _ hu hv => rw [lie_add]; exact add_mem hu hv
    | smul t u _ hu => rw [lie_smul]; exact SMulMemClass.smul_mem t hu
    | lie u v hu hv hu' hv' =>
      obtain ⟨w₁, hw₁, w₂, hw₂, hwu⟩ : ∃ y ∈ H, ∃ z ∈ b.borelLower, y + z = ⁅b.e i, u⁆ := by
        simpa only [LieSubmodule.mem_sup] using! hu'
      obtain ⟨w₃, hw₃, w₄, hw₄, hwv⟩ : ∃ y ∈ H, ∃ z ∈ b.borelLower, y + z = ⁅b.e i, v⁆ := by
        simpa only [LieSubmodule.mem_sup] using! hv'
      rw [leibniz_lie, ← hwu, ← hwv, lie_add, add_lie, ← add_assoc]
      repeat apply add_mem
      · exact LieSubmodule.mem_sup_right <| b.borelLower.lie_mem (x := ⟨w₁, hw₁⟩) hv
      · exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hw₂ hv
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| b.borelLower.lie_mem (x := ⟨w₃, hw₃⟩) hu
      · rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hw₄ hu

Goal state after:
ι : 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
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
⊢ ⁅y, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : m.ToType
⊢ 0 < count x.fst m

Tactic:
by have := x.2.2; lia

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 * (toEnd R L ↥(genWeightSpace M χ)) y -
        (toEnd R L ↥(genWeightSpace M χ)) y * (toEnd R L ↥(genWeightSpace M χ)) x) =
    0

Tactic:
map_sub,

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 * (toEnd R L ↥(genWeightSpace M χ)) y) -
      (LinearMap.trace R ↥(genWeightSpace M χ))
        ((toEnd R L ↥(genWeightSpace M χ)) y * (toEnd R L ↥(genWeightSpace M χ)) x) =
    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
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
this : I ≤ K
⊢ ∃ t ⊆ s, I = t.sup id

Tactic:
obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩

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

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
inst✝¹ : LinearWeights R L M
inst✝ : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial ↥(shiftedGenWeightSpace R L M ⇑χ)
m : M
property✝ : m ∈ shiftedGenWeightSpace R L M ⇑χ
hm₁✝ : ⟨m, property✝⟩ ∈ maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M ⇑χ)
hm₂ : ⟨⟨m, property✝⟩, hm₁✝⟩ ≠ 0
hm₁ : ∀ (x : L), ⁅x, ⟨m, property✝⟩⁆ = 0
⊢ ∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m

Tactic:
Subtype.ext_iff,

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
inst✝¹ : LinearWeights R L M
inst✝ : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial ↥(shiftedGenWeightSpace R L M ⇑χ)
m : M
property✝ : m ∈ shiftedGenWeightSpace R L M ⇑χ
hm₁✝ : ⟨m, property✝⟩ ∈ maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M ⇑χ)
hm₂ : ⟨⟨m, property✝⟩, hm₁✝⟩ ≠ 0
hm₁ : ∀ (x : L), ↑⁅x, ⟨m, property✝⟩⁆ = ↑0
⊢ ∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
⊢ ↑x.snd < count x.fst m

Tactic:
by_cases hv : x.1 = v

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
hv : x.fst = v
⊢ ↑x.snd < count x.fst m

case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
h : ¬(x.fst = v ∧ ↑x.snd = count v m)
hv : ¬x.fst = v
⊢ ↑x.snd < count x.fst m
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
_x : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' I ≤ s.sup id
a✝⁵ :
  ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' I ≤ s.sup id),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun s a ↦ PSigma.casesOn a fun a a_1 ↦ s.card) y _x →
      ∃ t ⊆ y.1, I = t.sup id
s : Finset (LieIdeal R L)
a✝⁴ : (_ : ↑s ⊆ {I | IsAtom I}) ×' I ≤ s.sup id
a✝³ :
  ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' I ≤ s.sup id),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun s a ↦ PSigma.casesOn a fun a a_1 ↦ s.card) y ⟨s, a✝⁴⟩ →
      ∃ t ⊆ y.1, I = t.sup id
a✝² : ↑s ⊆ {I | IsAtom I}
a✝¹ : I ≤ s.sup id
a✝ :
  ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' I ≤ s.sup id),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun s a ↦ PSigma.casesOn a fun a a_1 ↦ s.card) y
        ⟨s, ⟨a✝², a✝¹⟩⟩ →
      ∃ t ⊆ y.1, I = t.sup id
S : Set (LieIdeal R L) := {I | IsAtom I}
hI : I < s.sup id
J : LieIdeal R L
h✝ : J ∈ s ∧ ¬J ≤ I
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
this : I ≤ K
⊢ (s.erase J).card < s.card

Tactic:
decreasing_by exact Finset.card_lt_card hs'

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

Goal state before:
pp: k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
j : Monics k × ℕ
hj : j ∈ v.support
⊢ (toSplittingField (Finset.image Prod.fst v.support)) (v j) * 0 = 0

Tactic:
mul_zero

Goal state after:
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
j : Monics k × ℕ
hj : j ∈ v.support
⊢ 0 = 0
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi))

Tactic:
map_mul

Goal state after:
case mul_X
k : Type u
inst✝ : Field k
p : MvPolynomial (Vars k) k
fi : Vars k
ih :
  ∀ (z : AlgebraicClosure k), (Ideal.Quotient.mk (maxIdeal k)) p = z → IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p)
z : AlgebraicClosure k
hp : (Ideal.Quotient.mk (maxIdeal k)) (p * MvPolynomial.X fi) = z
⊢ IsIntegral k ((Ideal.Quotient.mk (maxIdeal k)) p * (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi))
Module: Mathlib.RingTheory.Finiteness.Nilpotent

Goal state before:
pp: case h.smul
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
a✝¹ : R
x✝ : M
hx✝ : x✝ ∈ Submodule.span R ↑S
a✝ : (f ^ S.sup g) x✝ = 0 x✝
⊢ (f ^ S.sup g) (a✝¹ • x✝) = 0 (a✝¹ • x✝)

Tactic:
| smul =>

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ g m = μ • m

Tactic:
rw [f.mem_genEigenspace] at hm
  obtain ⟨l, -, hm⟩ := hm
  rw [← f.mem_genEigenspace_nat] at hm
  set p := f.genEigenspace μ l
  have h₁ : MapsTo g p p := mapsTo_genEigenspace_of_comm hfg μ l
  have h₂ : MapsTo (g - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ l
  have h₃ : MapsTo (f - g) p p :=
    mapsTo_genEigenspace_of_comm (Commute.sub_right rfl hfg) μ l
  have h₄ : MapsTo (f - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ l
  replace hfg : Commute (f - algebraMap R (End R M) μ) (f - g) :=
    (Commute.sub_right rfl hfg).sub_left <| Algebra.commute_algebraMap_left μ (f - g)
  suffices IsNilpotent ((g - algebraMap R (End R M) μ).restrict h₂) by
    replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
      eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
    simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩
  simpa [LinearMap.restrict_sub h₄ h₃] using (LinearMap.restrict_commute hfg h₄ h₃).isNilpotent_sub
    (f.isNilpotent_restrict_sub_algebraMap μ l) (Module.End.isNilpotent.restrict h₃ hnil)

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

Goal state before:
pp: case smul
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
a✝¹ : R
x✝ : ↥H
hx✝ : x✝ ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
a✝ : (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x✝) = 0
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) (a✝¹ • x✝)) = 0

Tactic:
| smul =>

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

Goal state before:
pp: R : Type u_1
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✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ))
      ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
          (χ x • LinearMap.id) ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
        ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (χ y • LinearMap.id) - (χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id))) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
map_sub,

Goal state after:
R : Type u_1
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✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this :
  (trace R ↥(genWeightSpace M χ))
        ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y -
          (χ x • LinearMap.id) ∘ₗ (toEnd R L ↥(genWeightSpace M χ)) y) -
      (trace R ↥(genWeightSpace M χ))
        ((toEnd R L ↥(genWeightSpace M χ)) x ∘ₗ (χ y • LinearMap.id) - (χ x • LinearMap.id) ∘ₗ (χ y • LinearMap.id)) =
    0
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)