mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : α
i : ℕ
h : i < count x m
⊢ 0 < count x m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
⊢ ∀ (x : α × ℕ),
    x ∈ m.toFinset.disjiUnion (fun x ↦ Finset.map { toFun := Prod.mk x, inj' := ⋯ } (Finset.range (count x m))) ⋯ ↔
      x ∈ {p | p.2 < count p.1 m}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
p : α × ℕ
h : p ∈ m.toEnumFinset
this : p.2 < count p.1 m
⊢ 0 < count p.1 m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
⊢ {x ∈ m.toEnumFinset | x.1 = a} = {a} ×ˢ Finset.range (count a m)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
by
  ext a; simp [count_map, ← Finset.filter_val, eq_comm (a := a)]

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 : IsAtom I
J : LieIdeal R ↥I
J' : LieIdeal R L :=
  let __spread.0 := Submodule.map ↑I.incl ↑J;
  { toSubmodule := __spread.0, lie_mem := ⋯ }
hJ : ¬J = ⊤
this : J' = ⊥
⊢ J = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Finset.image Prod.fst m.toEnumFinset = m.toFinset

Tactic:
by

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
⊢ χ (x + y) = χ x + χ y

Tactic:
by

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 χ ≠ ⊥
t : R
x : L
⊢ χ (t • x) = t • χ x

Tactic:
by

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 : IsAtom I
⊢ ∀ (I_1 : LieIdeal R ↥I), I_1 = ⊥ ∨ I_1 = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card > 0
h : ∀ n ≥ (filter (fun x ↦ a = x.1) s.val).card - 1, (a, n) ∉ s
⊢ {x ∈ s | x.1 = a} ⊆ {a} ×ˢ Finset.range ((filter (fun x ↦ a = x.1) s.val).card - 1)

Tactic:
by

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
⊢ χ ⁅x, y⁆ = 0

Tactic:
by

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
⊢ χ ⁅x, y⁆ = 0

Tactic:
by
    rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card > 0
h : {x ∈ s | x.1 = a} ⊆ {a} ×ˢ Finset.range ((filter (fun x ↦ a = x.1) s.val).card - 1)
⊢ (filter (fun x ↦ a = x.1) s.val).card ≤ (filter (fun x ↦ a = x.1) s.val).card - 1

Tactic:
by

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
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 ∈ s, ¬J ≤ I

Tactic:
by

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✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x + y, m⁆ - χ (x + y) • m = ⁅x, m⁆ - χ x • m + (⁅y, m⁆ - χ y • m)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card > 0
⊢ ∃ n ≥ (filter (fun x ↦ a = x.1) s.val).card - 1, (a, n) ∈ s

Tactic:
by

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✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
x : L
m n : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, m + n⁆ - χ x • (m + n) = ⁅x, m⁆ - χ x • m + (⁅x, n⁆ - χ x • n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
a : α
ha : (filter (fun x ↦ a = x.1) s.val).card > 0
n : ℕ
han : n ≥ (filter (fun x ↦ a = x.1) s.val).card - 1
hn : (a, n) ∈ s
⊢ n < count a m

Tactic:
by

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
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:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
⊢ map Prod.fst s.val ≤ m

Tactic:
by

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✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, ⁅y, m⁆ - χ y • m⁆ - χ x • (⁅y, m⁆ - χ y • m) =
    ⁅⁅x, y⁆, m⁆ - χ ⁅x, y⁆ • m + (⁅y, ⁅x, m⁆ - χ x • m⁆ - χ y • (⁅x, m⁆ - χ x • m))

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
⊢ Function.Injective fun x ↦ (x.fst, ↑x.snd)

Tactic:
by

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
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
x : L
hx : x ∈ I
⊢ ∃ y ∈ id J, ∃ z ∈ K, y + z = x

Tactic:
by

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✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
x : m.ToType
⊢ m.coeEmbedding x ∈ m.toEnumFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
x : ↥m.toEnumFinset
⊢ (↑x).2 < count (↑x).1 m

Tactic:
by

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
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
this : ⟨y, hy⟩ ∈ center R ↥J
⊢ y + z ∈ K

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x ↦ x ∈ m.toEnumFinset) = m.coeEmbedding

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Finset.map m.coeEmbedding Finset.univ = m.toEnumFinset

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ map (fun x ↦ x.fst) Finset.univ.val = m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
⊢ map (f ∘ fun x ↦ x.fst) Finset.univ.val = map f m

Tactic:
by

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✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
⊢ map (fun x ↦ f x.fst) Finset.univ.val = map f m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toEnumFinset.card = m.card

Tactic:
by

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
χ : L → R
inst✝ : LinearWeights R L M
x : L
⊢ (toEnd R L ↥(shiftedGenWeightSpace R L M χ)) x =
    (shift R L M χ).conj ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ Fintype.card m.ToType = m.card

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x, x.fst

Tactic:
by

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
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
this : ⁅↑j, z⁆ = 0 ∧ ⁅↑j, y + z⁆ = 0
⊢ ⁅j, ⟨y, hy⟩⁆ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x ∈ m.toEnumFinset, x.1

Tactic:
by

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:
ZeroMemClass.coe_zero

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
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x, f (↑x).1 (↑x).2

pp: α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : m.ToType), f x.fst ↑x.snd = f (↑(m.coeEquiv x)).1 (↑(m.coeEquiv x)).2

Tactic:
· rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : m.ToType), f x.fst ↑x.snd = f (↑(m.coeEquiv x)).1 (↑(m.coeEquiv x)).2
Module: Mathlib.Data.Multiset.Fintype

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x, f x.fst ↑x.snd

Tactic:
by

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 ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m s t : Multiset α
h : s = t
x : s.ToType
⊢ count x.fst s = count x.fst t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m s t : Multiset α
h : s = t
x : t.ToType
⊢ count x.fst t = count x.fst s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
⊢ Fintype.card (ToType 0) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
⊢ Fintype.card ∅.ToType = 0

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : Option m.ToType
⊢ count v m < count v (v ::ₘ m)

Tactic:
by

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
⊢ ∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m

Tactic:
by

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

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✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
⊢ Nonempty (Weight k L M)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
⊢ Function.LeftInverse (fun x ↦ x.elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) fun x ↦
    if h : x.fst = v ∧ ↑x.snd = count v m then none else some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩

Tactic:
by

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

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✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = χ x • m
⊢ m ∈ weightSpace M ⇑(Weight.toLinear k L M χ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
⊢ Function.RightInverse (fun x ↦ x.elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) fun x ↦
    if h : x.fst = v ∧ ↑x.snd = count v m then none else some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩

Tactic:
by

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

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✝⁴ : Module.Finite k M
inst✝³ : LieModule k L M
inst✝² : LinearWeights k L M
inst✝¹ : IsTriangularizable k L M
inst✝ : Nontrivial M
⊢ ∃ χ, Nontrivial ↥(weightSpace M ⇑χ)

Tactic:
by

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
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
this : J ⊓ I = ⊥
⊢ ⁅↑j, y + z⁆ ∈ ⊥

Tactic:
by

Goal state after:
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
hx : x.fst ≠ v
⊢ count x.fst (v ::ₘ m) = count x.fst m

Tactic:
by

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

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
hx2 : ↑x.snd = count v m
⊢ consEquiv x = none

Tactic:
by

Goal state after:
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
hx : x.fst = v
hx2 : ↑x.snd < count v m
⊢ ↑x.snd < count x.fst m

Tactic:
by

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
hx2 : ↑x.snd < count v m
⊢ consEquiv x = some ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
⊢ IsEmpty (ToType ⟦[]⟧)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
⊢ IsEmpty (map f ⟦[]⟧).ToType

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m✝ m : Multiset α
f : α → β
l : List α
⊢ ∀ (a : ToType ⟦[]⟧), ((Equiv.equivOfIsEmpty (ToType ⟦[]⟧) (map f ⟦[]⟧).ToType) a).fst = f a.fst

Tactic:
by

Goal state after: