mathlib-initiative/mathlib-tactics huggingface dataset:
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
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
⊢ ((toEnd R L M) x ∘ₗ (toEnd R L M) y) ^ k = 0

Tactic:
ext m

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
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
m : M
⊢ (((toEnd R L M) x ∘ₗ (toEnd R L M) y) ^ k) m = 0 m
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
x : L
⊢ ((toEnd R L M) x).maxGenEigenspace 0 = ⊤

Tactic:
ext m

Goal state after:
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
x : L
m : M
⊢ m ∈ ((toEnd R L M) x).maxGenEigenspace 0 ↔ m ∈ ⊤
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✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
⊢ Nontrivial ↥(lowerCentralSeriesLast R L M)

Tactic:
LieSubmodule.nontrivial_iff_ne_bot,

Goal state after:
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✝¹ : Nontrivial M
inst✝ : IsNilpotent L M
⊢ lowerCentralSeriesLast R L M ≠ ⊥
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:
← ucs_eq_self_of_normalizer_eq_self h k

Goal state after:
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 ⊥ ≤ ucs k N₁
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₁ N₂ : LieSubmodule R L M
inst✝ : LieModule R L M
l k : ℕ
⊢ lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂

Tactic:
induction k generalizing l with

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

Goal state before:
pp: F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : (Polynomial.map (algebraMap K F) f).Splits
hf0 : f = 0
⊢ L →ₐ[K] ↥⊥

Tactic:
rw [← (splits_iff L f).1 (show f.Splits by simp [hf0])]

Goal state after:
F : Type u
K : Type v
L : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Field F
inst✝² : Algebra K L
inst✝¹ : Algebra K F
f : K[X]
inst✝ : IsSplittingField K L f
hf : (Polynomial.map (algebraMap K F) f).Splits
hf0 : f = 0
⊢ L →ₐ[K] ↥⊤
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 E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ ↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A⟮b⟯.val) x ∈ A⟮(algebraMap B C) b⟯

Tactic:
show (algebraMap B C) b = (Algebra.ofId B C).restrictScalars A b by rfl,

Goal state after:
F : Type u_1
inst✝⁹ : Field F
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
S : Set E
α : E
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : Field A
inst✝⁵ : Field B
inst✝⁴ : Field C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
b : B
x : ↥A⟮b⟯
⊢ ↑((AlgHom.restrictScalars A (Algebra.ofId B C)).comp A⟮b⟯.val) x ∈ A⟮(AlgHom.restrictScalars A (Algebra.ofId B C)) b⟯
Module: Mathlib.FieldTheory.IsAlgClosed.Spectrum

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
⊢ ¬IsUnit (↑ₐ ((fun x ↦ eval x p) k) - (aeval a) p)

Tactic:
aeval_q_eq,

Goal state after:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : 𝕜[X] := C (eval k p) - p
hroot : (C k - X) * -(q / (X - C k)) = q
aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q
⊢ ¬IsUnit ((aeval a) q)
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
x : E
⊢ IsCompactElement F⟮x⟯

Tactic:
simp_rw [isCompactElement_iff_le_of_directed_sSup_le,
    adjoin_simple_le_iff, sSup_eq_iSup', ← exists_prop]

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ ∀ (s : Set (IntermediateField F E)),
    s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → x ∈ ⨆ a, ↑a → ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1
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✝¹ : IsDomain R
inst✝ : IsDomain S
hSR : S ≃+* R
⊢ { e // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }

Tactic:
by
  letI : Algebra R S := RingHom.toAlgebra hSR.symm.toRingHom
  letI : Algebra S R := RingHom.toAlgebra hSR.toRingHom
  letI : Algebra R L := RingHom.toAlgebra ((algebraMap S L).comp (algebraMap R S))
  haveI : IsScalarTower R S L := .of_algebraMap_eq fun _ => rfl
  haveI : IsScalarTower S R L := .of_algebraMap_eq (by simp [RingHom.algebraMap_toAlgebra])
  have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hSR.symm.injective
  have : Algebra.IsAlgebraic R L := (IsAlgClosure.isAlgebraic.extendScalars
    (show Function.Injective (algebraMap S R) from hSR.injective))
  refine ⟨equivOfAlgebraic' R S L M, ?_⟩
  ext x
  simp only [RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingHom.coe_comp,
    AlgEquiv.coe_ringEquiv, RingEquiv.coe_toRingHom]
  conv_lhs => rw [← hSR.symm_apply_apply x]
  change equivOfAlgebraic' R S L M (algebraMap R L (hSR x)) = _
  rw [AlgEquiv.commutes]

Goal state after:
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
⊢ Module.rank F ↥⊥ = 1

Tactic:
rw [rank_eq_one_iff]

Goal state after:
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
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
f : AdjoinRoot (minpoly F α) →+* ↥F⟮α⟯ := AdjoinRoot.lift (↑(Algebra.ofId F ↥F⟮α⟯)) (AdjoinSimple.gen F α) ⋯
this✝ : Fact (Irreducible (minpoly F α))
this : F⟮α⟯.toSubfield ≤ (F⟮α⟯.toSubfield.subtype.comp f).fieldRange
⊢ Function.Surjective ⇑(AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F ↥F⟮α⟯) (AdjoinSimple.gen F α) ⋯)

Tactic:
intro x
          obtain ⟨y, hy⟩ := this (Subtype.mem x)
          exact ⟨y, Subtype.ext hy⟩

Goal state after:
Module: Mathlib.FieldTheory.Extension

Goal state before:
pp: 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
S : Set E
hK : ∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits
L : IntermediateField F E
f : ↥L →ₐ[F] K
hL : L ≤ adjoin F S
⊢ ∃ φ, φ.comp (inclusion hL) = f

Tactic:
by
  obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
    (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl
  refine ⟨φ.emb.comp (inclusion <| adjoin_le_iff.mpr fun s hs ↦ ?_), ?_⟩
  · rcases φ.exists_lift_of_splits (hK s hs).1 (hK s hs).2 with ⟨y, h1, h2⟩
    exact (hφ h1).1 h2
  · ext; apply hfφ.2

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

Goal state before:
pp: R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent L
⊢ ⊤.normalizer = ⊤

Tactic:
by rw [← top_toLieSubalgebra, normalizer_eq_top, top_toLieSubalgebra]

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

Goal state before:
pp: case mem.mem.inl.inr.inr
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
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ -(2 • u) ∈ span R {u, f, v}

Tactic:
neg_mem_iff

Goal state after:
case mem.mem.inl.inr.inr
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
f x y u v : L
t : IsSl2Triple v u f
__spread✝⁻⁰ : Submodule R L := span R {u, f, v}
⊢ 2 • u ∈ span R {u, f, v}
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inr.inl.inl
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 x y u v : L
t : IsSl2Triple h v u
__spread✝⁻⁰ : Submodule R L := span R {v, u, h}
⊢ -h ∈ span R {v, u, h}

Tactic:
neg_mem_iff

Goal state after:
case mem.mem.inr.inl.inl
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 x y u v : L
t : IsSl2Triple h v u
__spread✝⁻⁰ : Submodule R L := span R {v, u, h}
⊢ h ∈ span R {v, u, h}
Module: Mathlib.Algebra.Lie.Sl2

Goal state before:
pp: case mem.mem.inr.inr.inr.inl
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
e x y u v : L
t : IsSl2Triple u e v
__spread✝⁻⁰ : Submodule R L := span R {e, v, u}
⊢ -(2 • v) ∈ span R {e, v, u}

Tactic:
neg_mem_iff

Goal state after:
case mem.mem.inr.inr.inr.inl
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
e x y u v : L
t : IsSl2Triple u e v
__spread✝⁻⁰ : Submodule R L := span R {e, v, u}
⊢ 2 • v ∈ span R {e, v, u}
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x y : ↥(rootSpace H χ₁)
⊢ { toFun := fun m ↦ ⟨⁅↑(x + y), ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m ↦ ⟨⁅↑y, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext m

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
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x y : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ ↑({ toFun := fun m ↦ ⟨⁅↑(x + y), ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } m) =
    ↑(({ toFun := fun m ↦ ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := fun m ↦ ⟨⁅↑y, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ })
        m)
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
t : R
x : ↥(rootSpace H χ₁)
⊢ { toFun := fun m ↦ ⟨⁅↑(t • x), ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    t • { toFun := fun m ↦ ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext m

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
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
t : R
x : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ ↑({ toFun := fun m ↦ ⟨⁅↑(t • x), ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } m) =
    ↑((t • { toFun := fun m ↦ ⟨⁅↑x, ↑m⁆, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }) m)
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥H
y : ↥(rootSpace H χ₁)
⊢ (rootSpaceWeightSpaceProductAux R L H M hχ).toFun ⁅x, y⁆ = ⁅x, (rootSpaceWeightSpaceProductAux R L H M hχ).toFun y⁆

Tactic:
ext m

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
inst✝⁴ : LieRing.IsNilpotent ↥H
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥H
y : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ ↑(((rootSpaceWeightSpaceProductAux R L H M hχ).toFun ⁅x, y⁆) m) =
    ↑(⁅x, (rootSpaceWeightSpaceProductAux R L H M hχ).toFun y⁆ m)
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
⊢ ↑(genWeightSpace M (χ ∘ ⇑⊤.incl)) = ↑(genWeightSpace M χ)

Tactic:
ext m

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
χ : L → R
m : M
⊢ m ∈ ↑(genWeightSpace M (χ ∘ ⇑⊤.incl)) ↔ m ∈ ↑(genWeightSpace M χ)
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
inst✝ : IsArtinian R M
h : ∀ N < ⊤, IsCompl (genWeightSpace (↥N) 0) (posFittingComp R L ↥N)
M₀ : LieSubmodule R L M := genWeightSpace M 0
M₁ : LieSubmodule R L M := posFittingComp R L M
x : L
M₀ₓ : LieSubmodule R L M := genWeightSpaceOf M 0 x
hx : M₀ₓ ≠ ⊤
M₁ₓ : LieSubmodule R L M := posFittingCompOf R M x
M₀ₓ₀ : LieSubmodule R L ↥M₀ₓ := genWeightSpace (↥M₀ₓ) 0
M₀ₓ₁ : LieSubmodule R L ↥M₀ₓ := posFittingComp R L ↥M₀ₓ
h₁ : IsCompl M₀ₓ M₁ₓ
h₂ : IsCompl M₀ₓ₀ M₀ₓ₁
⊢ genWeightSpace M 0 ≤ M₀ₓ

Tactic:
exact iInf_le _ x

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

Goal state before:
pp: R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
⊢ (B (φ w - ψ w)) v = 0

Tactic:
sub_left,

Goal state after:
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
⊢ (B (φ w)) v - (B (ψ w)) v = 0
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
I : LieIdeal K L
hI : I ∈ {I | IsAtom I}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
⊢ ⁅↑x, z⁆ = 0

Tactic:
rw [← LieSubmodule.mem_bot (R := K) (L := L), ← (hJ.disjoint_of_ne hI hJI).eq_bot]

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}
J : LieIdeal K L
hJ : IsAtom J
hJI : ¬J = I
x : ↥J
y : ↥J
z : L
hz : z ∈ I
⊢ ⁅↑x, z⁆ ∈ J ⊓ 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
⊢ ⊥ = ⊤

Tactic:
ext m

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 ∈ ⊥ ↔ m ∈ ⊤
Module: Mathlib.Algebra.Lie.Semisimple.Basic

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSimple R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
⊢ ¬I = ⊤

Tactic:
rintro rfl

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
hI : IsLieAbelian ↥⊤
⊢ False
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
x : L
y : ↥I
hy : y ∈ ↑↑J
hx : x ∈ I ⊔ sSup ({I' | IsAtom I'} \ {I})
⊢ ⁅x, ↑I.incl y⁆ ∈ (Submodule.map ↑I.incl ↑J).carrier

Tactic:
rw [LieSubmodule.mem_sup] at hx

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 : IsAtom I
J : LieIdeal R ↥I
x : L
y : ↥I
hy : y ∈ ↑↑J
hx : ∃ y ∈ I, ∃ z ∈ sSup ({I' | IsAtom I'} \ {I}), y + z = x
⊢ ⁅x, ↑I.incl y⁆ ∈ (Submodule.map ↑I.incl ↑J).carrier
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.a.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 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₃, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
neg_mem_iff

Goal state after:
case lie.a.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 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₃, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
Module: Mathlib.Algebra.Lie.Basis.Basic

Goal state before:
pp: case lie.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 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₄, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower

Tactic:
neg_mem_iff

Goal state after:
case lie.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 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₄, u⁆ ∈ H.toLieSubmodule ⊔ b.borelLower
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
hχ : genWeightSpace M χ ≠ ⊥
⊢ 0 < finrank R ↥(genWeightSpace M χ)

Tactic:
by
  rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
    Nat.cast_pos] at hχ

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : m.ToType
⊢ x.fst = v → ¬↑x.snd = count v m

Tactic:
rintro rfl

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
x : m.ToType
⊢ ¬↑x.snd = count x.fst m