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
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₂
this :
  posFittingComp R L M₂ =
    LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂))
⊢ LieSubmodule.map e.toLieModuleHom (LieSubmodule.map e.symm.toLieModuleHom (posFittingComp R L M₂)) ≤
    LieSubmodule.map e.toLieModuleHom (posFittingComp R L M)

Tactic:
exact LieSubmodule.map_mono (map_posFittingComp_le _)

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
x : L
χ : L → R
⊢ LieSubmodule.map (genWeightSpaceOf M (χ x) x).incl (genWeightSpace (↥(genWeightSpaceOf M (χ x) x)) χ) =
    genWeightSpace M χ

Tactic:
simpa using

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
x : L
χ : L → R
⊢ genWeightSpace M χ ≤ genWeightSpaceOf M (χ x) x
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem.add
ι : 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 : ι
v w : L
hx✝ : v ∈ Submodule.span R (range b.h)
hy✝ : w ∈ Submodule.span R (range b.h)
hv : ⁅v, b.e i⁆ ∈ lieSpan R L (range b.e)
hw : ⁅w, b.e i⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅v + w, b.e i⁆ ∈ lieSpan R L (range b.e)

Tactic:
simpa using

Goal state after:
case mem.add
ι : 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 : ι
v w : L
hx✝ : v ∈ Submodule.span R (range b.h)
hy✝ : w ∈ Submodule.span R (range b.h)
hv : ⁅v, b.e i⁆ ∈ lieSpan R L (range b.e)
hw : ⁅w, b.e i⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅v, b.e i⁆ + ⁅w, b.e i⁆ ∈ lieSpan R L (range b.e)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case mem.smul
ι : 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 : ι
t : R
v : L
hx✝ : v ∈ Submodule.span R (range b.h)
hv : ⁅v, b.e i⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅t • v, b.e i⁆ ∈ lieSpan R L (range b.e)

Tactic:
simpa using

Goal state after:
case mem.smul
ι : 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 : ι
t : R
v : L
hx✝ : v ∈ Submodule.span R (range b.h)
hv : ⁅v, b.e i⁆ ∈ lieSpan R L (range b.e)
⊢ t • ⁅v, b.e i⁆ ∈ lieSpan R L (range b.e)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case add
ι : 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
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : 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:
simpa using

Goal state after:
case add
ι : 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
hx✝ : u ∈ lieSpan R L (range b.e)
hy✝ : 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⁆ + ⁅x, v⁆ ∈ lieSpan R L (range b.e)
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case smul
ι : 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
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.e)
hu : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
⊢ ⁅x, t • u⁆ ∈ lieSpan R L (range b.e)

Tactic:
simpa using

Goal state after:
case smul
ι : 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
t : R
u : L
hx✝ : u ∈ lieSpan R L (range b.e)
hu : ⁅x, u⁆ ∈ lieSpan R L (range b.e)
⊢ t • ⁅x, u⁆ ∈ lieSpan R L (range b.e)
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 : L
hy : y ∈ (lieSpan R L (range b.e)).carrier
x : L
hx : x ∈ H
⊢ ⁅⟨x, hx⟩, y⁆ ∈ (lieSpan R L (range b.e)).carrier

Tactic:
simpa using

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 : L
hy : y ∈ (lieSpan R L (range b.e)).carrier
x : L
hx : x ∈ H
⊢ ⁅x, y⁆ ∈ lieSpan R L (range b.e)
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_1
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
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
⊢ (⁅x, Φ⁆ y) z = (0 y) z

Tactic:
LieHom.lie_apply,

Goal state after:
case refine_1
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
Φ : LinearMap.BilinForm R M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
h : LinearMap.BilinForm.lieInvariant L Φ
x : L
y z : M
⊢ (⁅x, Φ y⁆ - Φ ⁅x, y⁆) z = (0 y) z
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✝ : Module.IsTorsionFree R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ | genWeightSpace M χ ≠ ⊥}

Tactic:
simpa using

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✝ : Module.IsTorsionFree R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
hχ₂ : χ₁ ≠ χ₂
⊢ genWeightSpace M χ₂ = ⊥
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : ↑s ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ ↑t ⊆ ↑s

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : ↑s ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ t ⊆ s
Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Goal state before:
pp: 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
hx : ∀ φ ∈ (domRestrict B W).range, φ x = 0
y : V
hy : y ∈ W
⊢ (B y) x = 0

Tactic:
exact hx (B.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
hI : ¬I = ⊥
J : LieIdeal K L
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : J ⊔ J' = ⊤
⊢ I ≤ J ⊔ J' ⊓ I

Tactic:
by rw [← sup_inf_assoc_of_le _ hJI, this, top_inf_eq]

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
⊢ sSup {I | IsAtom I} = ⊤

Tactic:
simpa using

Goal state after:
case refine_1
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
⊢ sSup {I | IsAtom I} = ⊤
Module: Mathlib.Algebra.Lie.Semisimple.Basic

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✝ : IsIrreducible R L M
aux : ∀ (x y : M), x = y
m : M
⊢ m ∈ ⊥ ↔ m ∈ ⊤

Tactic:
simpa using

Goal state after:
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✝ : IsIrreducible R L M
aux : ∀ (x y : M), x = y
m : M
⊢ m = 0
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)
i : ι
x : L
hx : x ∈ lieSpan R L (range b.f)
⊢ ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
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:
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:
simpa using

Goal state after:
α : 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
⊢ ∀ (a_1 : ℕ), (a, a_1) ∈ s → a_1 + 1 < (filter (fun x ↦ a = x.1) s.val).card
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:
simpa using

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

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

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m₁ m₂ : Multiset α
h : m₁.toEnumFinset ⊆ m₂.toEnumFinset
⊢ m₁ ≤ 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✝¹ : LieRing.IsNilpotent L
χ : L → R
inst✝ : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
a✝ : Nontrivial ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅t • x, ↑m⁆ - χ (t • x) • ↑m = ↑(t • ⁅x, m⁆)

Tactic:
simp only [smul_lie, LinearWeights.map_smul χ (aux R L M χ), smul_assoc t, SetLike.val_smul]

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

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
this : map Prod.fst (Finset.map m.coeEmbedding Finset.univ).val = m
⊢ map (fun x ↦ x.fst) Finset.univ.val = m
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:
simpa using

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 = 0
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
contra : IsEmpty (Weight k L M)
⊢ False

Tactic:
simpa using

Goal state after:
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
contra : IsEmpty (Weight k L M)
⊢ False
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: case inr.left
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) := ⋯
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := ⋯
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := ⋯
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ z ∈ sSup ↑s'

Tactic:
simpa using

Goal state after:
case inr.left
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) := ⋯
hI : I < s.sup id
J : LieIdeal R L
hJs : J ∈ s
hJI : ¬J ≤ I
s' : Finset (LieIdeal R L) := ⋯
hs' : s' ⊂ s
hs'S : ↑s' ⊆ S
K : LieIdeal R L := ⋯
y : L
hy : y ∈ id J
z : L
hz : z ∈ K
hx : y + z ∈ I
j : ↥J
⊢ z ∈ sSup ↑s'
Module: Mathlib.Algebra.Lie.Semisimple.Basic

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

Tactic:
simpa using

Goal state after:
case sSupIndep_isAtom
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
⊢ sSupIndep {⊤}
Module: Mathlib.LinearAlgebra.PID

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f
aux : ∀ (i : ι), B i i ≠ 0 → i ∈ Set.range ⇑snf.f
⊢ ∀ x ∈ Finset.univ, B x x ≠ 0 → x ∈ Set.range ⇑snf.f

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), f x ∈ p
hf' : ∀ x ∈ p, f x ∈ p
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
A : Matrix (Fin n) (Fin n) R := (toMatrix snf.bN snf.bN) (f.restrict hf')
B : Matrix ι ι R := (toMatrix snf.bM snf.bM) f
aux : ∀ (i : ι), B i i ≠ 0 → i ∈ Set.range ⇑snf.f
⊢ ∀ (x : Module.Free.ChooseBasisIndex R M), ¬B x x = 0 → ∃ y, snf.f y = x
Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Goal state before:
pp: k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
hf : f ∈ s
⊢ (∏ x ∈ s, map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑x).Splits

Tactic:
simpa using

Goal state after:
k : Type u
inst✝ : Field k
s : Finset (Monics k)
f : Monics k
hf : f ∈ s
⊢ (∏ x ∈ s, map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑x).Splits
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₂
inst✝ : FaithfulSMul R A
B : BilinForm R M₂
h : BilinForm.baseChange A B = 0
m m' : M₂
⊢ (B m) m' = (0 m) m'

Tactic:
simpa using

Goal state after:
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₂
inst✝ : FaithfulSMul R A
B : BilinForm R M₂
h : BilinForm.baseChange A B = 0
m m' : M₂
⊢ (B m) m' = 0
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ ⊥
⊢ x' ∈ ⊥

Tactic:
simpa using

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
this : e.symm x' ∈ ⊥
⊢ x' = 0
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
y : L
⊢ ∀ (y' : L'), ((killingForm R L') x') y' = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
L' : Type u_4
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : IsKilling R L
e : L ≃ₗ⁅R⁆ L'
x' : L'
hx' : ∀ y ∈ ⊤, ((LieModule.traceForm R L' L') x') y = 0
y : L
⊢ ∀ (y' : L'), ((killingForm R L') x') y' = 0