mathlib-initiative/mathlib-tactics huggingface dataset:
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
m : M
⊢ ∀ (a : L),
    (∀ (b : a ∈ ⊤), ∃ k, (((toEnd R (↥⊤) M) ⟨a, b⟩ - (χ ∘ ⇑⊤.incl) ⟨a, b⟩ • 1) ^ k) m = 0) ↔
      ∃ k, (((toEnd R L M) a - χ a • 1) ^ k) m = 0

Tactic:
simp

Goal state after:
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✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
k : ℕ
hk : rootSpace H 0 ≤ LieSubmodule.ucs k ⊥
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule

Tactic:
simp

Goal state after:
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
inst✝ : IsNoetherian R L
a✝ : H.IsCartanSubalgebra
⊢ zeroRootSubalgebra R L H = H

Tactic:
simp

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

Goal state before:
pp: case zero
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
⊢ ((toEnd R L M) x ^ 0) m ∈ lowerCentralSeries R L M 0

Tactic:
simp

Goal state after:
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
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
α : ↥H → R
x : ↥H
this : x ∈ corootSpace α ↔ ↑x ∈ LieSubmodule.map H.toLieSubmodule.incl (corootSpace α)
⊢ ↑x ∈ Submodule.span R {x | ∃ a b, ⁅↑a, ↑b⁆ = x} ↔
    ↑x ∈ Submodule.span R {x | ∃ y ∈ ↑(rootSpace H α), ∃ z ∈ ↑(rootSpace H (-α)), ⁅y, z⁆ = x}

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : BilinForm R M
x✝ y✝ : M
⊢ (((flipHom ≪≫ₗ flipHom) A) x✝) y✝ = (((LinearEquiv.refl R (BilinForm R M)) A) x✝) y✝

Tactic:
simp

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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : m ∈ genWeightSpace M χ
x : L
x✝ : M
⊢ (((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f) x✝ = (↑f ∘ₗ ((toEnd R L M) x - χ x • 1)) x✝

Tactic:
simp

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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective ⇑f
m : M
hm : ∀ (x : L), ∃ k, (((toEnd R L M₂) x - χ x • 1) ^ k) (f m) = 0
x : L
x✝ : M
⊢ (((toEnd R L M₂) x - χ x • 1) ∘ₗ ↑f) x✝ = (↑f ∘ₗ ((toEnd R L M) x - χ x • 1)) x✝

Tactic:
simp

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

Goal state before:
pp: L : Type u_2
inst✝⁵ : LieRing L
K : Type u_4
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
⊢ LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔ ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H ⇑α

Tactic:
by
  refine le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ _ ↦ inf_le_left))
  conv_lhs => rw [lieIdeal_eq_iSup_inf_genWeightSpace]
  exact iSup_le fun α ↦ by
    by_cases hα : α.IsZero
    · rw [show genWeightSpace L (α : H → K) = H.toLieSubmodule by ext; simp [hα.eq]]
      exact le_sup_left
    · exact le_sup_of_le_right (le_iSup₂_of_le α hα le_rfl)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
⊢ x ∈ Submodule.span R (Set.range ⇑b)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h : ∀ (i j : ι), (B (b i)) (b j) = (B (b j)) (b i)
x y : M
fx : M → R
tx : Finset M
ix : ↑tx ⊆ Set.range ⇑b
hx : ∑ a ∈ tx, fx a • a = x
⊢ y ∈ Submodule.span R (Set.range ⇑b)

Tactic:
simp

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

Goal state before:
pp: case e'_2
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
M₂ : Type u_5
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
e : M ≃ₗ⁅R,L⁆ M₂
m✝ : M₂
⊢ m✝ ∈ posFittingComp R L M₂ ↔
    m✝ ∈ LieSubmodule.map LieModuleHom.id (LieSubmodule.map (e.comp e.symm.toLieModuleHom) (posFittingComp R L M₂))

Tactic:
simp

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

Goal state before:
pp: case mem.zero
ι : 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
i : ι
⊢ ⁅0, b.e i⁆ ∈ lieSpan R L (range b.e)

Tactic:
simp

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

Goal state before:
pp: case zero
ι : 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
⊢ ⁅x, 0⁆ ∈ lieSpan R L (range b.e)

Tactic:
simp

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

Goal state before:
pp: case zero
ι : 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)
i : ι
x : L
⊢ ⁅b.e i, 0⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
simp

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
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x u v : L
hu : u ∈ lieSpan R L (range b.f)
hv : v ∈ lieSpan R L (range b.f)
hu' : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv' : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
w₁ : L
hw₁ : w₁ ∈ H
w₂ : L
hw₂ : w₂ ∈ b.borelLower
hwu : w₁ + w₂ = ⁅b.e i, u⁆
w₃ : L
hw₃ : w₃ ∈ H
w₄ : L
hw₄ : w₄ ∈ b.borelLower
hwv : w₃ + w₄ = ⁅b.e i, v⁆
⊢ ⁅⁅b.e i, u⁆, v⁆ + ⁅u, ⁅b.e i, v⁆⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
← hwu,

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
y z : L
hy : y ∈ lieSpan R L (range b.e)
hz : z ∈ lieSpan R L (range b.f)
i : ι
x u v : L
hu : u ∈ lieSpan R L (range b.f)
hv : v ∈ lieSpan R L (range b.f)
hu' : ⁅b.e i, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
hv' : ⁅b.e i, v⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
w₁ : L
hw₁ : w₁ ∈ H
w₂ : L
hw₂ : w₂ ∈ b.borelLower
hwu : w₁ + w₂ = ⁅b.e i, u⁆
w₃ : L
hw₃ : w₃ ∈ H
w₄ : L
hw₄ : w₄ ∈ b.borelLower
hwv : w₃ + w₄ = ⁅b.e i, v⁆
⊢ ⁅w₁ + w₂, v⁆ + ⁅u, ⁅b.e i, v⁆⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
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
⊢ ∀ b ∈ s, b ≠ i → w b * (B (v b)) (v i) = 0

Tactic:
intro j

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
⊢ j ∈ s → j ≠ i → w j * (B (v j)) (v i) = 0
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
B : BilinForm R M
x✝ : M
⊢ x✝ ∈ B.orthogonal ⊥ ↔ x✝ ∈ ⊤

Tactic:
simp

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
χ : Weight R L M
⊢ toLinear R L M χ ≠ 0 ↔ χ.IsNonZero

Tactic:
simp

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

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

Tactic:
simp

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✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Tactic:
simp

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:
le_iff_count,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
s : Finset (α × ℕ)
hsm : s ⊆ m.toEnumFinset
⊢ ∀ (a : α), count a (map Prod.fst s.val) ≤ count a m
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⁆) = 0

Tactic:
LieHom.map_lie,

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⁆ =
    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:
by
    obtain ⟨t, hts', htI⟩ := finitelyAtomistic s' hs'S I this
    exact ⟨t, hts'.trans hs'.subset, htI⟩

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
⊢ ⟨y, hy⟩ ∈ center R ↥J

Tactic:
intro j

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, ⟨y, hy⟩⁆ = 0
Module: Mathlib.Data.Multiset.Fintype

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x ↦ x.1) m.toEnumFinset.val

Tactic:
simp

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

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

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

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

Goal state before:
pp: case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v x : α
hx : Fin (count x (v ::ₘ m))
h✝ : ¬(x = v ∧ ↑hx = count v m)
⊢ ((some ⟨x, ⟨↑hx, ⋯⟩⟩).elim ⟨v, ⟨count v m, ⋯⟩⟩ fun x ↦ ⟨x.fst, Fin.castLE ⋯ x.snd⟩) = ⟨x, hx⟩

Tactic:
simp

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

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

Tactic:
simp

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

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

Goal state before:
pp: case refine_2
K : Type v
inst✝ : Field K
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
w✝¹ w✝ : K[X]
h : ¬((aeval (AdjoinRoot.root x.factor)) (x * w✝¹) = 0 ∧ (aeval (AdjoinRoot.root x.factor)) (x * w✝) = 0)
⊢ False

Tactic:
simp only [AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero,
      dvd_mul_of_dvd_left <| factor_dvd_of_not_isUnit hx, true_and, not_true] at h

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

Goal state before:
pp: case sSup_atoms_eq_top
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ sSup {I | IsAtom I} = ⊤

Tactic:
simp

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✝ : HasTrivialRadical R L
⊢ (ad R L).ker = ⊥

Tactic:
simp

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

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f✝ f : K[X]
x : SplittingFieldAux f.natDegree f
⊢ (MvPolynomial.aeval id) (MvPolynomial.X x) = x

Tactic:
simp

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

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
f : K[X]
e : f.SplittingField ≃ₐ[K] SplittingFieldAux f.natDegree f := algEquivSplittingFieldAux f
⊢ e.symm (e 0)⁻¹ = 0

Tactic:
simp

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
⊢ ∀ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 0

Tactic:
intro j

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 × ℕ
⊢ j ∈ v.support → (toSplittingField (Finset.image Prod.fst v.support)) (v j • (subProdXSubC j.1).coeff j.2) = 0
Module: Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : AddCommMonoid M₂
inst✝¹ : Algebra R A
inst✝ : Module R M₂
x✝¹ x✝ : M₂
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry (BilinForm.baseChange A 0)) 1) x✝¹)) 1) x✝ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry 0) 1) x✝¹)) 1) x✝

Tactic:
simp

Goal state after:
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
⊢ eval ((Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X fi)) (map (Ideal.Quotient.mk (maxIdeal k)) X) -
      (Ideal.Quotient.mk (maxIdeal k)) (MvPolynomial.X ⟨fi.fst, fi.snd⟩) =
    0

Tactic:
simp

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
D : LieDerivation R L L
hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule
x : L
⊢ (ad R L) (D x) ∈ ↑(ad R L).range.toSubmodule

Tactic:
simp

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
⊢ LieAlgebra.center R L = ⊥

Tactic:
simp

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

Goal state before:
pp: case h.zero
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
⊢ (f ^ S.sup g) 0 = 0 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ IsNilpotent (f - f)

Tactic:
simp

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

Goal state before:
pp: 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
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q

Tactic:
simp

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

Goal state before:
pp: case mem.inr
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✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hk : k ∈ Ioo p q
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
hk' : k + 1 ∈ Ioo p q
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k ∈ Ioo p q, genWeightSpace M (k • α + χ)

Tactic:
exact le_biSup (fun k ↦ genWeightSpace M (k • α + χ)) hk'

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

Goal state before:
pp: case zero
ι : 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 : L
⊢ 0 ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
simp

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

Goal state before:
pp: case zero
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✝ : LieRing.IsNilpotent ↥H
hq : genWeightSpace M (q • α + χ) = ⊥
x : L
hx : x ∈ rootSpace H α
y : M
⊢ ⁅x, 0⁆ ∈ genWeightSpaceChain M α χ p q

Tactic:
simp

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

Goal state before:
pp: 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 u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
x✝¹ x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ (match x✝¹ + x✝ with
    | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩) =
    (match x✝¹ with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩) +
      match x✝ with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩

Tactic:
simp

Goal state after: