mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N₁ N₂ : LieSubmodule R L M
⊢ (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer

Tactic:
by
  ext; simp [← forall_and]

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

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
x y z : L
hx : x ∈ H.normalizer
hy : ∃ y_1 ∈ R ∙ x, ∃ z ∈ H.toSubmodule, y_1 + z = y
hz : ∃ y ∈ R ∙ x, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
⊢ ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
obtain ⟨u₁, hu₁, v, hv : v ∈ H, rfl⟩ := hy

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x z : L
hx : x ∈ H.normalizer
hz : ∃ y ∈ R ∙ x, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
u₁ : L
hu₁ : u₁ ∈ R ∙ x
v : L
hv : v ∈ H
⊢ ⁅u₁ + v, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
Module: Mathlib.Algebra.Lie.Normalizer

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
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H

Tactic:
exact (H.mem_normalizer_iff' x).mp hx z hz

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

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ ((toEnd R L M) x ^ k) m = 0 m

Tactic:
rw [Module.End.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ (⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ ∃ k, ∀ (x : L), (toEnd R L M) x ^ k = 0

Tactic:
obtain ⟨k, hM⟩ := IsNilpotent.nilpotent R L M
  use k
  intro x; ext m
  rw [Module.End.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]
  exact iterate_toEnd_mem_lowerCentralSeries R L M x m k

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

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
this : DecidableEq R := Classical.decEq R
g' : G ⧸ stabilizer G x
⊢ g • (X - C (ofQuotientStabilizer G x g')) = X - C (ofQuotientStabilizer G x (g • g'))

Tactic:
rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k N₁ = N₁

Tactic:
by
  induction k with
  | zero => simp
  | succ k ih => rwa [ucs_succ, ih]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k ⊥ ≤ N₁

Tactic:
rw [← ucs_eq_self_of_normalizer_eq_self h k]
  gcongr
  simp

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

Goal state before:
pp: case splits'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ (Polynomial.map (algebraMap F L) (f * g)).Splits

pp: case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤

Tactic:
· rw [Polynomial.map_mul, IsScalarTower.algebraMap_eq F K L, ← map_map, ← map_map]
    exact Splits.mul ((splits K f).map _) (splits L (g.map (algebraMap F K)))

Goal state after:
case adjoin_rootSet'
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
x : E
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simpa only [Set.mem_iInter] using! Set.ext_iff.1 (coe_sInf S) x

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Field

Goal state before:
pp: F : Type u_5
E : Type u_6
K : Type u_7
inst✝⁹ : CommSemiring F
inst✝⁸ : StrongRankCondition F
inst✝⁷ : CommSemiring E
inst✝⁶ : StrongRankCondition E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Algebra F K
inst✝¹ : IsScalarTower F E K
L : Subalgebra F K
inst✝ : Module.Free F ↥L
⊢ Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
    L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]
  exact rank_span_le _ |>.trans Cardinal.mk_range_le

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

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
p : k[X]
hp : p = C (p.coeff 0)
⊢ p.roots = 0

Tactic:
rw [hp, roots_C]

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

Goal state before:
pp: k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ IsAlgClosed k'

Tactic:
apply IsAlgClosed.of_exists_root

Goal state after:
k : Type u
inst✝² : Field k
k' : Type u
inst✝¹ : Field k'
e : k ≃+* k'
inst✝ : IsAlgClosed k
⊢ ∀ (p : k'[X]), p.Monic → Irreducible p → ∃ x, eval x p = 0
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ (↑⟨⊥, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier

pp: case inr
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
i : Lifts F E K
hi : i ∈ c
⊢ (↑⟨i, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier

Tactic:
exacts [bot_le, le_iSup_of_le ⟨i, hi⟩ le_rfl]

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

Goal state before:
pp: k : Type u
inst✝²⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²⁵ : Field K
inst✝²⁴ : Field J
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Field L
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra R M
inst✝¹⁸ : IsTorsionFree R M
inst✝¹⁷ : IsAlgClosure R M
inst✝¹⁶ : Algebra K M
inst✝¹⁵ : IsAlgClosure K M
inst✝¹⁴ : Algebra S L
inst✝¹³ : IsTorsionFree S L
inst✝¹² : IsAlgClosure S L
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R L
inst✝⁹ : IsScalarTower R S L
inst✝⁸ : Algebra K J
inst✝⁷ : Algebra J L
inst✝⁶ : IsAlgClosure J L
inst✝⁵ : Algebra K L
inst✝⁴ : IsScalarTower K J L
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : Algebra.IsAlgebraic R L
⊢ L ≃ₐ[R] M

Tactic:
have : IsTorsionFree R L := .trans_faithfulSMul R S L

Goal state after:
k : Type u
inst✝²⁶ : Field k
K : Type u_1
J : Type u_2
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝²⁵ : Field K
inst✝²⁴ : Field J
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Field L
inst✝²⁰ : Field M
inst✝¹⁹ : Algebra R M
inst✝¹⁸ : IsTorsionFree R M
inst✝¹⁷ : IsAlgClosure R M
inst✝¹⁶ : Algebra K M
inst✝¹⁵ : IsAlgClosure K M
inst✝¹⁴ : Algebra S L
inst✝¹³ : IsTorsionFree S L
inst✝¹² : IsAlgClosure S L
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R L
inst✝⁹ : IsScalarTower R S L
inst✝⁸ : Algebra K J
inst✝⁷ : Algebra J L
inst✝⁶ : IsAlgClosure J L
inst✝⁵ : Algebra K L
inst✝⁴ : IsScalarTower K J L
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : Algebra.IsAlgebraic R L
this : IsTorsionFree R L
⊢ L ≃ₐ[R] M
Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x✝ : E
hx : x✝ ∈ ⨆ i, f i
i : ι
x : E
h : x ∈ f i
⊢ x ∈ ⨆ i, F⟮↑i.snd⟯

Tactic:
exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x)

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
x : V
hx : x ∈ ↑p
⊢ f x - ((algebraMap K (End K V)) μ') x ∈ ↑p

Tactic:
algebraMap_end_apply

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi ↦ xi) ∈ p
hm₁ : (m.sum fun _i xi ↦ xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ ((f - i • 1) ^ l i).ker
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ ↦ (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
x : V
hx : x ∈ ↑p
⊢ f x - μ' • x ∈ ↑p
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case zero
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
hi : 0 ≤ n
H : ((toEnd R L M) f ^ 0) m = 0
⊢ False

pp: case succ
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
n✝ : ℕ
a✝ : n✝ ≤ n → ((toEnd R L M) f ^ n✝) m = 0 → False
hi : n✝ + 1 ≤ n
H : ((toEnd R L M) f ^ (n✝ + 1)) m = 0
⊢ False

Tactic:
· exact P.ne_zero (by simpa using H)

Goal state after:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
n : ℕ
hn : μ = ↑n
n✝ : ℕ
a✝ : n✝ ≤ n → ((toEnd R L M) f ^ n✝) m = 0 → False
hi : n✝ + 1 ≤ n
H : ((toEnd R L M) f ^ (n✝ + 1)) m = 0
⊢ False
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✝ : IsNoetherian R M
⊢ ⨆ k, LieSubmodule.ucs k ⊥ = genWeightSpace M 0

Tactic:
obtain ⟨k, hk⟩ := (LieSubmodule.isNilpotent_iff_exists_self_le_ucs
    <| genWeightSpace M (0 : L → R)).mp inferInstance
  refine le_antisymm (iSup_ucs_le_genWeightSpace_zero R L M) (le_trans hk ?_)
  exact le_iSup (fun k ↦ (⊥ : LieSubmodule R L M).ucs k) k

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

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

Tactic:
| lie u v hu hv hu' hv' =>

Goal state after:
Module: Mathlib.Order.BooleanGenerators

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
⊢ ∀ b ∈ X, b ≤ sSup (T₁ ∩ T₂)

Tactic:
intro I hI

Goal state after:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup (T₁ ∩ T₂)
Module: Mathlib.Algebra.Lie.InvariantForm

Goal state before:
pp: case refine_2
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
⊢ sSupIndep {I | IsAtom I}

Tactic:
intro I hI

Goal state after:
case refine_2
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 ∈ {I | IsAtom I}
⊢ Disjoint I (sSup ({I | IsAtom I} \ {I}))
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✝ : IsSimple R L
⊢ ∀ (I : LieIdeal R L), IsLieAbelian ↥I → I = ⊥

Tactic:
intro I hI

Goal state after:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
⊢ I = ⊥
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
⊢ ⁅b.e i, ⁅u, v⁆⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
| lie u v hu hv hu' hv' =>

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
⊢ False

Tactic:
replace h : {x ∈ s | x.1 = a} ⊆ {a} ×ˢ .range (card (s.1.filter fun x ↦ a = x.1) - 1) := by
      simpa +contextual [forall_comm (β := _ = a), Finset.subset_iff,
        imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h

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)
⊢ False
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 dsimp; infer_instance

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 dsimp; infer_instance

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), IsLieAbelian ↥I → I = ⊥

Tactic:
intro I hI

Goal state after:
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 : IsLieAbelian ↥I
⊢ I = ⊥
Module: Mathlib.Algebra.Lie.Killing

Goal state before:
pp: case mpr
R : Type u_1
L : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : IsKilling R L
inst✝³ : Module.Free R L
inst✝² : Module.Finite R L
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ Subsingleton L → IsLieAbelian L

Tactic:
exact fun _ => inferInstance

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

Goal state before:
pp: case h.mem
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 x : M
hx : x ∈ ↑S
⊢ (f ^ S.sup g) x = 0 x

Tactic:
exact pow_map_zero_of_le (Finset.le_sup hx) (hg x)

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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun k ↦ k • χ₁ + χ₂
this : Injective f
⊢ ∀ᶠ (k : ℕ) in Filter.cofinite, genWeightSpace M (k • χ₁ + χ₂) = ⊥

Tactic:
Filter.eventually_cofinite,

Goal state after:
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
inst✝³ : IsAddTorsionFree R
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : IsNoetherian R M
hχ₁ : χ₁ ≠ 0
f : ℕ → L → R := fun k ↦ k • χ₁ + χ₂
this : Injective f
⊢ {x | ¬genWeightSpace M (x • χ₁ + χ₂) = ⊥}.Finite
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.hy.a
ι : 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
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
yc : L
hyc : yc ∈ H
yl : L
hyl : yl ∈ lieSpan R L (range b.f)
yu : L
hyu : yu ∈ lieSpan R L (range b.e)
aux : yc + yl + yu = ⁅u, z⁆
⊢ ⁅v, yu⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
rw [← lie_skew, neg_mem_iff]
        exact LieSubmodule.mem_sup_right <| LieSubalgebra.lie_mem _ hyu hv

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 : L
this : ∀ (i : ι), ∀ x ∈ lieSpan R L (range b.f), ⁅b.e i, x⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
u v : L
hu : u ∈ lieSpan R L (range b.e)
hv : v ∈ lieSpan R L (range b.e)
hu' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅u, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
hv' : ∀ {z : L}, z ∈ lieSpan R L (range b.f) → ⁅v, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper
z : L
hz : z ∈ lieSpan R L (range b.f)
⊢ ⁅⁅u, v⁆, z⁆ ∈ H.toLieSubmodule ⊔ b.borelLower ⊔ b.borelUpper

Tactic:
| lie u v hu hv hu' hv' =>

Goal state after: